AlignmentCertificateLemmas.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

One polynomial controls all binary linear lifts

For fixed binary dimension, multiply the nonzero obstructions for the finitely many sets of 3r + 1 nonzero inputs. A nonvanishing specialization then obeys the alignment bound simultaneously for every binary linear map. The resulting polynomial and its degree are chosen before the extension field.

theorem OAI.UniqueGamesTheorem.Quadratic.exists_all_lifts_alignment_polynomial line 29

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.UniqueGamesTheorem.Quadratic.alignmentEvent, OAI.UniqueGamesTheorem.Quadratic.parameterMap

def OAI.UniqueGamesTheorem.Quadratic.parameterMapEquiv line 105
Source documentation
Every binary-linear map is determined by its freely chosen field-valued basis entries, with no rejection or nonuniform multiplicity.
```
def parameterMapEquiv : ((Fin 3 × J) → F) ≃
    ((J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F)) where
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.parameterMap_event_card line 119
theorem OAI.UniqueGamesTheorem.Quadratic.parameterMap_event_probability line 132
Source documentation
The uniform probability on field entries is literally the uniform probability on all linear maps. This is the denominator used before conditioning on injectivity in UniformSubspaces.bad_subspace_bound.
```
theorem parameterMap_event_probability
    (event : ((J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F)) → Prop) :
    (finiteAssignmentProbability (fun x => event (parameterMap x)) : ℚ) =
      (Nat.card {g : (J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F) // event g} : ℚ) /
        Nat.card ((J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability, OAI.UniqueGamesTheorem.Quadratic.parameterMap
def OAI.UniqueGamesTheorem.Quadratic.nonzeroBinaryInputs line 166
def OAI.UniqueGamesTheorem.Quadratic.distinctNonzeroBinaryPairs line 170
def OAI.UniqueGamesTheorem.Quadratic.separationPolynomial line 174
theorem OAI.UniqueGamesTheorem.Quadratic.separationPolynomial_ne_zero line 178
theorem OAI.UniqueGamesTheorem.Quadratic.parameterMap_separated_of_eval_ne_zero line 196
Source documentation
Outside the zero set of the fixed separation polynomial, the actual parametrization is injective and no two distinct nonzero inputs have proportional images. The same polynomial works over every characteristic-two field.
```
theorem parameterMap_separated_of_eval_ne_zero
    {F : Type*} [Field F] [CharP F 2] [Algebra (ZMod 2) F]
    (x : (Fin 3 × J) → F)
    (hx : eval₂ (algebraMap (ZMod 2) F) x (separationPolynomial J) ≠ 0) :
    Function.Injective (parameterMap x) ∧
      ∀ t u : J → ZMod 2, t ≠ 0 → u ≠ 0 →
        (∃ a : F, parameterMap x t = a • parameterMap x u) → t = u := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.separationPolynomial, OAI.UniqueGamesTheorem.Quadratic.parameterMap
theorem OAI.UniqueGamesTheorem.Quadratic.exists_genericity_polynomial line 261
theorem OAI.UniqueGamesTheorem.Quadratic.exists_genericity_error_numerator line 281
Source documentation
The total exceptional probability for random coordinate entries is O_r(1 / |F|), with a positive integer numerator fixed before F is chosen. Both noninjectivity and failure of the all-lifts image property are counted.
```
theorem exists_genericity_error_numerator (J : Type*) [Fintype J] :
    ∃ D : ℕ, 0 < D ∧
      ∀ (F : Type*) [Field F] [Fintype F] [CharP F 2] [Algebra (ZMod 2) F],
        finiteAssignmentProbability (fun x : (Fin 3 × J) → F =>
          ¬(Function.Injective (parameterMap x) ∧ IsGeneric (parameterMap x).range)) ≤
            (D : ℚ≥0) / Fintype.card F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.D, OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability, OAI.UniqueGamesTheorem.Quadratic.parameterMap, OAI.UniqueGamesTheorem.Quadratic.IsGeneric
abbrev OAI.UniqueGamesTheorem.Quadratic.traceBinary line 316
Source documentation
The field trace to the binary prime field.
```
noncomputable abbrev traceBinary : F →ₗ[ZMod 2] ZMod 2 := Algebra.trace (ZMod 2) F
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.trace_square line 319
theorem OAI.UniqueGamesTheorem.Quadratic.trace_square_mul line 326
Source documentation
Moving a square from the first factor through the trace.
```
theorem trace_square_mul (t c : F) :
    traceBinary (t ^ 2 * c) = traceBinary (t * squareRoot c) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.traceBinary, OAI.UniqueGamesTheorem.Quadratic.squareRoot
theorem OAI.UniqueGamesTheorem.Quadratic.trace_mul_vanish_iff line 335
Source documentation
The trace pairing detects every nonzero field element.
```
theorem trace_mul_vanish_iff (a : F) :
    (∀ t : F, traceBinary (t * a) = 0) ↔ a = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.traceBinary
theorem OAI.UniqueGamesTheorem.Quadratic.trace_quadratic_vanish_iff line 345