CanonicalHorizontal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Horizontal body localization for the canonical host entry table.

theorem OAI.Problem348.Construction.horizontal_plus_entries_impossible line 10

theorem OAI.Problem348.Construction.horizontal_minus_entries_localize line 20

Source documentation

A W- body forces the shared leaf diagonal, as literal variable positions.

theorem horizontal_minus_entries_localize {h i : ℕ} {r c₀ c₁ : VariablePosition h}
    (hr : AtLevel (i + 1) false r) (hc₀ : AtLevel (i + 1) false c₀)
    (hc₁ : AtLevel i false c₁)
    (horder : node c₀ / 2 ≤ node c₁) (hparity : node r % 2 = node c₀ % 2)
    (h₀ : variableEntry r c₀ = true) (h₁ : variableEntry r c₁ = false) :
    i + 1 = h ∧ ∃ z : Fin (2 ^ h),
      r = (Fin.last (2 * h), z) ∧ c₀ = (Fin.last (2 * h), z) := by
…

Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.AtLevel, OAI.Problem348.Construction.node, OAI.Problem348.Construction.variableEntry