PathPropagation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Boolean propagation independent of the host construction. No entry between variable positions is assumed to remain unchanged. Only the dummy incidences, root bits, and identification of the two leaves are hypotheses.

def OAI.Problem348.PathPropagation.Body line 19
Source documentation
The lower-right two-by-two pattern of the fixed matrix fixedH.
```
def Body (B : R → C → Bool) (r₁ r₂ : R) (c₁ c₂ : C) : Prop :=
…
```

theorem OAI.Problem348.PathPropagation.vertical_plus line 24

Source documentation

Avoiding the body propagates a one upwards across a column of dummy ones.

theorem vertical_plus {B : R → C → Bool} {r₁ r₂ : R} {c₁ c₂ : C}
    (havoid : ¬ Body B r₁ r₂ c₁ c₂)
    (h₁ : B r₁ c₁ = true) (h₂ : B r₂ c₁ = true)
    (h₃ : B r₂ c₂ = true) : B r₁ c₂ = true := by
…

Mentions: OAI.Problem348.PathPropagation.Body

theorem OAI.Problem348.PathPropagation.vertical_minus line 33

Source documentation

Avoiding the body propagates a zero downwards across dummy ones.

theorem vertical_minus {B : R → C → Bool} {r₁ r₂ : R} {c₁ c₂ : C}
    (havoid : ¬ Body B r₁ r₂ c₁ c₂)
    (h₁ : B r₁ c₁ = true) (h₂ : B r₂ c₁ = true)
    (h₃ : B r₁ c₂ = false) : B r₂ c₂ = false := by
…

Mentions: OAI.Problem348.PathPropagation.Body

theorem OAI.Problem348.PathPropagation.horizontal_plus line 42

Source documentation

Avoiding the body propagates a one rightwards above a dummy row.

theorem horizontal_plus {B : R → C → Bool} {r₁ r₂ : R} {c₁ c₂ : C}
    (havoid : ¬ Body B r₁ r₂ c₁ c₂)
    (h₁ : B r₁ c₁ = true) (h₂ : B r₂ c₁ = true)
    (h₃ : B r₂ c₂ = true) : B r₁ c₂ = true :=
…

Mentions: OAI.Problem348.PathPropagation.Body

theorem OAI.Problem348.PathPropagation.horizontal_minus line 49

Source documentation

Avoiding the body propagates a zero leftwards above a dummy row.

theorem horizontal_minus {B : R → C → Bool} {r₁ r₂ : R} {c₁ c₂ : C}
    (havoid : ¬ Body B r₁ r₂ c₁ c₂)
    (h₁ : B r₁ c₂ = false) (h₂ : B r₂ c₁ = true)
    (h₃ : B r₂ c₂ = true) : B r₁ c₁ = false := by
…

Mentions: OAI.Problem348.PathPropagation.Body

def OAI.Problem348.PathPropagation.ModeBody line 59
Source documentation
One of the four mode bodies encountered at the edge from level i to level i + 1 of the selected path.
```
def ModeBody (B : R → C → Bool)
    (xp xm : ℕ → R) (yp ym : ℕ → C) (xd : R) (yd : C) (i : ℕ) : Prop :=
…
```

theorem OAI.Problem348.PathPropagation.propagate line 68

Source documentation

The induction invariant: absence of all four mode bodies preserves the opposite plus and minus bits at every level of the selected path.

theorem propagate {B : R → C → Bool}
    {xp xm : ℕ → R} {yp ym : ℕ → C} {xd : R} {yd : C} {h : ℕ}
    (hrootp : B (xp 0) (yp 0) = true)
    (hrootm : B (xm 0) (ym 0) = false)
    (hdcol : ∀ i, i ≤ h → B (xp i) yd = true ∧ B (xm i) yd = true)
    (hdrow : ∀ i, i ≤ h → B xd (yp i) = true ∧ B xd (ym i) = true)
    (havoid : ∀ i, i < h → ¬ ModeBody B xp xm yp ym xd yd i) :
    ∀ i, i ≤ h → B (xp i) (yp i) = true ∧ B (xm i) (ym i) = false := by
…

Mentions: OAI.Problem348.PathPropagation.ModeBody

theorem OAI.Problem348.PathPropagation.exists_modeBody line 101

Source documentation

Opposite root entries and shared leaves force some mode body. Arbitrary changes to every other variable-variable entry are explicitly allowed.

theorem exists_modeBody {B : R → C → Bool}
    {xp xm : ℕ → R} {yp ym : ℕ → C} {xd : R} {yd : C} {h : ℕ}
    (hrootp : B (xp 0) (yp 0) = true)
    (hrootm : B (xm 0) (ym 0) = false)
    (hdcol : ∀ i, i ≤ h → B (xp i) yd = true ∧ B (xm i) yd = true)
    (hdrow : ∀ i, i ≤ h → B xd (yp i) = true ∧ B xd (ym i) = true)
    (hleafr : xp h = xm h) (hleafc : yp h = ym h) :
    ∃ i, i < h ∧ ModeBody B xp xm yp ym xd yd i := by
…

Mentions: OAI.Problem348.PathPropagation.ModeBody