AnchorRigidityFixed.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem348.AnchorRigidity.firstCore line 11
Source documentation
The actual first 32 positions of the fixed anchor.
```
def firstCore : Finset (Fin 64) := Finset.univ.filter fun i => i.val < 32
```
theorem OAI.Problem348.AnchorRigidity.mem_firstCore line 13
theorem OAI.Problem348.AnchorRigidity.firstCore_card line 16
theorem OAI.Problem348.AnchorRigidity.firstCore_column_zeros line 18
theorem OAI.Problem348.AnchorRigidity.firstCore_row_zeros line 27

theorem OAI.Problem348.AnchorRigidity.prefix_of_majority line 39

Source documentation

A majority of anchor labels in an initial segment contains the dense prefix. This is the small order/cardinality bridge from the no-shattering majority argument to the finite rigidity theorem.

theorem prefix_of_majority {T : Type uT} (mode : Fin 64 → Option T)
    (initial : ∀ i j, i ≤ j → mode j ≠ none → mode i ≠ none)
    (majority : 32 < (Finset.univ.filter fun i => (mode i).isSome).card) :
    ∀ i : Fin 64, i.val < 32 → ∃ t, mode i = some t := by
…

theorem OAI.Problem348.AnchorRigidity.prefix_alternative_of_majority line 62

Source documentation

The majority conclusion on either axis provides the prefix alternative required by anchor64_rigidity_of_prefix.

theorem prefix_alternative_of_majority {T : Type uT}
    (rowMode colMode : Fin 64 → Option T)
    (row_initial : ∀ i j, i ≤ j → rowMode j ≠ none → rowMode i ≠ none)
    (col_initial : ∀ i j, i ≤ j → colMode j ≠ none → colMode i ≠ none)
    (majority : 32 < (Finset.univ.filter fun i => (rowMode i).isSome).card ∨
      32 < (Finset.univ.filter fun j => (colMode j).isSome).card) :
    (∀ i : Fin 64, i.val < 32 → ∃ t, rowMode i = some t) ∨
      (∀ j : Fin 64, j.val < 32 → ∃ t, colMode j = some t) := by
…

theorem OAI.Problem348.AnchorRigidity.anchor64_rigidity_of_prefix line 74

Source documentation

Same-mode conclusion for the exact anchor after prefix pinning.

theorem anchor64_rigidity_of_prefix {T : Type uT}
    (rowMode colMode : Fin 64 → Option T)
    (dummyRow dummyCol : Fin 64 → Prop)
    (hprefix : (∀ i : Fin 64, i.val < 32 → ∃ t, rowMode i = some t) ∨
      (∀ j : Fin 64, j.val < 32 → ∃ t, colMode j = some t))
    (variable_col_sparse : ∀ j, colMode j = none → ¬ dummyCol j →
      (∀ i ∈ firstCore, ∃ t, rowMode i = some t) →
      (firstCore.filter fun i => anchor64 i j = true).card ≤ 4)
    (variable_row_sparse : ∀ i, rowMode i = none → ¬ dummyRow i →
      (∀ j ∈ firstCore, ∃ t, colMode j = some t) →
      (firstCore.filter fun j => anchor64 i j = true).card ≤ 4)
    (dummy_row_unique : ∀ i k, dummyRow i → dummyRow k → i = k)
…

Mentions: OAI.Problem348.AnchorRigidity.firstCore, OAI.Problem348.anchor64