HostAnchorFrames.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Concrete selected-anchor frames for the canonical host. The frame signatures follow from the actual host entry definition.

theorem OAI.Problem348.Construction.host_row_role_zero line 16
Source documentation
A true first row role gives the exact first unit signature.
```
theorem host_row_role_zero {h : ℕ} (t : Mode h) (r : Position h)
    (hr : rowRole t 0 r) (v : Fin 64) (y : Fin (2 ^ h)) :
    host r (.inl (t,v,y)) = decide (v.val = 0) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_row_role_one line 25
Source documentation
A true second row role gives the exact second unit signature.
```
theorem host_row_role_one {h : ℕ} (t : Mode h) (r : Position h)
    (hr : rowRole t 1 r) (v : Fin 64) (y : Fin (2 ^ h)) :
    host r (.inl (t,v,y)) = decide (v.val = 1) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_col_role_zero line 34
Source documentation
A true first column role gives the exact first unit signature.
```
theorem host_col_role_zero {h : ℕ} (t : Mode h) (c : Position h)
    (hc : colRole t 0 c) (u : Fin 64) (x : Fin (2 ^ h)) :
    host (.inl (t,u,x)) c = decide (u.val = 0) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_col_role_one line 43
Source documentation
A true second column role gives the exact second unit signature.
```
theorem host_col_role_one {h : ℕ} (t : Mode h) (c : Position h)
    (hc : colRole t 1 c) (u : Fin 64) (x : Fin (2 ^ h)) :
    host (.inl (t,u,x)) c = decide (u.val = 1) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.host
def OAI.Problem348.Construction.SelectedAnchor.matrix line 54
Source documentation
Independent reindexings of the exact canonical raw host.
```
def matrix {h n : ℕ} (er ec : Position h ≃ Fin n) : BinaryMatrix n :=
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.BinaryMatrix
theorem OAI.Problem348.Construction.SelectedAnchor.matrix_apply line 57
def OAI.Problem348.Construction.SelectedAnchor.frame line 62
Source documentation
One selected representative from each anchor group of a fixed mode.
```
def frame {h n : ℕ} (er ec : Position h ≃ Fin n) (t : Mode h)
    (a b : Fin 64 → Fin (2 ^ h))
    (hr : StrictMono (fun u => er (.inl (t,u,a u))))
    (hc : StrictMono (fun v => ec (.inl (t,v,b v)))) :
    GuardedPath.AnchorFrame n where
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.GuardedPath.AnchorFrame

theorem OAI.Problem348.Construction.SelectedAnchor.frame_valid line 72

Source documentation

The actual host roles and the row/column order comparisons give a valid selected frame. No body entry is required or constrained.

theorem frame_valid {h n : ℕ} (er ec : Position h ≃ Fin n) (t : Mode h)
    (a b : Fin 64 → Fin (2 ^ h))
    (hr : StrictMono (fun u => er (.inl (t,u,a u))))
    (hc : StrictMono (fun v => ec (.inl (t,v,b v))))
    (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₁)
    (hbeforeR : ∀ u, er (.inl (t,u,a u)) < er r₀)
    (hrows : er r₀ < er r₁)
    (hbeforeC : ∀ v, ec (.inl (t,v,b v)) < ec c₀)
    (hcols : ec c₀ < ec c₁) :
    (frame er ec t a b hr hc).Valid (matrix er ec)
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.colRole, OAI.Problem348.Construction.SelectedAnchor.frame, OAI.Problem348.Construction.SelectedAnchor.matrix