OrderedBodyLocalization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Body localization for the independent host enumerations

The canonical full-axis enumeration gives exhaustive body-mode localization. All comparisons use the actual row and column indices; no order-reflection certificate remains as an assumption.

theorem OAI.Problem348.OrderedHost.rowIndex_reflects_variable_order line 18
theorem OAI.Problem348.OrderedHost.columnIndex_reflects_variable_order line 23

theorem OAI.Problem348.OrderedHost.bodyNodeOrder_of_indices line 29

Source documentation

The actual independent enumerations discharge all four numerical mode orders.

theorem bodyNodeOrder_of_indices {h : ℕ} {t : Mode h}
    {r₀ r₁ c₀ c₁ : Position h}
    (hr₀ : rowRole t 0 r₀) (hr₁ : rowRole t 1 r₁)
    (hc₀ : colRole t 0 c₀) (hc₁ : colRole t 1 c₁)
    (hrow : rowIndex h r₀ < rowIndex h r₁)
    (hcol : columnIndex h c₀ < columnIndex h c₁) :
    BodyNodeOrder t r₀ r₁ c₀ c₁ :=
…

Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex

theorem OAI.Problem348.OrderedHost.body_leaf_diagonal line 42

Source documentation

Every correctly assigned ordered body in the canonical host has its top-left cell on the shared leaf diagonal.

theorem body_leaf_diagonal {h : ℕ} {t : Mode h}
    {r₀ r₁ c₀ c₁ : Position h}
    (hr₀ : rowRole t 0 r₀) (hr₁ : rowRole t 1 r₁)
    (hc₀ : colRole t 0 c₀) (hc₁ : colRole t 1 c₁)
    (hrow : rowIndex h r₀ < rowIndex h r₁)
    (hcol : columnIndex h c₀ < columnIndex h c₁)
    (hb : ModeLocalization.IsP (host r₀ c₀) (host r₀ c₁)
      (host r₁ c₀) (host r₁ c₁)) :
    ∃ z : Fin (2 ^ h),
      r₀ = Sum.inr (Sum.inl (Fin.last (2 * h), z)) ∧
      c₀ = Sum.inr (Sum.inl (Fin.last (2 * h), z)) :=
…

Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.ModeLocalization.IsP