OrderedAnchorGroups.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Prescribed anchor coordinates in the actual ordered host

The independent enumerations satisfy OrderedHost.row_anchor_strictMono and column_anchor_strictMono, giving the order premises of one-mode group exhaustion without a default order instance on the raw Position sum type.

theorem OAI.Problem348.OrderedHost.group_le_of_ordered_representatives line 20
theorem OAI.Problem348.OrderedHost.row_anchor_group_le line 33
Source documentation
Increasing rows in one mode have nondecreasing anchor group indices.
```
theorem row_anchor_group_le {h : ℕ} (t : Mode h) (u v : Fin 64)
    (x y : Fin (2 ^ h))
    (hxy : rowIndex h (Sum.inl (t,u,x)) < rowIndex h (Sum.inl (t,v,y))) :
    u ≤ v :=
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex
theorem OAI.Problem348.OrderedHost.column_anchor_group_le line 42
Source documentation
The analogous group-order implication for the actual column enumeration.
```
theorem column_anchor_group_le {h : ℕ} (t : Mode h) (u v : Fin 64)
    (x y : Fin (2 ^ h))
    (hxy : columnIndex h (Sum.inl (t,u,x)) < columnIndex h (Sum.inl (t,v,y))) :
    u ≤ v :=
…
```
Mentions: OAI.Problem348.OrderedHost.columnIndex

theorem OAI.Problem348.OrderedHost.anchor_representatives_of_one_mode line 53

Source documentation

Mode rigidity locates the prefix in one mode, forcing its exact group coordinates in the concrete ordered host. No additional group, twin, density, or order hypotheses are required.

theorem anchor_representatives_of_one_mode {h : ℕ}
    (r c : Fin 64 → Position h) (t : Mode h)
    (hr : StrictMono (fun i => rowIndex h (r i)))
    (hc : StrictMono (fun j => columnIndex h (c j)))
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (hrowmode : ∀ i, ∃ u x, r i = Sum.inl (t,u,x))
    (hcolmode : ∀ j, ∃ v y, c j = Sum.inl (t,v,y)) :
    ∃ x y : Fin 64 → Fin (2 ^ h),
      (∀ i, r i = Sum.inl (t,i,x i)) ∧ (∀ j, c j = Sum.inl (t,j,y j)) := by
…

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