OrderedAnchorRigidity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Anchor rigidity for the ordered canonical host

No-shattering, sparse anchor traces, twin classes, and the two independent axis orders determine all anchor representatives.

theorem OAI.Problem348.HostAnchorRigidity.modeLabel_eq_selectedMode line 16
theorem OAI.Problem348.HostAnchorRigidity.selected_rows_groupInjective line 20
theorem OAI.Problem348.HostAnchorRigidity.selected_columns_groupInjective line 31
theorem OAI.Problem348.HostAnchorRigidity.actual_columnSparse line 43
Source documentation
The sparse-column requirement follows from the actual host incidence bound.
```
theorem actual_columnSparse {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j) : ColumnSparse r c := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.ColumnSparse
theorem OAI.Problem348.HostAnchorRigidity.actual_rowSparse line 57
Source documentation
The transpose sparse-row requirement, with no assumptions left over.
```
theorem actual_rowSparse {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j) : RowSparse r c := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.RowSparse
theorem OAI.Problem348.HostAnchorRigidity.mode_nonempty_iff_anchor line 70
theorem OAI.Problem348.HostAnchorRigidity.row_initial_of_indices line 74
theorem OAI.Problem348.HostAnchorRigidity.col_initial_of_indices line 84
theorem OAI.Problem348.HostAnchorRigidity.representatives_of_indices line 97
Source documentation
Every ordered copy of the fixed 64-by-64 anchor in the canonical host uses precisely one mode, with its groups in the prescribed order. There are no sparsity, majority, nonshattering, twin, or abstract-order premises.
```
theorem representatives_of_indices {h : ℕ} (r c : Fin 64 → Position h)
    (hr : StrictMono (fun i => OrderedHost.rowIndex h (r i)))
    (hc : StrictMono (fun j => OrderedHost.columnIndex h (c j)))
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j) :
    ∃ (t : Mode h) (a b : Fin 64 → Fin (2 ^ h)),
      (∀ i, r i = Sum.inl (t,i,a i)) ∧
      (∀ j, c j = Sum.inl (t,j,b j)) := by
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex, OAI.Problem348.anchor64