HostRoleExtraction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Body-role extraction for the canonical host

Anchor traces determine body roles in the actual Construction.host table.

theorem OAI.Problem348.Construction.rowRole_of_anchor_trace line 14
theorem OAI.Problem348.Construction.colRole_of_anchor_trace line 38
theorem OAI.Problem348.Construction.anchor_trace_of_rowRole line 63
Source documentation
Exact converse, useful also when constructing a guarded anchor frame.
```
theorem anchor_trace_of_rowRole {h : ℕ} (t : Mode h) (r : Position h)
    (z : Fin 64 → Fin (2 ^ h)) (b : Fin 2) (hr : rowRole t b r) :
    ∀ v : Fin 64, host r (Sum.inl (t, v, z v)) = decide (v.val = b.val) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.rowRole, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.anchor_trace_of_colRole line 79

theorem OAI.Problem348.Construction.host_body_roles_of_matching line 96

Source documentation

Raw matching version, independent of any enumeration or order on the axes.

theorem host_body_roles_of_matching {h : ℕ}
    (r c : Fin 66 → Position h)
    (hmatch : ∀ i j, host (r i) (c j) = fixedH i j)
    (t : Mode h) (zr zc : Fin 64 → Fin (2 ^ h))
    (hrows : ∀ u, r (BodySignatures52.anchorIndex u) = Sum.inl (t, u, zr u))
    (hcols : ∀ v, c (BodySignatures52.anchorIndex v) = Sum.inl (t, v, zc v))
    (b : Fin 2) :
    rowRole t b (r (BodySignatures52.bodyIndex b)) ∧
      colRole t b (c (BodySignatures52.bodyIndex b)) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host, OAI.Problem348.fixedH, OAI.Problem348.Construction.Mode, OAI.Problem348.BodySignatures52.anchorIndex, OAI.Problem348.Construction.rowRole, OAI.Problem348.BodySignatures52.bodyIndex, OAI.Problem348.Construction.colRole

theorem OAI.Problem348.Construction.host_body_entries_of_matching line 116

Source documentation

The lower-right four cells of any raw matching copy form exactly P.

theorem host_body_entries_of_matching {h : ℕ}
    (r c : Fin 66 → Position h)
    (hmatch : ∀ i j, host (r i) (c j) = fixedH i j) :
    host (r (BodySignatures52.bodyIndex 0)) (c (BodySignatures52.bodyIndex 0)) = true ∧
    host (r (BodySignatures52.bodyIndex 0)) (c (BodySignatures52.bodyIndex 1)) = false ∧
    host (r (BodySignatures52.bodyIndex 1)) (c (BodySignatures52.bodyIndex 0)) = true ∧
    host (r (BodySignatures52.bodyIndex 1)) (c (BodySignatures52.bodyIndex 1)) = true := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host, OAI.Problem348.fixedH, OAI.Problem348.BodySignatures52.bodyIndex

theorem OAI.Problem348.Construction.host_body_roles_of_copy line 128

Source documentation

An actual ordered copy in a transported canonical host has the two prescribed body roles, once anchor rigidity pins its prefix.

theorem host_body_roles_of_copy {h n : ℕ} {A : BinaryMatrix n}
    (row col : Fin n → Position h)
    (hA : ∀ i j, A i j = host (row i) (col j))
    {rc : IncreasingMap 66 n × IncreasingMap 66 n}
    (hcopy : rc ∈ orderedCopies fixedH A)
    (t : Mode h) (zr zc : Fin 64 → Fin (2 ^ h))
    (hrows : ∀ u, row (rc.1.val (BodySignatures52.anchorIndex u)) =
      Sum.inl (t, u, zr u))
    (hcols : ∀ v, col (rc.2.val (BodySignatures52.anchorIndex v)) =
      Sum.inl (t, v, zc v))
    (b : Fin 2) :
    rowRole t b (row (rc.1.val (BodySignatures52.bodyIndex b))) ∧
…

Mentions: OAI.Problem348.BinaryMatrix, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host, OAI.Problem348.IncreasingMap, OAI.Problem348.orderedCopies, OAI.Problem348.fixedH, OAI.Problem348.Construction.Mode, OAI.Problem348.BodySignatures52.anchorIndex, OAI.Problem348.Construction.rowRole, OAI.Problem348.BodySignatures52.bodyIndex