AnchorRigidity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite combinatorial anchor rigidity under explicit density, sparsity, and mode-incidence hypotheses.

theorem OAI.Problem348.AnchorRigidity.card_le_true_card_add_one line 15

Source documentation

At most one zero leaves all but at most one position equal to one.

theorem card_le_true_card_add_one {I : Type uI} [DecidableEq I]
    (s : Finset I) (f : I → Bool)
    (hz : (s.filter fun i => f i = false).card ≤ 1) :
    s.card ≤ (s.filter fun i => f i = true).card + 1 := by
…

theorem OAI.Problem348.AnchorRigidity.exists_common_true line 27

Source documentation

Two columns with at most one zero share a one on any core of size at least three.

theorem exists_common_true {I : Type uI} [DecidableEq I]
    (s : Finset I) (f g : I → Bool) (hs : 3 ≤ s.card)
    (hf : (s.filter fun i => f i = false).card ≤ 1)
    (hg : (s.filter fun i => g i = false).card ≤ 1) :
    ∃ i ∈ s, f i = true ∧ g i = true := by
…

theorem OAI.Problem348.AnchorRigidity.one_sided line 50

Source documentation

One-sided rigidity. A dense anchor core on the row axis forces both axes into one mode. The dummy predicate is only needed to permit one exceptional non-anchor column before the common mode has been identified.

theorem one_sided
    {I : Type uI} {J : Type uJ} {T : Type uT} [Fintype I] [Fintype J]
    (B : I → J → Bool) (rowMode : I → Option T) (colMode : J → Option T)
    (dummyCol : J → Prop) (core : Finset I)
    (hcore : 6 ≤ core.card)
    (core_anchor : ∀ i ∈ core, ∃ t, rowMode i = some t)
    (core_zeros : ∀ j, (core.filter fun i => B i j = false).card ≤ 1)
    (variable_sparse : ∀ j, colMode j = none → ¬ dummyCol j →
      (core.filter fun i => B i j = true).card ≤ 4)
    (dummy_unique : ∀ j k, dummyCol j → dummyCol k → j = k)
    (cross_mode : ∀ i j t u, rowMode i = some t → colMode j = some u →
      B i j = true → t = u)
…

def OAI.Problem348.AnchorRigidity.DenseAnchorCore line 133
Source documentation
A dense core consists of at least six selected anchor positions. Every opposite position has at most one zero on it, while a variable opposite position would have at most four ones.
```
def DenseAnchorCore {I : Type uI} {J : Type uJ} {T : Type uT}
    (B : I → J → Bool) (rowMode : I → Option T) (colMode : J → Option T)
    (dummyCol : J → Prop) : Prop :=
…
```

theorem OAI.Problem348.AnchorRigidity.rigidity line 145

Source documentation

Symmetric form of anchor rigidity: a dense anchor core on either axis suffices. The no-shattering/order argument supplies this disjunction in the application to the 64 by 64 pattern.

theorem rigidity
    {I : Type uI} {J : Type uJ} {T : Type uT} [Fintype I] [Fintype J]
    (B : I → J → Bool) (rowMode : I → Option T) (colMode : J → Option T)
    (dummyRow : I → Prop) (dummyCol : J → Prop)
    (hcore : DenseAnchorCore B rowMode colMode dummyCol ∨
      DenseAnchorCore (fun j i => B i j) colMode rowMode dummyRow)
    (dummy_row_unique : ∀ i k, dummyRow i → dummyRow k → i = k)
    (dummy_col_unique : ∀ j k, dummyCol j → dummyCol k → j = k)
    (cross_mode : ∀ i j t u, rowMode i = some t → colMode j = some u →
      B i j = true → t = u)
    (nonanchor_row_unit : ∀ i, rowMode i = none → ∀ j k t,
      colMode j = some t → colMode k = some t →
…

Mentions: OAI.Problem348.AnchorRigidity.DenseAnchorCore