HostTwins.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete twin-position facts for anchor rigidity in the flat-class host.

theorem OAI.Problem348.Construction.host_anchor_row_twin line 12
Source documentation
Changing the representative inside an anchor row group changes no entry.
```
theorem host_anchor_row_twin {h : ℕ} (t : Mode h) (u : Fin 64)
    (x y : Fin (2 ^ h)) (c : Position h) :
    host (Sum.inl (t,u,x)) c = host (Sum.inl (t,u,y)) c := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_anchor_column_twin line 18
Source documentation
Changing the representative inside an anchor column group changes no entry.
```
theorem host_anchor_column_twin {h : ℕ} (t : Mode h) (v : Fin 64)
    (x y : Fin (2 ^ h)) (r : Position h) :
    host r (Sum.inl (t,v,x)) = host r (Sum.inl (t,v,y)) := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_dummy_row_twin line 24
Source documentation
All dummy rows, including their anchor incidences, have equal signatures.
```
theorem host_dummy_row_twin {h : ℕ} (x y : Fin (2 ^ h)) (c : Position h) :
    host (Sum.inr (Sum.inr x)) c = host (Sum.inr (Sum.inr y)) c := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_dummy_column_twin line 29
Source documentation
All dummy columns, including their anchor incidences, have equal signatures.
```
theorem host_dummy_column_twin {h : ℕ} (x y : Fin (2 ^ h)) (r : Position h) :
    host r (Sum.inr (Sum.inr x)) = host r (Sum.inr (Sum.inr y)) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host
def OAI.Problem348.Construction.anchorGroup line 34
Source documentation
The anchor-group label forgets only the coordinate within a group.
```
def anchorGroup {h : ℕ} : Position h → Option (Mode h × Fin 64)
  | Sum.inl (t,u,_) => some (t,u)
  | Sum.inr _ => none

/-- A group-label equality is enough to prove that two full row signatures agree. -/
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode
theorem OAI.Problem348.Construction.host_rows_eq_of_anchorGroup line 39
Source documentation
A group-label equality is enough to prove that two full row signatures agree.
```
theorem host_rows_eq_of_anchorGroup {h : ℕ} {r r' : Position h}
    {t : Mode h} {u : Fin 64}
    (hr : anchorGroup r = some (t,u)) (hr' : anchorGroup r' = some (t,u)) :
    ∀ c, host r c = host r' c := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.anchorGroup, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_columns_eq_of_anchorGroup line 53
Source documentation
The same group-label criterion on the column axis.
```
theorem host_columns_eq_of_anchorGroup {h : ℕ} {c c' : Position h}
    {t : Mode h} {u : Fin 64}
    (hc : anchorGroup c = some (t,u)) (hc' : anchorGroup c' = some (t,u)) :
    ∀ r, host r c = host r c' := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.anchorGroup, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.mode_eq_of_host_anchor_true line 67
Source documentation
A true anchor--anchor entry forces the two modes to coincide.
```
theorem mode_eq_of_host_anchor_true {h : ℕ} {t t' : Mode h}
    {u v : Fin 64} {x y : Fin (2 ^ h)}
    (he : host (Sum.inl (t,u,x)) (Sum.inl (t',v,y)) = true) : t = t' := by
…
```
Mentions: OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.nonanchor_row_one_group_unique line 74
Source documentation
In any one mode a non-anchor row can be one in at most one anchor group.
```
theorem nonanchor_row_one_group_unique {h : ℕ}
    (r : VariablePosition h ⊕ Fin (2 ^ h)) (t : Mode h)
    (u v : Fin 64) (x y : Fin (2 ^ h))
    (hu : host (Sum.inr r) (Sum.inl (t,u,x)) = true)
    (hv : host (Sum.inr r) (Sum.inl (t,v,y)) = true) : u = v := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.nonanchor_column_one_group_unique line 93
Source documentation
In any one mode a non-anchor column can be one in at most one anchor group.
```
theorem nonanchor_column_one_group_unique {h : ℕ}
    (c : VariablePosition h ⊕ Fin (2 ^ h)) (t : Mode h)
    (u v : Fin 64) (x y : Fin (2 ^ h))
    (hu : host (Sum.inl (t,u,x)) (Sum.inr c) = true)
    (hv : host (Sum.inl (t,v,y)) (Sum.inr c) = true) : u = v := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.Mode, OAI.Problem348.Construction.host