DirectNonshattering.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A direct qualitative proof of the non-anchor trace obstruction. No enumeration of suffix generators is needed.

If all binary words occur, any two selected columns in the same class can be separated by a singleton word, contradicting their suffix monotonicity. Thus all five classes are distinct. The word 11110 then uses four classes, while a variable row uses at most three and a dummy row is all ones.

theorem OAI.Problem348.DirectNonshattering.class_injective_of_surjective line 22

Source documentation

A surjective family of class-monotone words separates the column classes.

theorem class_injective_of_surjective
    {R : Type uR} {C : Type uC} {K : Type uK} [DecidableEq C] [LinearOrder K]
    {L : Type uL} (classOf : C → L) (key : C → K) (A : R → C → Bool)
    (hmono : ∀ r i j, classOf i = classOf j → key i ≤ key j →
      A r i = true → A r j = true)
    (hsurj : Function.Surjective A) : Function.Injective classOf := by
…

theorem OAI.Problem348.DirectNonshattering.not_surjective_of_card line 44

Source documentation

General form: q + 2 columns cannot be shattered by classwise suffix rows supported on at most q classes, together with all-one rows.

theorem not_surjective_of_card
    {R : Type uR} {C : Type uC} {L : Type uL} {K : Type uK} [Fintype C] [DecidableEq C] [DecidableEq L]
    [LinearOrder K] (q : ℕ) (hcard : q + 2 ≤ Fintype.card C)
    (classOf : C → L) (key : C → K) (A : R → C → Bool)
    (hmono : ∀ r i j, classOf i = classOf j → key i ≤ key j →
      A r i = true → A r j = true)
    (hsupport : ∀ r,
      ((univ.filter (fun i => A r i = true)).image classOf).card ≤ q ∨
      (∀ i, A r i = true)) :
    ¬ Function.Surjective A := by
…

theorem OAI.Problem348.DirectNonshattering.not_surjective_five line 75

Source documentation

No family with suffixes in at most three classes, plus all-one rows, realizes every binary word on five columns.

theorem not_surjective_five
    {R : Type uR} {L : Type uL} {K : Type uK} [DecidableEq L] [LinearOrder K]
    (classOf : Fin 5 → L) (key : Fin 5 → K) (A : R → Fin 5 → Bool)
    (hmono : ∀ r i j, classOf i = classOf j → key i ≤ key j →
      A r i = true → A r j = true)
    (hsupport : ∀ r,
      ((univ.filter (fun i => A r i = true)).image classOf).card ≤ 3 ∨
      (∀ i, A r i = true)) :
    ¬ Function.Surjective A :=
…

theorem OAI.Problem348.DirectNonshattering.exists_missing_word line 87

Source documentation

The conclusion in a form convenient for a five-column shattering test.

theorem exists_missing_word
    {R : Type uR} {L : Type uL} {K : Type uK} [DecidableEq L] [LinearOrder K]
    (classOf : Fin 5 → L) (key : Fin 5 → K) (A : R → Fin 5 → Bool)
    (hmono : ∀ r i j, classOf i = classOf j → key i ≤ key j →
      A r i = true → A r j = true)
    (hsupport : ∀ r,
      ((univ.filter (fun i => A r i = true)).image classOf).card ≤ 3 ∨
      (∀ i, A r i = true)) :
    ∃ w : Fin 5 → Bool, ∀ r, A r ≠ w := by
…

theorem OAI.Problem348.DirectNonshattering.not_surjective_of_constant_column line 100
Source documentation
A column equal to one in every row also rules out shattering immediately.
```
theorem not_surjective_of_constant_column
    {R : Type uR} {C : Type uC} (A : R → C → Bool) (j : C)
    (hj : ∀ r, A r j = true) : ¬ Function.Surjective A := by
…
```

theorem OAI.Problem348.DirectNonshattering.not_surjective_selected_columns line 112

Source documentation

Whole-host version. Dummy columns are all ones, and every non-dummy row has at most three active classes among the non-dummy columns. The chosen five columns need not be ordered or even assumed distinct.

theorem not_surjective_selected_columns
    {R : Type uR} {C : Type uC} {L : Type uL} {K : Type uK} [Fintype C] [DecidableEq C] [DecidableEq L]
    [LinearOrder K]
    (A : R → C → Bool) (dummyRow : R → Prop) (dummyColumn : C → Prop)
    [DecidablePred dummyColumn]
    (classOf : C → L) (key : C → K)
    (hrow : ∀ r, dummyRow r → ∀ c, A r c = true)
    (hcolumn : ∀ c, dummyColumn c → ∀ r, A r c = true)
    (hmono : ∀ r, ¬ dummyRow r → ∀ c d,
      ¬ dummyColumn c → ¬ dummyColumn d → classOf c = classOf d →
      key c ≤ key d → A r c = true → A r d = true)
    (hsupport : ∀ r, ¬ dummyRow r →
…

theorem OAI.Problem348.DirectNonshattering.exists_missing_word_with_zero line 158

Source documentation

On k+2 coordinates, classwise monotone traces with at most k active classes, allowing also the constant-one trace, omit a Boolean word. The rank need not be injective within a class.

theorem exists_missing_word_with_zero {ρ : Type uRho} {β : Type uBeta} [DecidableEq β] (k : ℕ)
    (cls : Fin (k + 2) → β) (key : Fin (k + 2) → ℕ)
    (trace : ρ → Fin (k + 2) → Bool)
    (hup : ∀ r a b, cls a = cls b → key a ≤ key b →
      trace r a = true → trace r b = true)
    (hsupport : ∀ r, (∀ j, trace r j = true) ∨
      ((Finset.univ.filter (fun j => trace r j = true)).image cls).card ≤ k) :
    ∃ word : Fin (k + 2) → Bool,
      (∃ j, word j = false) ∧ ∀ r, trace r ≠ word := by
…

theorem OAI.Problem348.DirectNonshattering.exists_missing_word_pointwise line 199

Source documentation

Coordinatewise form of the missing-word theorem.

theorem exists_missing_word_pointwise {ρ : Type uRho} {β : Type uBeta} [DecidableEq β] (k : ℕ)
    (cls : Fin (k + 2) → β) (key : Fin (k + 2) → ℕ)
    (trace : ρ → Fin (k + 2) → Bool)
    (hup : ∀ r a b, cls a = cls b → key a ≤ key b →
      trace r a = true → trace r b = true)
    (hsupport : ∀ r, (∀ j, trace r j = true) ∨
      ((Finset.univ.filter (fun j => trace r j = true)).image cls).card ≤ k) :
    ∃ word : Fin (k + 2) → Bool, ∀ r, ∃ j, trace r j ≠ word j := by
…

theorem OAI.Problem348.DirectNonshattering.matrix_missing_word line 216

Source documentation

Matrix-facing form, handling both dummy columns and dummy rows. No injectivity assumption on the selected columns is needed.

theorem matrix_missing_word {R : Type uR} {C : Type uC} {β : Type uBeta} [DecidableEq β] (k : ℕ)
    (A : R → C → Bool) (cols : Fin (k + 2) → C)
    (cls : C → β) (key : C → ℕ) (dummyRow : R → Prop) (dummyCol : C → Prop)
    (hdummyRow : ∀ r, dummyRow r → ∀ c, A r c = true)
    (hdummyCol : ∀ c, dummyCol c → ∀ r, A r c = true)
    (hup : ∀ r, ¬ dummyRow r → ∀ a b,
      ¬ dummyCol a → ¬ dummyCol b → cls a = cls b → key a ≤ key b →
      A r a = true → A r b = true)
    (hsupport : ∀ r, ¬ dummyRow r →
      (∀ j, ¬ dummyCol (cols j)) →
      ((Finset.univ.filter (fun j => A r (cols j) = true)).image
        (cls ∘ cols)).card ≤ k) :
…

theorem OAI.Problem348.DirectNonshattering.matrix_missing_word_of_class_cover line 248

Source documentation

An explicit cover by at most k column classes is enough for the support premise. This form avoids cardinal computations on selected columns.

theorem matrix_missing_word_of_class_cover {R : Type uR} {C : Type uC} {β : Type uBeta} [DecidableEq β] (k : ℕ)
    (A : R → C → Bool) (cols : Fin (k + 2) → C)
    (cls : C → β) (key : C → ℕ) (dummyRow : R → Prop) (dummyCol : C → Prop)
    (hdummyRow : ∀ r, dummyRow r → ∀ c, A r c = true)
    (hdummyCol : ∀ c, dummyCol c → ∀ r, A r c = true)
    (hup : ∀ r, ¬ dummyRow r → ∀ a b,
      ¬ dummyCol a → ¬ dummyCol b → cls a = cls b → key a ≤ key b →
      A r a = true → A r b = true)
    (hcover : ∀ r, ¬ dummyRow r → ∃ S : Finset β, S.card ≤ k ∧
      ∀ c, ¬ dummyCol c → A r c = true → cls c ∈ S) :
    ∃ word : Fin (k + 2) → Bool, ∀ r, ∃ j, A r (cols j) ≠ word j := by
…