HostAnchorRigidity.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Concrete cross-mode and single-mode incidence facts for the canonical host. These discharge the corresponding premises of abstract anchor rigidity once an anchor copy has distinct selected anchor groups.

def OAI.Problem348.AnchorRigidity.positionMode line 20

Source documentation

The mode label of a raw anchor position, and none off the anchors.

def positionMode {h : ℕ} : Position h → Option (Mode h)
  | Sum.inl (t, _, _) => some t
  | Sum.inr _ => none

/-- Group label, ignoring the within-group coordinate. -/

def OAI.Problem348.AnchorRigidity.positionGroup line 25

Source documentation

Group label, ignoring the within-group coordinate.

def positionGroup {h : ℕ} : Position h → Option (Mode h × Fin 64)
  | Sum.inl (t, u, _) => some (t, u)
  | Sum.inr _ => none

/-- A selected family uses each anchor group at most once. -/

def OAI.Problem348.AnchorRigidity.DistinctAnchorGroups line 30
Source documentation
A selected family uses each anchor group at most once.
```
def DistinctAnchorGroups {h : ℕ} {I : Type uI} (r : I → Position h) : Prop :=
…
```
theorem OAI.Problem348.AnchorRigidity.host_cross_mode line 34
Source documentation
A true entry between anchors forces their modes to agree.
```
theorem host_cross_mode {h : ℕ} (r c : Position h) (t u : Mode h)
    (hr : positionMode r = some t) (hc : positionMode c = some u)
    (hb : host r c = true) : t = u := by
…
```
Mentions: OAI.Problem348.AnchorRigidity.positionMode

theorem OAI.Problem348.AnchorRigidity.host_nonanchor_row_one_group line 48

Source documentation

On the columns of one mode, a nonanchor row has ones in only one group.

theorem host_nonanchor_row_one_group {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
…

theorem OAI.Problem348.AnchorRigidity.host_nonanchor_col_one_group line 68

Source documentation

On the rows of one mode, a nonanchor column has ones in only one group.

theorem host_nonanchor_col_one_group {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
…

theorem OAI.Problem348.AnchorRigidity.host_nonanchor_row_unit line 88

Source documentation

Unit-incidence premise for a selected family of columns with no repeated group.

theorem host_nonanchor_row_unit {h : ℕ} {J : Type uJ}
    (r : Position h) (c : J → Position h) (hcgroup : DistinctAnchorGroups c)
    (hr : positionMode r = none) (j k : J) (t : Mode h)
    (hj : positionMode (c j) = some t) (hk : positionMode (c k) = some t)
    (hbj : host r (c j) = true) (hbk : host r (c k) = true) : j = k := by
…

Mentions: OAI.Problem348.AnchorRigidity.DistinctAnchorGroups, OAI.Problem348.AnchorRigidity.positionMode

theorem OAI.Problem348.AnchorRigidity.host_nonanchor_col_unit line 110

Source documentation

Unit-incidence premise for a selected family of rows with no repeated group.

theorem host_nonanchor_col_unit {h : ℕ} {I : Type uI}
    (r : I → Position h) (c : Position h) (hrgroup : DistinctAnchorGroups r)
    (hc : positionMode c = none) (i k : I) (t : Mode h)
    (hi : positionMode (r i) = some t) (hk : positionMode (r k) = some t)
    (hbi : host (r i) c = true) (hbk : host (r k) c = true) : i = k := by
…

Mentions: OAI.Problem348.AnchorRigidity.DistinctAnchorGroups, OAI.Problem348.AnchorRigidity.positionMode

def OAI.Problem348.HostAnchorRigidity.modeLabel line 147

Source documentation

The mode label of an anchor, and none for a non-anchor.

def modeLabel {h : ℕ} : Position h → Option (Mode h)
  | Sum.inl (t, _, _) => some t
  | Sum.inr _ => none

/-- The actual dummy positions on either raw axis. -/

def OAI.Problem348.HostAnchorRigidity.Dummy line 152
Source documentation
The actual dummy positions on either raw axis.
```
def Dummy {h : ℕ} (x : Position h) : Prop :=
…
```
theorem OAI.Problem348.HostAnchorRigidity.exists_anchor_of_mode line 155
theorem OAI.Problem348.HostAnchorRigidity.exists_nonanchor_of_mode_none line 164
theorem OAI.Problem348.HostAnchorRigidity.exists_dummy_of_dummy line 171

theorem OAI.Problem348.HostAnchorRigidity.selected_anchor_rows_unique line 175

Source documentation

Distinct selected anchor rows cannot have the same mode and group.

theorem selected_anchor_rows_unique {h : ℕ}
    (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    {i k : Fin 64} {t : Mode h} {u : Fin 64} {x y : Fin (2 ^ h)}
    (hi : r i = Sum.inl (t, u, x))
    (hk : r k = Sum.inl (t, u, y)) : i = k := by
…

Mentions: OAI.Problem348.anchor64

theorem OAI.Problem348.HostAnchorRigidity.selected_anchor_columns_unique line 187

Source documentation

Distinct selected anchor columns cannot have the same mode and group.

theorem selected_anchor_columns_unique {h : ℕ}
    (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    {j k : Fin 64} {t : Mode h} {v : Fin 64} {x y : Fin (2 ^ h)}
    (hj : c j = Sum.inl (t, v, x))
    (hk : c k = Sum.inl (t, v, y)) : j = k := by
…

Mentions: OAI.Problem348.anchor64

theorem OAI.Problem348.HostAnchorRigidity.selected_dummy_rows_unique line 200
Source documentation
At most one selected row can be dummy, because all dummy rows are twins.
```
theorem selected_dummy_rows_unique {h : ℕ}
    (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    {i k : Fin 64} (hi : Dummy (r i)) (hk : Dummy (r k)) : i = k := by
…
```
Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.Dummy

theorem OAI.Problem348.HostAnchorRigidity.selected_dummy_columns_unique line 212

Source documentation

At most one selected column can be dummy.

theorem selected_dummy_columns_unique {h : ℕ}
    (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    {j k : Fin 64} (hj : Dummy (c j)) (hk : Dummy (c k)) : j = k := by
…

Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.Dummy

theorem OAI.Problem348.HostAnchorRigidity.selected_cross_mode line 225

Source documentation

A one between two anchors forces their modes to coincide.

theorem selected_cross_mode {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (i j : Fin 64) (t u : Mode h)
    (hi : modeLabel (r i) = some t) (hj : modeLabel (c j) = some u)
    (hij : anchor64 i j = true) : t = u := by
…

Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.modeLabel

theorem OAI.Problem348.HostAnchorRigidity.selected_nonanchor_row_unit line 237

Source documentation

On the selected anchors of a fixed mode a non-anchor row has at most one one.

theorem selected_nonanchor_row_unit {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (i : Fin 64) (hi : modeLabel (r i) = none) (j k : Fin 64) (t : Mode h)
    (hj : modeLabel (c j) = some t) (hk : modeLabel (c k) = some t)
    (hij : anchor64 i j = true) (hik : anchor64 i k = true) : j = k := by
…

Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.modeLabel

theorem OAI.Problem348.HostAnchorRigidity.selected_nonanchor_column_unit line 252

Source documentation

On the selected anchors of a fixed mode a non-anchor column has at most one one.

theorem selected_nonanchor_column_unit {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (j : Fin 64) (hj : modeLabel (c j) = none) (i k : Fin 64) (t : Mode h)
    (hi : modeLabel (r i) = some t) (hk : modeLabel (r k) = some t)
    (hij : anchor64 i j = true) (hkj : anchor64 k j = true) : i = k := by
…

Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.modeLabel

theorem OAI.Problem348.HostAnchorRigidity.mode_constant_of_dense_core line 268

Source documentation

Concrete host rigidity assuming a dense core, with twin, signature, density, and cross-mode properties following from the host entries.

theorem mode_constant_of_dense_core {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (hcore :
      AnchorRigidity.DenseAnchorCore anchor64 (modeLabel ∘ r) (modeLabel ∘ c) (Dummy ∘ c) ∨
      AnchorRigidity.DenseAnchorCore (fun j i => anchor64 i j)
        (modeLabel ∘ c) (modeLabel ∘ r) (Dummy ∘ r)) :
    ∃ t : Mode h, (∀ i, modeLabel (r i) = some t) ∧
      (∀ j, modeLabel (c j) = some t) := by
…

Mentions: OAI.Problem348.anchor64, OAI.Problem348.AnchorRigidity.DenseAnchorCore, OAI.Problem348.HostAnchorRigidity.modeLabel, OAI.Problem348.HostAnchorRigidity.Dummy