HostAnchorPinning.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the exact anchor-majority and concrete-host rigidity steps.

theorem OAI.Problem348.HostAnchorRigidity.selected_columns_injective line 14
Source documentation
An exact anchor copy is automatically injective on the column axis.
```
theorem selected_columns_injective {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j) : Function.Injective c := by
…
```
Mentions: OAI.Problem348.anchor64
theorem OAI.Problem348.HostAnchorRigidity.selected_rows_injective line 23
Source documentation
An exact anchor copy is automatically injective on the row axis.
```
theorem selected_rows_injective {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j) : Function.Injective r := by
…
```
Mentions: OAI.Problem348.anchor64
def OAI.Problem348.HostAnchorRigidity.ColumnSparse line 31
Source documentation
Variable-column sparseness on a selected prefix.
```
def ColumnSparse {h : ℕ} (r c : Fin 64 → Position h) : Prop :=
…
```
def OAI.Problem348.HostAnchorRigidity.RowSparse line 37
Source documentation
Variable-row sparseness on a selected prefix.
```
def RowSparse {h : ℕ} (r c : Fin 64 → Position h) : Prop :=
…
```

theorem OAI.Problem348.HostAnchorRigidity.mode_constant_of_prefix line 43

Source documentation

Prefix anchoring plus actual variable sparseness pins all positions to one mode.

theorem mode_constant_of_prefix {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (hprefix : (∀ i : Fin 64, i.val < 32 → ∃ t, modeLabel (r i) = some t) ∨
      (∀ j : Fin 64, j.val < 32 → ∃ t, modeLabel (c j) = some t))
    (hcs : ColumnSparse r c) (hrs : RowSparse r c) :
    ∃ t : Mode h, (∀ i, modeLabel (r i) = some t) ∧
      (∀ j, modeLabel (c j) = some t) := by
…

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

theorem OAI.Problem348.HostAnchorRigidity.mode_constant_of_no_shattering line 62

Source documentation

No five-column shattering and the anchor-before-nonanchor order give a majority; prefix rigidity then yields one common mode.

theorem mode_constant_of_no_shattering {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (row_initial : ∀ i j, i ≤ j → modeLabel (r j) ≠ none → modeLabel (r i) ≠ none)
    (col_initial : ∀ i j, i ≤ j → modeLabel (c j) ≠ none → modeLabel (c i) ≠ none)
    (hnoshatter : ∀ cs : Fin 5 → Position h, Function.Injective cs →
      (∀ b, modeLabel (cs b) = none) → ∃ w : Fin 5 → Bool,
        ∀ x, modeLabel x = none → ∃ b, host x (cs b) ≠ w b)
    (hcs : ColumnSparse r c) (hrs : RowSparse r c) :
    ∃ t : Mode h, (∀ i, modeLabel (r i) = some t) ∧
      (∀ j, modeLabel (c j) = some t) := by
…

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

def OAI.Problem348.HostAnchorRigidity.GroupsMonotone line 89
Source documentation
The within-mode group order enjoyed by an increasingly selected axis.
```
def GroupsMonotone {h : ℕ} (r : Fin 64 → Position h) : Prop :=
…
```

theorem OAI.Problem348.HostAnchorRigidity.representatives_of_mode_constant line 96

Source documentation

Once one common mode is known, group uniqueness and the actual group order identify its representatives in the exact pattern order.

theorem representatives_of_mode_constant {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (hrow : GroupsMonotone r) (hcol : GroupsMonotone c)
    {t : Mode h} (hmr : ∀ i, modeLabel (r i) = some t)
    (hmc : ∀ j, modeLabel (c j) = some t) :
    ∃ a b : Fin 64 → Fin (2 ^ h),
      (∀ i, r i = Sum.inl (t, i, a i)) ∧
      (∀ j, c j = Sum.inl (t, j, b j)) := by
…

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

theorem OAI.Problem348.HostAnchorRigidity.representatives_of_no_shattering line 137

Source documentation

Full anchor representative conclusion assuming initial anchor segments, nonshattering, variable sparseness, and within-mode group order.

theorem representatives_of_no_shattering {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (row_initial : ∀ i j, i ≤ j → modeLabel (r j) ≠ none → modeLabel (r i) ≠ none)
    (col_initial : ∀ i j, i ≤ j → modeLabel (c j) ≠ none → modeLabel (c i) ≠ none)
    (hnoshatter : ∀ cs : Fin 5 → Position h, Function.Injective cs →
      (∀ b, modeLabel (cs b) = none) → ∃ w : Fin 5 → Bool,
        ∀ x, modeLabel x = none → ∃ b, host x (cs b) ≠ w b)
    (hcs : ColumnSparse r c) (hrs : RowSparse r c)
    (hrow : GroupsMonotone r) (hcol : GroupsMonotone c) :
    ∃ (t : Mode h) (a b : Fin 64 → Fin (2 ^ h)),
      (∀ i, r i = Sum.inl (t, i, a i)) ∧
      (∀ j, c j = Sum.inl (t, j, b j)) := by
…

Mentions: OAI.Problem348.anchor64, OAI.Problem348.HostAnchorRigidity.modeLabel, OAI.Problem348.HostAnchorRigidity.ColumnSparse, OAI.Problem348.HostAnchorRigidity.RowSparse, OAI.Problem348.HostAnchorRigidity.GroupsMonotone

theorem OAI.Problem348.HostAnchorRigidity.actual_nonshattering line 156
Source documentation
The concrete canonical host supplies the missing-word hypothesis, without any ordering or injectivity condition on the five columns.
```
theorem actual_nonshattering {h : ℕ} (cs : Fin 5 → Position h)
    (hcs : ∀ b, modeLabel (cs b) = none) :
    ∃ w : Fin 5 → Bool, ∀ x, modeLabel x = none →
      ∃ b, host x (cs b) ≠ w b := by
…
```
Mentions: OAI.Problem348.HostAnchorRigidity.modeLabel

theorem OAI.Problem348.HostAnchorRigidity.representatives_of_sparse line 172

Source documentation

Concrete-host anchor pinning assuming axis-order and sparse-core conditions; nonshattering follows from the host entries.

theorem representatives_of_sparse {h : ℕ} (r c : Fin 64 → Position h)
    (hcopy : ∀ i j, host (r i) (c j) = anchor64 i j)
    (row_initial : ∀ i j, i ≤ j → modeLabel (r j) ≠ none → modeLabel (r i) ≠ none)
    (col_initial : ∀ i j, i ≤ j → modeLabel (c j) ≠ none → modeLabel (c i) ≠ none)
    (hcs : ColumnSparse r c) (hrs : RowSparse r c)
    (hrow : GroupsMonotone r) (hcol : GroupsMonotone c) :
    ∃ (t : Mode h) (a b : Fin 64 → Fin (2 ^ h)),
      (∀ i, r i = Sum.inl (t, i, a i)) ∧
      (∀ j, c j = Sum.inl (t, j, b j)) := by
…