OrderedHost.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The canonical host with both full-axis orders

The raw host, variable depth-first orders, and anchor/dummy order extension give two orders. They are not global instances on the same carrier. Their increasing enumerations are independent equivalences to the matrix size.

abbrev OAI.Problem348.OrderedHost.size line 21
abbrev OAI.Problem348.OrderedHost.rowOrder line 24
Source documentation
Rows: anchors first, then the minus/subtree/plus tree order, then dummy.
```
abbrev rowOrder (h : ℕ) : LinearOrder (Position h) := by
…
```
abbrev OAI.Problem348.OrderedHost.columnOrder line 29
Source documentation
Columns: anchors first, then dummy, then the plus/subtree/minus tree order.
```
abbrev columnOrder (h : ℕ) : LinearOrder (Position h) := by
…
```
def OAI.Problem348.OrderedHost.rowIndex line 34
Source documentation
The increasing row enumeration, from raw positions to actual indices.
```
def rowIndex (h : ℕ) : Position h ≃ Fin (size h) := by
…
```
Mentions: OAI.Problem348.OrderedHost.size
def OAI.Problem348.OrderedHost.columnIndex line 39
Source documentation
The increasing column enumeration, independent of the row enumeration.
```
def columnIndex (h : ℕ) : Position h ≃ Fin (size h) := by
…
```
Mentions: OAI.Problem348.OrderedHost.size
theorem OAI.Problem348.OrderedHost.rowIndex_lt_iff line 43
theorem OAI.Problem348.OrderedHost.columnIndex_lt_iff line 50
theorem OAI.Problem348.OrderedHost.rowIndex_variable_lt_iff line 58
Source documentation
On variable positions the full row enumeration has exactly the tree-key order.
```
theorem rowIndex_variable_lt_iff {h : ℕ} (v w : VariablePosition h) :
    rowIndex h (Sum.inr (Sum.inl v)) < rowIndex h (Sum.inr (Sum.inl w)) ↔
      TreePositions.rowKey h v < TreePositions.rowKey h w := by
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.TreePositions.rowKey
theorem OAI.Problem348.OrderedHost.columnIndex_variable_lt_iff line 66
Source documentation
On variable positions the full column enumeration has exactly the tree-key order.
```
theorem columnIndex_variable_lt_iff {h : ℕ} (v w : VariablePosition h) :
    columnIndex h (Sum.inr (Sum.inl v)) < columnIndex h (Sum.inr (Sum.inl w)) ↔
      TreePositions.columnKey h v < TreePositions.columnKey h w := by
…
```
Mentions: OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.TreePositions.columnKey
theorem OAI.Problem348.OrderedHost.row_anchor_strictMono line 74
Source documentation
Any representatives of the 64 successive anchor groups are increasing rows.
```
theorem row_anchor_strictMono {h : ℕ} (t : Mode h)
    (a : Fin 64 → Fin (2 ^ h)) :
    StrictMono (fun u => rowIndex h (Sum.inl (t, u, a u))) := by
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex
theorem OAI.Problem348.OrderedHost.column_anchor_strictMono line 84
Source documentation
The analogous anchor representatives are increasing columns.
```
theorem column_anchor_strictMono {h : ℕ} (t : Mode h)
    (a : Fin 64 → Fin (2 ^ h)) :
    StrictMono (fun u => columnIndex h (Sum.inl (t, u, a u))) := by
…
```
Mentions: OAI.Problem348.OrderedHost.columnIndex
theorem OAI.Problem348.OrderedHost.row_anchor_lt_nonanchor line 93
theorem OAI.Problem348.OrderedHost.column_anchor_lt_nonanchor line 101
theorem OAI.Problem348.OrderedHost.row_variable_lt_dummy line 109
theorem OAI.Problem348.OrderedHost.column_dummy_lt_variable line 115
theorem OAI.Problem348.OrderedHost.row_anchor_initial line 122
Source documentation
Initial-segment property for anchors, stated without an extra host predicate.
```
theorem row_anchor_initial {h : ℕ} {r s : Position h}
    (hrs : rowIndex h r < rowIndex h s) (hs : ∃ a, s = Sum.inl a) :
    ∃ a, r = Sum.inl a := by
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex
theorem OAI.Problem348.OrderedHost.column_anchor_initial line 130

theorem OAI.Problem348.OrderedHost.row_plus_child_lt_parent line 139

Source documentation

First tree-order equivalence, now for the actual row indices.

theorem row_plus_child_lt_parent {h i : ℕ} (hi : i < h) (x y : Fin (2 ^ h)) :
    rowIndex h (.inr (.inl (TreePositions.plusPos (i + 1) (by omega) x))) <
      rowIndex h (.inr (.inl (TreePositions.plusPos i (by omega) y))) ↔
      TreePositions.node (i + 1) x / 2 ≤ TreePositions.node i y := by
…

Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.TreePositions.plusPos, OAI.Problem348.TreePositions.node

theorem OAI.Problem348.OrderedHost.row_minus_parent_lt_child line 147

Source documentation

Second tree-order equivalence, now for the actual row indices.

theorem row_minus_parent_lt_child {h i : ℕ} (hi : i < h) (x y : Fin (2 ^ h)) :
    rowIndex h (.inr (.inl (TreePositions.minusPos i (by omega) y))) <
      rowIndex h (.inr (.inl (TreePositions.minusPos (i + 1) (by omega) x))) ↔
      TreePositions.node i y ≤ TreePositions.node (i + 1) x / 2 := by
…

Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.TreePositions.minusPos, OAI.Problem348.TreePositions.node

theorem OAI.Problem348.OrderedHost.column_plus_parent_lt_child line 155

Source documentation

Third tree-order equivalence, now for the actual column indices.

theorem column_plus_parent_lt_child {h i : ℕ} (hi : i < h) (x y : Fin (2 ^ h)) :
    columnIndex h (.inr (.inl (TreePositions.plusPos i (by omega) y))) <
      columnIndex h (.inr (.inl (TreePositions.plusPos (i + 1) (by omega) x))) ↔
      TreePositions.node i y ≤ TreePositions.node (i + 1) x / 2 := by
…

Mentions: OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.TreePositions.plusPos, OAI.Problem348.TreePositions.node

theorem OAI.Problem348.OrderedHost.column_minus_child_lt_parent line 163

Source documentation

Fourth tree-order equivalence, now for the actual column indices.

theorem column_minus_child_lt_parent {h i : ℕ} (hi : i < h) (x y : Fin (2 ^ h)) :
    columnIndex h (.inr (.inl (TreePositions.minusPos (i + 1) (by omega) x))) <
      columnIndex h (.inr (.inl (TreePositions.minusPos i (by omega) y))) ↔
      TreePositions.node (i + 1) x / 2 ≤ TreePositions.node i y := by
…

Mentions: OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.TreePositions.minusPos, OAI.Problem348.TreePositions.node