BlockSpanLemmas.lean`

57 declarations, 0 contain sorry, 0 declared as axioms

The spanning clause of Lemma latent-block. Three coordinate lines already suffice. Horizontal coordinate vectors lie in their own block; vertical coordinate vectors lie in either of the other two blocks.

def OAI.UniqueGamesTheorem.Quadratic.basisCoord line 36
Source documentation
The three standard coordinate vectors of the quadratic block.
```
def basisCoord (i : Fin 3) : Vec F := Pi.single i 1
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.basisCoord_ne_zero line 38
theorem OAI.UniqueGamesTheorem.Quadratic.Q_smul_basisCoord line 43
theorem OAI.UniqueGamesTheorem.Quadratic.dot_smul_basisCoord_of_ne line 48
theorem OAI.UniqueGamesTheorem.Quadratic.basisCoord_decomposition line 54
Source documentation
The explicit coordinate decomposition, over the field rather than only over the binary scalars of the block spaces.
```
theorem basisCoord_decomposition (x : Vec F) :
    x = x 0 • basisCoord 0 + x 1 • basisCoord 1 + x 2 • basisCoord 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.basisCoord
theorem OAI.UniqueGamesTheorem.Quadratic.horizontal_mem_U_basisCoord line 61
theorem OAI.UniqueGamesTheorem.Quadratic.vertical_mem_U_basisCoord_of_ne line 67
def OAI.UniqueGamesTheorem.Quadratic.coordinateBlockSpan line 74
Source documentation
The binary span of the three coordinate block spaces.
```
def coordinateBlockSpan : Submodule (ZMod 2) (Vec F × Vec F) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.U_basisCoord_le_coordinateBlockSpan line 77
theorem OAI.UniqueGamesTheorem.Quadratic.horizontal_mem_coordinateBlockSpan line 84
theorem OAI.UniqueGamesTheorem.Quadratic.vertical_mem_coordinateBlockSpan line 89
theorem OAI.UniqueGamesTheorem.Quadratic.mem_coordinateBlockSpan line 103
Source documentation
Every pair is a sum of three horizontal and three vertical coordinate pairs, all already in the sum of the coordinate blocks.
```
theorem mem_coordinateBlockSpan (p : Vec F × Vec F) :
    p ∈ (coordinateBlockSpan : Submodule (ZMod 2) (Vec F × Vec F)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.coordinateBlockSpan
theorem OAI.UniqueGamesTheorem.Quadratic.coordinateBlockSpan_eq_top line 123
theorem OAI.UniqueGamesTheorem.Quadratic.iSup_U_nonzero_eq_top line 131
Source documentation
The block spaces for all nonzero line generators span the whole ambient binary vector space. The proof uses just the three coordinate generators.
```
theorem iSup_U_nonzero_eq_top :
    (⨆ v : {v : Vec F // v ≠ 0}, U v.1) = ⊤ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U

theorem OAI.UniqueGamesTheorem.Quadratic.eq_top_of_binary_coordinates line 158

Source documentation

A coordinate-stable subspace containing the coordinates is the whole function space when the coordinates separate points and exclude the zero point. The proof constructs each point indicator by successively removing the other points.

theorem eq_top_of_binary_coordinates
    {F X I : Type*} [Field F] [Fintype X]
    (c : I → X → F) (W : Submodule F (X → F))
    (hbinary : ∀ i x, c i x = 0 ∨ c i x = 1)
    (hseparate : ∀ x y, x ≠ y → ∃ i, c i x ≠ c i y)
    (hnonzero : ∀ x, ∃ i, c i x ≠ 0)
    (hcoordinate : ∀ i, c i ∈ W)
    (hstable : ∀ i f, f ∈ W → (fun x => c i x * f x) ∈ W) :
    W = ⊤ := by
…

def OAI.UniqueGamesTheorem.Quadratic.quadraticEvaluationSpan line 219
Source documentation
Degree-two evaluation space. Repeated indices are allowed, so on binary points this also contains every degree-one evaluation.
```
def quadraticEvaluationSpan {F X I : Type*} [Field F]
    (c : I → X → F) : Submodule F (X → F) :=
…
```
def OAI.UniqueGamesTheorem.Quadratic.cubicEvaluationSpan line 225
Source documentation
Degree-three evaluation space. Repeated indices recover all lower positive degrees on binary points.
```
def cubicEvaluationSpan {F X I : Type*} [Field F]
    (c : I → X → F) : Submodule F (X → F) :=
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.eq_top_of_cubic_le_of_le_quadratic line 230

theorem OAI.UniqueGamesTheorem.Quadratic.quadraticEvaluationSpan_eq_top_of_cubic_le line 281

Source documentation

Equality of the quadratic and cubic evaluation spaces can occur only when both are already the full function space.

theorem quadraticEvaluationSpan_eq_top_of_cubic_le
    {F X I : Type*} [Field F] [Fintype X]
    (c : I → X → F)
    (hbinary : ∀ i x, c i x = 0 ∨ c i x = 1)
    (hseparate : ∀ x y, x ≠ y → ∃ i, c i x ≠ c i y)
    (hnonzero : ∀ x, ∃ i, c i x ≠ 0)
    (h : cubicEvaluationSpan c ≤ quadraticEvaluationSpan c) :
    quadraticEvaluationSpan c = ⊤ :=
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.cubicEvaluationSpan, OAI.UniqueGamesTheorem.Quadratic.quadraticEvaluationSpan

theorem OAI.UniqueGamesTheorem.Quadratic.binary_eq_zero_or_one line 292
Source documentation
Every element of the binary field is either zero or one.
```
theorem binary_eq_zero_or_one (x : ZMod 2) : x = 0 ∨ x = 1 := by
…
```

theorem OAI.UniqueGamesTheorem.Quadratic.eq_top_of_binary_evaluation_stable line 300

Source documentation

The exact evaluation-space form used for the genericity argument. φ embeds the binary coordinates into the field of rational functions (or any other field of characteristic two).

theorem eq_top_of_binary_evaluation_stable
    {F : Type*} [Field F] {r : ℕ}
    (E : Finset (Fin r → ZMod 2))
    (hzero : (0 : Fin r → ZMod 2) ∉ E)
    (φ : ZMod 2 →+* F)
    (W : Submodule F (E → F))
    (hcoordinate : ∀ i : Fin r, (fun t : E => φ (t.val i)) ∈ W)
    (hstable : ∀ (i : Fin r) (f : E → F), f ∈ W →
      (fun t : E => φ (t.val i) * f t) ∈ W) : W = ⊤ := by
…

theorem OAI.UniqueGamesTheorem.Quadratic.exists_cubic_not_mem_of_finrank_lt line 351

Source documentation

A proper-dimensional subspace of the quadratic evaluation space misses at least one cubic evaluation. This supplies a concrete coefficient vector outside the alignment-column span.

theorem exists_cubic_not_mem_of_finrank_lt
    {F X I : Type*} [Field F] [Fintype X]
    (c : I → X → F) (W : Submodule F (X → F))
    (hbinary : ∀ i x, c i x = 0 ∨ c i x = 1)
    (hseparate : ∀ x y, x ≠ y → ∃ i, c i x ≠ c i y)
    (hnonzero : ∀ x, ∃ i, c i x ≠ 0)
    (hquadratic : W ≤ quadraticEvaluationSpan c)
    (hdim : Module.finrank F W < Fintype.card X) :
    ∃ i j k, (fun x => c i x * c j x * c k x) ∉ W := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.quadraticEvaluationSpan

abbrev OAI.UniqueGamesTheorem.Quadratic.BinaryField line 388
Source documentation
The degree-d binary Galois field. Cardinality statements below require d > 0; the degenerate exponent zero is deliberately excluded.
```
abbrev BinaryField (d : ℕ) := GaloisField 2 d
```
theorem OAI.UniqueGamesTheorem.Quadratic.card_binaryField line 390
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_binaryField line 394
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_binaryField_triple line 398
def OAI.UniqueGamesTheorem.Quadratic.fieldDegree line 405
Source documentation
A deliberately simple explicit upper choice; optimization of the field size is irrelevant because these thresholds are fixed before the input.
```
def fieldDegree (cardThreshold rankThreshold : ℕ) : ℕ :=
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.fieldDegree_pos line 408
theorem OAI.UniqueGamesTheorem.Quadratic.threshold_lt_two_pow_fieldDegree line 411
theorem OAI.UniqueGamesTheorem.Quadratic.rankThreshold_le_triple_fieldDegree line 415
theorem OAI.UniqueGamesTheorem.Quadratic.exists_binary_field_degree line 419
theorem OAI.UniqueGamesTheorem.Quadratic.chosen_binaryField_thresholds line 425
Source documentation
Simultaneous cardinality and rank threshold attainment by the same field.
```
theorem chosen_binaryField_thresholds (N r : ℕ) :
    N < Nat.card (BinaryField (fieldDegree N r)) ∧
      r ≤ Module.finrank (ZMod 2) (Fin 3 → BinaryField (fieldDegree N r)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.BinaryField, OAI.UniqueGamesTheorem.Quadratic.fieldDegree
def OAI.UniqueGamesTheorem.Quadratic.SquarefreeExponent line 456
Source documentation
Exponents zero or one represent parity classes.
```
def SquarefreeExponent (a : σ →₀ ℕ) : Prop := ∀ k, a k < 2
```

theorem OAI.UniqueGamesTheorem.Quadratic.coeff_expand_mul_monomial_of_ne line 459

Source documentation

Two different squarefree shifts have disjoint expanded supports.

theorem coeff_expand_mul_monomial_of_ne
    (p : MvPolynomial σ R) (a b n : σ →₀ ℕ)
    (ha : SquarefreeExponent a) (hb : SquarefreeExponent b) (hab : a ≠ b) :
    (expand 2 p * monomial b 1).coeff (2 • n + a) = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.SquarefreeExponent

theorem OAI.UniqueGamesTheorem.Quadratic.coeff_expand_mul_monomial_self line 485
Source documentation
Within one parity class coefficient extraction recovers the coefficient before expansion.
```
theorem coeff_expand_mul_monomial_self
    (p : MvPolynomial σ R) (a n : σ →₀ ℕ) :
    (expand 2 p * monomial a 1).coeff (2 • n + a) = p.coeff n := by
…
```

theorem OAI.UniqueGamesTheorem.Quadratic.coeff_sum_expand_mul_monomial line 491

Source documentation

Extraction from a finite sum isolates its unique parity class.

theorem coeff_sum_expand_mul_monomial [Fintype ι]
    (e : ι → σ →₀ ℕ) (he : ∀ i, SquarefreeExponent (e i))
    (hinj : Function.Injective e) (p : ι → MvPolynomial σ R)
    (i : ι) (n : σ →₀ ℕ) :
    (∑ j, expand 2 (p j) * monomial (e j) 1).coeff (2 • n + e i) =
      (p i).coeff n := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.SquarefreeExponent

theorem OAI.UniqueGamesTheorem.Quadratic.sum_expand_mul_monomial_eq_zero_iff line 509
Source documentation
A polynomial dependence between distinct squarefree parity classes is trivial, even when each coefficient is itself an arbitrary polynomial in the squared variables.
```
theorem sum_expand_mul_monomial_eq_zero_iff [Fintype ι]
    (e : ι → σ →₀ ℕ) (he : ∀ i, SquarefreeExponent (e i))
    (hinj : Function.Injective e) (p : ι → MvPolynomial σ R) :
    (∑ i, expand 2 (p i) * monomial (e i) 1) = 0 ↔ ∀ i, p i = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.SquarefreeExponent
def OAI.UniqueGamesTheorem.Quadratic.blockExponent line 522
theorem OAI.UniqueGamesTheorem.Quadratic.blockExponent_apply line 527
theorem OAI.UniqueGamesTheorem.Quadratic.blockExponent_squarefree line 533
theorem OAI.UniqueGamesTheorem.Quadratic.blockExponent_injective line 540
theorem OAI.UniqueGamesTheorem.Quadratic.blockExponent_eq_sum line 549
theorem OAI.UniqueGamesTheorem.Quadratic.monomial_blockExponent line 563
theorem OAI.UniqueGamesTheorem.Quadratic.sum_expand_mul_blockMonomial_eq_zero_iff line 572
Source documentation
In particular the three-block monomials have independent polynomial coefficients after squaring the variables.
```
theorem sum_expand_mul_blockMonomial_eq_zero_iff {J : Type*} [Fintype J]
    (p : (Fin 3 → J) → MvPolynomial (Fin 3 × J) R) :
    (∑ v, expand 2 (p v) * monomial (blockExponent v) 1) = 0 ↔
      ∀ v, p v = 0 :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.blockExponent
theorem OAI.UniqueGamesTheorem.Quadratic.zmodTwo_sq line 602
Source documentation
Every coefficient in the binary prime field is fixed by squaring.
```
theorem zmodTwo_sq (a : ZMod 2) : a ^ 2 = a := by
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.expand_two_eq_sq line 612

theorem OAI.UniqueGamesTheorem.Quadratic.exists_coordinate_separator line 618

Source documentation

A separating linear functional written in coordinate form.

theorem exists_coordinate_separator {X K : Type*} [Field K] [Fintype X]
    (W : Submodule K (X → K)) (v : X → K) (hv : v ∉ W) :
    ∃ a : X → K, (∀ w ∈ W, ∑ x, a x * w x = 0) ∧
      (∑ x, a x * v x) ≠ 0 := by
…

def OAI.UniqueGamesTheorem.Quadratic.universalLinearForm line 642
Source documentation
The universal coordinate z_i(t) with the x_ij as indeterminates.
```
noncomputable def universalLinearForm (t : J → ZMod 2) (i : Fin 3) :
    MvPolynomial (Fin 3 × J) (ZMod 2) :=
…
```
def OAI.UniqueGamesTheorem.Quadratic.universalAlignmentColumn line 648
Source documentation
Polynomial alignment columns; every lift is one linear combination of these columns.
```
noncomputable def universalAlignmentColumn (t : X → J → ZMod 2)
    (ij : Fin 3 × J) (x : X) : MvPolynomial (Fin 3 × J) (ZMod 2) :=
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.universalLinearForm_prod line 652

def OAI.UniqueGamesTheorem.Quadratic.cubicPairing line 664

Source documentation

Coefficient obtained by pairing a polynomial row with a cubic binary evaluation.

noncomputable def cubicPairing (t : X → J → ZMod 2)
    (p : X → MvPolynomial (Fin 3 × J) (ZMod 2)) (v : Fin 3 → J) :
    MvPolynomial (Fin 3 × J) (ZMod 2) :=
…

def OAI.UniqueGamesTheorem.Quadratic.alignmentObstruction line 672
Source documentation
Clearing the rational dual's denominator and squaring gives this one polynomial obstruction to simultaneous alignment. Its degree is finite and depends only on the fixed set of inputs.
```
noncomputable def alignmentObstruction (t : X → J → ZMod 2)
    (p : X → MvPolynomial (Fin 3 × J) (ZMod 2)) :
    MvPolynomial (Fin 3 × J) (ZMod 2) :=
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.alignmentObstruction_parity_expansion line 677
theorem OAI.UniqueGamesTheorem.Quadratic.alignmentObstruction_ne_zero line 693

theorem OAI.UniqueGamesTheorem.Quadratic.exists_polynomial_alignment_annihilator line 720

Source documentation

A polynomial row annihilates all alignment columns and detects a cubic evaluation. The row is constructed from a rational dual separator; there is no assumed algebraic genericity certificate.

theorem exists_polynomial_alignment_annihilator
    {J X : Type*} [Fintype J] [Fintype X]
    (t : X → J → ZMod 2) (ht : Function.Injective t)
    (hnonzero : ∀ x, t x ≠ 0) (hcard : 3 * Fintype.card J < Fintype.card X) :
    ∃ p : X → MvPolynomial (Fin 3 × J) (ZMod 2),
      (∀ ij, ∑ x, p x * universalAlignmentColumn t ij x = 0) ∧
      ∃ v : Fin 3 → J, cubicPairing t p v ≠ 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.universalAlignmentColumn, OAI.UniqueGamesTheorem.Quadratic.cubicPairing

theorem OAI.UniqueGamesTheorem.Quadratic.alignmentObstruction_eval_eq_zero line 822

Source documentation

Every specialization of the polynomial row obstructs every alignment column combination simultaneously.

theorem alignmentObstruction_eval_eq_zero
    {J X F : Type*} [Fintype J] [Fintype X] [Field F] [CharP F 2]
    (t : X → J → ZMod 2)
    (p : X → MvPolynomial (Fin 3 × J) (ZMod 2))
    (hann : ∀ ij, ∑ x, p x * universalAlignmentColumn t ij x = 0)
    (ρ : MvPolynomial (Fin 3 × J) (ZMod 2) →+* F)
    (c : X → F) (a : (Fin 3 × J) → F)
    (hc : ∀ x, c x ^ 2 = ρ (∏ i, universalLinearForm (t x) i))
    (ha : ∀ x, c x = ∑ ij, ρ (universalAlignmentColumn t ij x) * a ij) :
    ρ (alignmentObstruction t p) = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.universalAlignmentColumn, OAI.UniqueGamesTheorem.Quadratic.universalLinearForm, OAI.UniqueGamesTheorem.Quadratic.alignmentObstruction

theorem OAI.UniqueGamesTheorem.Quadratic.exists_nonzero_alignment_obstruction line 858

Source documentation

The uniform algebraic obstruction exists for every set of more than three times the binary dimension many distinct nonzero inputs. Its one polynomial works for all lifts over every characteristic-two field.

theorem exists_nonzero_alignment_obstruction
    {J X : Type*} [Fintype J] [Fintype X]
    (t : X → J → ZMod 2) (ht : Function.Injective t)
    (hnonzero : ∀ x, t x ≠ 0) (hcard : 3 * Fintype.card J < Fintype.card X) :
    ∃ P : MvPolynomial (Fin 3 × J) (ZMod 2), P ≠ 0 ∧
      ∀ (F : Type*) [Field F] [CharP F 2]
        (ρ : MvPolynomial (Fin 3 × J) (ZMod 2) →+* F)
        (c : X → F) (a : (Fin 3 × J) → F),
        (∀ x, c x ^ 2 = ρ (∏ i, universalLinearForm (t x) i)) →
        (∀ x, c x = ∑ ij, ρ (universalAlignmentColumn t ij x) * a ij) →
        ρ P = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.universalLinearForm, OAI.UniqueGamesTheorem.Quadratic.universalAlignmentColumn