GenericPolynomial.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

Polynomial parity obstruction

This supplies the algebraic obstruction step in the v2 genericity proof. Squaring a cleared dual row exposes its distinct squarefree parity classes. No genericity or minor-existence conclusion is assumed here.

theorem OAI.MaxCutGames.Quadratic.zmodTwo_sq line 28
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.MaxCutGames.Quadratic.expand_two_eq_sq line 38

theorem OAI.MaxCutGames.Quadratic.exists_coordinate_separator line 44

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.MaxCutGames.Quadratic.universalLinearForm line 66
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.MaxCutGames.Quadratic.universalAlignmentColumn line 72
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.MaxCutGames.Quadratic.universalLinearForm_prod line 76

def OAI.MaxCutGames.Quadratic.cubicPairing line 88

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.MaxCutGames.Quadratic.alignmentObstruction line 96
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.MaxCutGames.Quadratic.alignmentObstruction_parity_expansion line 101
theorem OAI.MaxCutGames.Quadratic.alignmentObstruction_ne_zero line 117

theorem OAI.MaxCutGames.Quadratic.eq_top_of_binary_coordinates line 138

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.MaxCutGames.Quadratic.quadraticEvaluationSpan line 199
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.MaxCutGames.Quadratic.cubicEvaluationSpan line 205
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.MaxCutGames.Quadratic.eq_top_of_cubic_le_of_le_quadratic line 210

theorem OAI.MaxCutGames.Quadratic.quadraticEvaluationSpan_eq_top_of_cubic_le line 261

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.MaxCutGames.Quadratic.cubicEvaluationSpan, OAI.MaxCutGames.Quadratic.quadraticEvaluationSpan

theorem OAI.MaxCutGames.Quadratic.binary_eq_zero_or_one line 272
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.MaxCutGames.Quadratic.eq_top_of_binary_evaluation_stable line 280

Source documentation

The exact evaluation-space form used for the v2 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.MaxCutGames.Quadratic.exists_cubic_not_mem_of_finrank_lt line 327

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.MaxCutGames.Quadratic.quadraticEvaluationSpan

theorem OAI.MaxCutGames.Quadratic.exists_polynomial_alignment_annihilator line 354

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.MaxCutGames.Quadratic.universalAlignmentColumn, OAI.MaxCutGames.Quadratic.cubicPairing

theorem OAI.MaxCutGames.Quadratic.alignmentObstruction_eval_eq_zero line 456

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.MaxCutGames.Quadratic.universalAlignmentColumn, OAI.MaxCutGames.Quadratic.universalLinearForm, OAI.MaxCutGames.Quadratic.alignmentObstruction

theorem OAI.MaxCutGames.Quadratic.exists_nonzero_alignment_obstruction line 492

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.MaxCutGames.Quadratic.universalLinearForm, OAI.MaxCutGames.Quadratic.universalAlignmentColumn

def OAI.MaxCutGames.Quadratic.parameterMap line 520
Source documentation
Independent field entries specify a binary-linear map into F³.
```
def parameterMap (x : (Fin 3 × J) → F) : (J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F) :=
…
```
theorem OAI.MaxCutGames.Quadratic.parameterMap_apply line 524
theorem OAI.MaxCutGames.Quadratic.parameterMap_basis line 530
theorem OAI.MaxCutGames.Quadratic.eval_universalLinearForm line 537
Source documentation
Evaluation of the universal polynomial is the actual linear map.
```
theorem eval_universalLinearForm (x : (Fin 3 × J) → F) (t : J → ZMod 2) (i : Fin 3) :
    MvPolynomial.eval₂ (algebraMap (ZMod 2) F) x (universalLinearForm t i) =
      parameterMap x t i := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.universalLinearForm, OAI.MaxCutGames.Quadratic.parameterMap

theorem OAI.MaxCutGames.Quadratic.dot_parameter_lift line 546

Source documentation

All linear lifts have the prescribed universal alignment columns, with their arbitrary values on the binary basis as column coefficients.

theorem dot_parameter_lift (x : (Fin 3 × J) → F)
    (g : (J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F)) (t : J → ZMod 2) :
    (∑ i, parameterMap x t i * g t i) =
      ∑ ij : Fin 3 × J,
        MvPolynomial.eval₂ (algebraMap (ZMod 2) F) x
          (universalAlignmentColumn (fun t : J → ZMod 2 => t) ij t) *
          g ((Pi.basisFun (ZMod 2) J) ij.2) ij.1 := by
…

Mentions: OAI.MaxCutGames.Quadratic.parameterMap, OAI.MaxCutGames.Quadratic.universalAlignmentColumn

theorem OAI.MaxCutGames.Quadratic.alignmentRightHandSide_sq line 561
Source documentation
The unique square-root value satisfies the universal cubic equation.
```
theorem alignmentRightHandSide_sq (x : (Fin 3 × J) → F) (t : J → ZMod 2) :
    alignmentRightHandSide (parameterMap x t) ^ 2 =
      MvPolynomial.eval₂ (algebraMap (ZMod 2) F) x
        (∏ i : Fin 3, universalLinearForm t i) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.alignmentRightHandSide, OAI.MaxCutGames.Quadratic.parameterMap, OAI.MaxCutGames.Quadratic.universalLinearForm

theorem OAI.MaxCutGames.Quadratic.exists_all_lifts_alignment_polynomial line 585

Source documentation

An unconditional polynomial exceptional-set certificate for the complete all-lifts alignment condition. There is no quantified bound on the maps g outside the conclusion, and no choice of extension field enters P.

theorem exists_all_lifts_alignment_polynomial (J : Type*) [Fintype J] [DecidableEq J] :
    ∃ P : MvPolynomial (Fin 3 × J) (ZMod 2), P ≠ 0 ∧
      ∀ (F : Type*) [Field F] [Fintype F] [CharP F 2] [Algebra (ZMod 2) F]
        (x : (Fin 3 × J) → F),
        MvPolynomial.eval₂ (algebraMap (ZMod 2) F) x P ≠ 0 →
        ∀ g : (J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F),
          (alignmentEvent (R := ZMod 2) (parameterMap x) g
…

Mentions: OAI.MaxCutGames.Quadratic.alignmentEvent, OAI.MaxCutGames.Quadratic.parameterMap

theorem OAI.MaxCutGames.Quadratic.exists_binary_coordinate_one line 657
theorem OAI.MaxCutGames.Quadratic.exists_binary_minor_one line 664
Source documentation
Distinct nonzero vectors over the binary field have a nonzero two-column minor. Since the coefficient field is binary, the minor equals one.
```
theorem exists_binary_minor_one {J : Type*} (t u : J → ZMod 2)
    (ht : t ≠ 0) (hu : u ≠ 0) (htu : t ≠ u) :
    ∃ j k, t j * u k + t k * u j = 1 := by
…
```
def OAI.MaxCutGames.Quadratic.selectorAssignment line 685
Source documentation
Set the first two rows of the indeterminate matrix to coordinate selectors. The third row is zero.
```
noncomputable def selectorAssignment (j k : J) : (Fin 3 × J) → ZMod 2 := by
…
```
theorem OAI.MaxCutGames.Quadratic.eval_universalLinearForm_selector_zero line 690
theorem OAI.MaxCutGames.Quadratic.eval_universalLinearForm_selector_one line 695
theorem OAI.MaxCutGames.Quadratic.universalLinearForm_zero_ne_zero line 700
def OAI.MaxCutGames.Quadratic.universalPairMinor line 710
Source documentation
A two-row determinant, with subtraction equal to addition in characteristic two.
```
noncomputable def universalPairMinor (t u : J → ZMod 2) :
    MvPolynomial (Fin 3 × J) (ZMod 2) :=
…
```
theorem OAI.MaxCutGames.Quadratic.universalPairMinor_ne_zero line 715
theorem OAI.MaxCutGames.Quadratic.universalPairMinor_eq_zero_of_proportional line 729
Source documentation
Proportional specialized image vectors force the fixed pair minor to vanish, for every value of the proportionality scalar.
```
theorem universalPairMinor_eq_zero_of_proportional
    {F : Type*} [Field F] [CharP F 2]
    (t u : J → ZMod 2)
    (ρ : MvPolynomial (Fin 3 × J) (ZMod 2) →+* F) (a : F)
    (h : ∀ i, ρ (universalLinearForm t i) = a * ρ (universalLinearForm u i)) :
    ρ (universalPairMinor t u) = 0 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.universalLinearForm, OAI.MaxCutGames.Quadratic.universalPairMinor