HostAnchorGroups.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Group coordinates of a canonical host anchor copy

One-mode anchor rigidity, the entries of Construction.host, and distinct rows and columns of anchor64 force exhaustion of the anchor groups. The two axes use independent key functions, with no global order instance on the raw carrier.

theorem OAI.Problem348.Construction.AnchorGroups.row_representatives line 22

Source documentation

The row groups of a one-mode anchor copy are exactly their pattern indices. Only the within-mode comparison property of the chosen row order is needed.

theorem row_representatives {h : ℕ} {K : Type uK} [LinearOrder K]
    (key : Position h → K) (r c : Fin 64 → Position h) (t : Mode h)
    (hr : StrictMono (fun i => key (r i)))
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (hmode : ∀ i, ∃ u x, r i = Sum.inl (t, u, x))
    (horder : ∀ u v : Fin 64, ∀ x y : Fin (2 ^ h),
      key (Sum.inl (t,u,x)) < key (Sum.inl (t,v,y)) → u ≤ v) :
    ∃ x : Fin 64 → Fin (2 ^ h), ∀ i, r i = Sum.inl (t,i,x i) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host, OAI.Problem348.anchor64

theorem OAI.Problem348.Construction.AnchorGroups.column_representatives line 50

Source documentation

The analogous conclusion for the independently ordered column axis.

theorem column_representatives {h : ℕ} {K : Type uK} [LinearOrder K]
    (key : Position h → K) (r c : Fin 64 → Position h) (t : Mode h)
    (hc : StrictMono (fun j => key (c j)))
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (hmode : ∀ j, ∃ v y, c j = Sum.inl (t, v, y))
    (horder : ∀ u v : Fin 64, ∀ x y : Fin (2 ^ h),
      key (Sum.inl (t,u,x)) < key (Sum.inl (t,v,y)) → u ≤ v) :
    ∃ y : Fin 64 → Fin (2 ^ h), ∀ j, c j = Sum.inl (t,j,y j) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host, OAI.Problem348.anchor64

theorem OAI.Problem348.Construction.AnchorGroups.representatives line 80

Source documentation

Both axes of the canonical anchor copy use every group in its prescribed order, with independent choices of the within-group offsets.

theorem representatives {h : ℕ} {KR : Type uKR} {KC : Type uKC}
    [LinearOrder KR] [LinearOrder KC]
    (rowKey : Position h → KR) (colKey : Position h → KC)
    (r c : Fin 64 → Position h) (t : Mode h)
    (hr : StrictMono (fun i => rowKey (r i)))
    (hc : StrictMono (fun j => colKey (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))
    (hroworder : ∀ u v : Fin 64, ∀ x y : Fin (2 ^ h),
      rowKey (Sum.inl (t,u,x)) < rowKey (Sum.inl (t,v,y)) → u ≤ v)
    (hcolorder : ∀ u v : Fin 64, ∀ x y : Fin (2 ^ h),
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host, OAI.Problem348.anchor64