ParityIndependence.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Separation of polynomial parity classes

The genericity argument uses monomials with distinct squarefree exponent vectors. Polynomial coefficients in the original «variables» become polynomials in squares after adjoining their square roots. The lemmas below prove the resulting coefficient separation directly, without assuming an algebraic independence witness.

def OAI.MaxCutGames.Quadratic.SquarefreeExponent line 24
Source documentation
Exponents zero or one represent parity classes.
```
def SquarefreeExponent (a : σ →₀ ℕ) : Prop := ∀ k, a k < 2
```

theorem OAI.MaxCutGames.Quadratic.coeff_expand_mul_monomial_of_ne line 27

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

theorem OAI.MaxCutGames.Quadratic.coeff_expand_mul_monomial_self line 53
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.MaxCutGames.Quadratic.coeff_sum_expand_mul_monomial line 59

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

theorem OAI.MaxCutGames.Quadratic.sum_expand_mul_monomial_eq_zero_iff line 77
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.MaxCutGames.Quadratic.SquarefreeExponent
def OAI.MaxCutGames.Quadratic.blockExponent line 90
theorem OAI.MaxCutGames.Quadratic.blockExponent_apply line 95
theorem OAI.MaxCutGames.Quadratic.blockExponent_squarefree line 101
theorem OAI.MaxCutGames.Quadratic.blockExponent_injective line 108
theorem OAI.MaxCutGames.Quadratic.blockExponent_eq_sum line 117
theorem OAI.MaxCutGames.Quadratic.monomial_blockExponent line 131
theorem OAI.MaxCutGames.Quadratic.sum_expand_mul_blockMonomial_eq_zero_iff line 140
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.MaxCutGames.Quadratic.blockExponent