HostBodyOrder.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

From increasing body positions to the four node-order inequalities

These lemmas use the actual host roles and tree keys. Each independent coordinate map reflects the corresponding tree-key order on variable positions; no mode-specific ordering is assumed.

theorem OAI.Problem348.Construction.vertical_plus_node_order line 18
theorem OAI.Problem348.Construction.vertical_minus_node_order line 35
theorem OAI.Problem348.Construction.horizontal_plus_node_order line 52
theorem OAI.Problem348.Construction.horizontal_minus_node_order line 73

theorem OAI.Problem348.Construction.bodyNodeOrder_of_ordered line 98

Source documentation

Increasing positions in the actual two tree orders satisfy precisely the node-order premise of the exhaustive six-mode localization theorem.

theorem bodyNodeOrder_of_ordered {h : ℕ} {R : Type uR} {C : Type uC} [Preorder R] [Preorder C]
    (rowIndex : Position h → R) (colIndex : Position h → C)
    (hrowKey : ∀ v w : VariablePosition h,
      rowIndex (Sum.inr (Sum.inl v)) < rowIndex (Sum.inr (Sum.inl w)) →
        TreePositions.rowKey h v < TreePositions.rowKey h w)
    (hcolKey : ∀ v w : VariablePosition h,
      colIndex (Sum.inr (Sum.inl v)) < colIndex (Sum.inr (Sum.inl w)) →
        TreePositions.columnKey h v < TreePositions.columnKey h w)
    {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 r₀ < rowIndex r₁) (hcol : colIndex c₀ < colIndex c₁) :
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.VariablePosition, OAI.Problem348.TreePositions.rowKey, OAI.Problem348.TreePositions.columnKey, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole

theorem OAI.Problem348.Construction.host_ordered_body_leaf_diagonal line 120

Source documentation

The concrete host localization conclusion, with the numerical mode-order certificate discharged by the constructed key orders and increasing coordinates.

theorem host_ordered_body_leaf_diagonal {h : ℕ} {R : Type uR} {C : Type uC}
    [Preorder R] [Preorder C]
    (rowIndex : Position h → R) (colIndex : Position h → C)
    (hrowKey : ∀ v w : VariablePosition h,
      rowIndex (Sum.inr (Sum.inl v)) < rowIndex (Sum.inr (Sum.inl w)) →
        TreePositions.rowKey h v < TreePositions.rowKey h w)
    (hcolKey : ∀ v w : VariablePosition h,
      colIndex (Sum.inr (Sum.inl v)) < colIndex (Sum.inr (Sum.inl w)) →
        TreePositions.columnKey h v < TreePositions.columnKey h w)
    {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₁)
…