ModeLocalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Localization of the four body modes

The arithmetic case analysis assumes the stated order inequalities and entry values, independently of the host-position encoding.

def OAI.Problem348.ModeLocalization.IsP line 15
Source documentation
The four entries of the body pattern, in row-major order.
```
def IsP (a b c d : Bool) : Prop :=
…
```
theorem OAI.Problem348.ModeLocalization.le_iff_parent_le_of_same_parity line 19
Source documentation
Within either parity class, taking the parent preserves and reflects order.
```
theorem le_iff_parent_le_of_same_parity {p q : ℕ}
    (hparity : p % 2 = q % 2) :
    p ≤ q ↔ p / 2 ≤ q / 2 := by
…
```
theorem OAI.Problem348.ModeLocalization.eq_of_parent_eq_of_same_parity line 24
theorem OAI.Problem348.ModeLocalization.vPlus_not_isP line 29
Source documentation
A V_i^+ body cannot match P: its row order forces the zero to be one.
```
theorem vPlus_not_isP (p a b : ℕ) (horder : p / 2 ≤ a) :
    ¬ IsP true (decide (p / 2 ≤ b)) true (decide (a ≤ b)) := by
…
```
Mentions: OAI.Problem348.ModeLocalization.IsP
theorem OAI.Problem348.ModeLocalization.vMinus_not_isP line 35
Source documentation
A V_i^- body cannot match P: its row order forces the last one to be zero.
```
theorem vMinus_not_isP (p a b : ℕ) (horder : a ≤ p / 2) :
    ¬ IsP true (decide (a < b)) true (decide (p / 2 < b)) := by
…
```
Mentions: OAI.Problem348.ModeLocalization.IsP
theorem OAI.Problem348.ModeLocalization.wPlus_not_isP line 41
Source documentation
A W_{i,d}^+ body cannot match P, including at the shared leaf level.
```
theorem wPlus_not_isP (p q b : ℕ) (horder : b ≤ q / 2)
    (hparity : p % 2 = q % 2) :
    ¬ IsP (decide (p / 2 ≤ b)) (decide (p ≤ q)) true true := by
…
```
Mentions: OAI.Problem348.ModeLocalization.IsP

theorem OAI.Problem348.ModeLocalization.wMinus_isP_implies_leaf_diagonal line 48

Source documentation

In a minus W mode, a body match can occur only on a shared leaf diagonal.

theorem wMinus_isP_implies_leaf_diagonal
    (h i p q b : ℕ) (horder : q / 2 ≤ b)
    (hparity : p % 2 = q % 2)
    (hbody : IsP (if i = h then decide (p ≤ q) else decide (p < q))
      (decide (p / 2 < b)) true true) :
    i = h ∧ p = q := by
…

Mentions: OAI.Problem348.ModeLocalization.IsP

theorem OAI.Problem348.ModeLocalization.wMinus_leaf_diagonal_isP line 65
Source documentation
Conversely, the diagonal leaf choice with its parent column gives P.
```
theorem wMinus_leaf_diagonal_isP (h p : ℕ) :
    IsP (if h = h then decide (p ≤ p) else decide (p < p))
      (decide (p / 2 < p / 2)) true true := by
…
```
Mentions: OAI.Problem348.ModeLocalization.IsP