BodyExtension.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The anchor/body extension step for arbitrary repairs. The finite-order gluing lemma is independent of the host construction.

def OAI.Problem348.appendTwo line 17
Source documentation
Append two values to a function on a finite initial segment.
```
def appendTwo {α : Type uAlpha} {k : ℕ} (f : Fin k → α) (a b : α) :
    Fin (k + 2) → α := fun i =>
…
```
theorem OAI.Problem348.appendTwo_initial line 21
theorem OAI.Problem348.appendTwo_first line 26
theorem OAI.Problem348.appendTwo_second line 31
theorem OAI.Problem348.strictMono_appendTwo line 36
def OAI.Problem348.appendTwoIncreasing line 54
Source documentation
The increasing map obtained by appending two positions after an anchor.
```
def appendTwoIncreasing {k n : ℕ} (r : IncreasingMap k n)
    (a b : Fin n) (ha : ∀ i, r.val i < a) (hab : a < b) :
    IncreasingMap (k + 2) n :=
…
```
Mentions: OAI.Problem348.IncreasingMap

theorem OAI.Problem348.appendTwo_matches_fixedH line 60

Source documentation

An anchor and the four body entries reproduce every entry of the fixed pattern.

theorem appendTwo_matches_fixedH {n : ℕ} (B : BinaryMatrix n)
    (r c : IncreasingMap 64 n) (r₀ r₁ c₀ c₁ : Fin n)
    (hanchor : ∀ u v, B (r.val u) (c.val v) = anchor64 u v)
    (hrow₀ : ∀ v, B r₀ (c.val v) = decide (v.val = 0))
    (hrow₁ : ∀ v, B r₁ (c.val v) = decide (v.val = 1))
    (hcol₀ : ∀ u, B (r.val u) c₀ = decide (u.val = 0))
    (hcol₁ : ∀ u, B (r.val u) c₁ = decide (u.val = 1))
    (h₀₀ : B r₀ c₀ = true) (h₀₁ : B r₀ c₁ = false)
    (h₁₀ : B r₁ c₀ = true) (h₁₁ : B r₁ c₁ = true) :
    ∀ i j : Fin 66,
      B (appendTwo r.val r₀ r₁ i) (appendTwo c.val c₀ c₁ j) = fixedH i j := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.IncreasingMap, OAI.Problem348.anchor64, OAI.Problem348.appendTwo, OAI.Problem348.fixedH

theorem OAI.Problem348.not_HFree_of_anchor_body line 90

Source documentation

The exact anchor-extension bridge needed by arbitrary-repair propagation.

theorem not_HFree_of_anchor_body {n : ℕ} (B : BinaryMatrix n)
    (r c : IncreasingMap 64 n) (r₀ r₁ c₀ c₁ : Fin n)
    (hr : ∀ i, r.val i < r₀) (hr₀₁ : r₀ < r₁)
    (hc : ∀ j, c.val j < c₀) (hc₀₁ : c₀ < c₁)
    (hanchor : ∀ u v, B (r.val u) (c.val v) = anchor64 u v)
    (hrow₀ : ∀ v, B r₀ (c.val v) = decide (v.val = 0))
    (hrow₁ : ∀ v, B r₁ (c.val v) = decide (v.val = 1))
    (hcol₀ : ∀ u, B (r.val u) c₀ = decide (u.val = 0))
    (hcol₁ : ∀ u, B (r.val u) c₁ = decide (u.val = 1))
    (h₀₀ : B r₀ c₀ = true) (h₀₁ : B r₀ c₁ = false)
    (h₁₀ : B r₁ c₀ = true) (h₁₁ : B r₁ c₁ = true) :
    ¬ HFree fixedH B := by
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.IncreasingMap, OAI.Problem348.anchor64, OAI.Problem348.HFree, OAI.Problem348.fixedH