HostNonshattering.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Nonshattering for the concrete canonical host

This is a direct application of the qualitative five-column obstruction to Problem348.Construction.host. It needs no axis order and no injectivity assumption on the five selected non-anchor columns.

abbrev OAI.Problem348.Construction.NonanchorPosition line 23
Source documentation
The two kinds of non-anchor positions, without their outer sum tag.
```
abbrev NonanchorPosition (h : ℕ) := VariablePosition h ⊕ Fin (2 ^ h)
```
Mentions: OAI.Problem348.Construction.VariablePosition
def OAI.Problem348.Construction.nonanchorClass line 27
Source documentation
Column-class labels for the non-anchor induced submatrix. The dummy label is irrelevant because dummy columns are treated separately.
```
def nonanchorClass {h : ℕ} : NonanchorPosition h → ℕ
  | Sum.inl v => v.1.val
  | Sum.inr _ => 0
```
Mentions: OAI.Problem348.Construction.NonanchorPosition
def OAI.Problem348.Construction.nonanchorKey line 31
def OAI.Problem348.Construction.nonanchorDummy line 35
instance OAI.Problem348.Construction.(instance at line 39) line 39
def OAI.Problem348.Construction.variableSupportLabels line 43
Source documentation
The three class labels that can contain ones in a variable row.
```
def variableSupportLabels {h : ℕ} (r : VariablePosition h) : Finset ℕ :=
…
```
Mentions: OAI.Problem348.Construction.VariablePosition
theorem OAI.Problem348.Construction.variableSupportLabels_card_le line 46
theorem OAI.Problem348.Construction.variableEntry_mono_class line 51
Source documentation
The constant-class suffix property, stated for the actual host kernel.
```
theorem variableEntry_mono_class {h : ℕ} (r c d : VariablePosition h)
    (hclass : c.1.val = d.1.val) (hnode : node c ≤ node d)
    (hc : variableEntry r c = true) : variableEntry r d = true := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.node, OAI.Problem348.Construction.variableEntry
theorem OAI.Problem348.Construction.variableEntry_mem_support line 61
Source documentation
A true variable entry has one of the three possible column-class labels.
```
theorem variableEntry_mem_support {h : ℕ} (r c : VariablePosition h)
    (hc : variableEntry r c = true) : c.1.val ∈ variableSupportLabels r := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.variableEntry, OAI.Problem348.Construction.variableSupportLabels
theorem OAI.Problem348.Construction.nonanchor_host_not_surjective line 71
Source documentation
The induced matrix on all non-anchor positions misses a five-bit word.
```
theorem nonanchor_host_not_surjective (h : ℕ)
    (selected : Fin 5 → NonanchorPosition h) :
    ¬ Function.Surjective
      (fun r : NonanchorPosition h =>
        fun i => host (Sum.inr r) (Sum.inr (selected i))) := by
…
```
Mentions: OAI.Problem348.Construction.NonanchorPosition, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_nonanchor_missing_word line 111
Source documentation
The actual host, stated using its outer position type. This avoids any choice of a separate non-anchor enumeration in anchor-rigidity applications.
```
theorem host_nonanchor_missing_word {h : ℕ} (columns : Fin 5 → Position h)
    (hcolumns : ∀ i, ∃ c : NonanchorPosition h, columns i = Sum.inr c) :
    ∃ w : Fin 5 → Bool, ∀ r : Position h,
      (∃ a : NonanchorPosition h, r = Sum.inr a) →
      (fun i => host r (columns i)) ≠ w := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.NonanchorPosition, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.host_nonanchor_submatrix_not_surjective line 128
Source documentation
Restricting to any collection of non-anchor rows still misses a word. This is the form used for the final 32 rows of an alleged anchor copy.
```
theorem host_nonanchor_submatrix_not_surjective {h : ℕ} {R : Type uR}
    (rows : R → Position h) (columns : Fin 5 → Position h)
    (hrows : ∀ r, ∃ a : NonanchorPosition h, rows r = Sum.inr a)
    (hcolumns : ∀ i, ∃ c : NonanchorPosition h, columns i = Sum.inr c) :
    ¬ Function.Surjective (fun r i => host (rows r) (columns i)) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.NonanchorPosition, OAI.Problem348.Construction.host
theorem OAI.Problem348.Construction.exists_nonanchor_iff_not_isLeft line 139
Source documentation
The outer sum tag gives a convenient intrinsic non-anchor predicate.
```
@[simp] theorem exists_nonanchor_iff_not_isLeft {h : ℕ} (x : Position h) :
    (∃ a : NonanchorPosition h, x = Sum.inr a) ↔ ¬ x.isLeft := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.NonanchorPosition

theorem OAI.Problem348.Construction.host_nonanchor_missing_entry line 144

Source documentation

Pointwise missing-word property for concrete anchor rigidity.

theorem host_nonanchor_missing_entry {h : ℕ} (columns : Fin 5 → Position h)
    (hcolumns : ∀ i, ¬ (columns i).isLeft) :
    ∃ w : Fin 5 → Bool, ∀ r : Position h, ¬ r.isLeft →
      ∃ i, host r (columns i) ≠ w i := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host

theorem OAI.Problem348.Construction.host_nonanchor_subtype_not_surjective line 156

Source documentation

The subtype formulation also avoids making any non-anchor choices.

theorem host_nonanchor_subtype_not_surjective {h : ℕ}
    (columns : Fin 5 → Position h) (hcolumns : ∀ i, ¬ (columns i).isLeft) :
    ¬ Function.Surjective
      (fun r : {x : Position h // ¬ x.isLeft} => fun i => host r.val (columns i)) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host