HostBodyModes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exhaustive localization of bodies in canonical host modes

All entry and role hypotheses refer to the actual canonical host. The numerical order premise is exactly the four parent comparisons supplied by the two tree orders.

def OAI.Problem348.Construction.BodyNodeOrder line 17
Source documentation
The necessary parent comparison for an ordered body in each of the six modes.
```
def BodyNodeOrder {h : ℕ} (t : Mode h) (r₀ r₁ c₀ c₁ : Position h) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.rowRole_first_variable line 23
theorem OAI.Problem348.Construction.colRole_horizontal_variable line 30
theorem OAI.Problem348.Construction.host_horizontal_plus_not_body line 40
Source documentation
The horizontal plus roles cannot realize the body's top row.
```
theorem host_horizontal_plus_not_body {h : ℕ} {t : Mode h}
    (hklo : 2 ≤ kind t) (hkhi : kind t < 4) {r₀ r₁ c₀ c₁ : Position h}
    (hr₀ : rowRole t 0 r₀) (hc₀ : colRole t 0 c₀) (hc₁ : colRole t 1 c₁)
    (horder : positionNode c₀ ≤ positionNode c₁ / 2) :
    ¬ IsP (host r₀ c₀) (host r₀ c₁) (host r₁ c₀) (host r₁ c₁) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.kind, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.positionNode, OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.host_horizontal_minus_leaf_diagonal line 63

Source documentation

The horizontal minus roles force the body's top-left entry onto a shared leaf.

theorem host_horizontal_minus_leaf_diagonal {h : ℕ} {t : Mode h}
    (hklo : 4 ≤ kind t) {r₀ r₁ c₀ c₁ : Position h}
    (hr₀ : rowRole t 0 r₀) (hc₀ : colRole t 0 c₀) (hc₁ : colRole t 1 c₁)
    (horder : positionNode c₀ / 2 ≤ positionNode c₁)
    (hb : 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)) := by
…

Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.kind, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.positionNode, OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.host_body_leaf_diagonal line 92

Source documentation

Under BodyNodeOrder, every ordered body in any canonical mode has its top-left cell on the shared leaf diagonal.

theorem host_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₁)
    (horder : BodyNodeOrder t r₀ r₁ c₀ c₁)
    (hb : 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)) := by
…

Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.BodyNodeOrder, OAI.Problem348.Construction.host