GenericSeparationLemmas.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Polynomial obstructions to collapsed or proportional binary inputs

One linear polynomial detects each nonzero input. One quadratic polynomial detects each pair of distinct nonzero binary inputs. The witnesses are proved nonzero by explicit coordinate-selector evaluations. Together with the alignment obstruction they yield a finite product whose zero set contains every failure of genericity. An O_r(1/q) bound suffices here.

theorem OAI.UniqueGamesTheorem.Quadratic.exists_binary_coordinate_one line 35
theorem OAI.UniqueGamesTheorem.Quadratic.exists_binary_minor_one line 42
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.UniqueGamesTheorem.Quadratic.selectorAssignment line 65
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.UniqueGamesTheorem.Quadratic.eval_universalLinearForm_selector_zero line 70
theorem OAI.UniqueGamesTheorem.Quadratic.eval_universalLinearForm_selector_one line 75
theorem OAI.UniqueGamesTheorem.Quadratic.universalLinearForm_zero_ne_zero line 80
def OAI.UniqueGamesTheorem.Quadratic.universalPairMinor line 90
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.UniqueGamesTheorem.Quadratic.universalPairMinor_ne_zero line 95
theorem OAI.UniqueGamesTheorem.Quadratic.universalPairMinor_eq_zero_of_proportional line 109
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.UniqueGamesTheorem.Quadratic.universalLinearForm, OAI.UniqueGamesTheorem.Quadratic.universalPairMinor
def OAI.UniqueGamesTheorem.Quadratic.assignmentProbability line 147
Source documentation
The exact uniform probability on an explicit finite assignment space.
```
def assignmentProbability {n : ℕ} (event : (Fin n → F) → Prop) : ℚ≥0 := by
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.assignmentProbability_mono line 152

theorem OAI.UniqueGamesTheorem.Quadratic.assignmentProbability_eval_zero_le line 163

Source documentation

The checked Schwartz-Zippel theorem on the whole finite field.

theorem assignmentProbability_eval_zero_le {n : ℕ}
    (p : MvPolynomial (Fin n) F) (hp : p ≠ 0) :
    assignmentProbability (fun x => MvPolynomial.eval x p = 0) ≤
      (p.totalDegree : ℚ≥0) / Fintype.card F := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.assignmentProbability

theorem OAI.UniqueGamesTheorem.Quadratic.totalDegree_map_eq_of_injective line 173

Source documentation

Injective coefficient extension preserves the total degree exactly.

theorem totalDegree_map_eq_of_injective {σ : Type*}
    (φ : K →+* F) (hφ : Function.Injective φ) (p : MvPolynomial σ K) :
    (MvPolynomial.map φ p).totalDegree = p.totalDegree := by
…

theorem OAI.UniqueGamesTheorem.Quadratic.assignmentProbability_eval₂_zero_le line 182
Source documentation
A prime-field polynomial gives the same fixed numerator in every finite extension field. Only the denominator grows with the field size.
```
theorem assignmentProbability_eval₂_zero_le {n : ℕ}
    (φ : K →+* F) (hφ : Function.Injective φ)
    (p : MvPolynomial (Fin n) K) (hp : p ≠ 0) :
    assignmentProbability (fun x => MvPolynomial.eval₂ φ x p = 0) ≤
      (p.totalDegree : ℚ≥0) / Fintype.card F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.assignmentProbability

theorem OAI.UniqueGamesTheorem.Quadratic.assignmentProbability_le_of_polynomial line 198

Source documentation

An exceptional event contained in a polynomial zero set satisfies the same bound, including events expressed by existence of an arbitrary lift.

theorem assignmentProbability_le_of_polynomial {n : ℕ}
    (φ : K →+* F) (hφ : Function.Injective φ)
    (p : MvPolynomial (Fin n) K) (hp : p ≠ 0)
    (event : (Fin n → F) → Prop)
    (hvanish : ∀ x, event x → MvPolynomial.eval₂ φ x p = 0) :
    assignmentProbability event ≤ (p.totalDegree : ℚ≥0) / Fintype.card F :=
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.assignmentProbability

theorem OAI.UniqueGamesTheorem.Quadratic.assignmentProbability_union_le line 209

Source documentation

A fixed finite family of exceptional events admits a single fixed-degree bound. There is still no enumeration or union over the possible lifts.

theorem assignmentProbability_union_le {n : ℕ} {J : Type*} [Fintype J]
    (φ : K →+* F) (hφ : Function.Injective φ)
    (p : J → MvPolynomial (Fin n) K) (hp : ∀ j, p j ≠ 0)
    (event : J → (Fin n → F) → Prop)
    (hvanish : ∀ j x, event j x → MvPolynomial.eval₂ φ x (p j) = 0) :
    assignmentProbability (fun x => ∃ j, event j x) ≤
      ((∑ j, (p j).totalDegree : ℕ) : ℚ≥0) / Fintype.card F := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.assignmentProbability

def OAI.UniqueGamesTheorem.Quadratic.reindexAssignments line 257
Source documentation
Reindexing an assignment transports it contravariantly along the variable equivalence.
```
def reindexAssignments (e : σ ≃ τ) : (σ → F) ≃ (τ → F) where
…
```
def OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability line 264
Source documentation
Uniform assignment probability for an arbitrary finite variable set.
```
def finiteAssignmentProbability [Fintype σ] (event : (σ → F) → Prop) : ℚ≥0 := by
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability_reindex line 270

theorem OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability_le_of_polynomial line 288

Source documentation

A bad event contained in a fixed nonzero polynomial's zero set has probability at most its total degree divided by the field size.

theorem finiteAssignmentProbability_le_of_polynomial [Fintype σ]
    (φ : K →+* F) (hφ : Function.Injective φ)
    (p : MvPolynomial σ K) (hp : p ≠ 0)
    (event : (σ → F) → Prop)
    (hvanish : ∀ x, event x → MvPolynomial.eval₂ φ x p = 0) :
    finiteAssignmentProbability event ≤ (p.totalDegree : ℚ≥0) / Fintype.card F := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability

theorem OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability_eval₂_zero_le line 311

theorem OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability_union_le line 320

Source documentation

A finite family of input-set obstructions yields a fixed total numerator. The family index is independent of the chosen linear lift.

theorem finiteAssignmentProbability_union_le [Fintype σ] {J : Type*} [Fintype J]
    (φ : K →+* F) (hφ : Function.Injective φ)
    (p : J → MvPolynomial σ K) (hp : ∀ j, p j ≠ 0)
    (event : J → (σ → F) → Prop)
    (hvanish : ∀ j x, event j x → MvPolynomial.eval₂ φ x (p j) = 0) :
    finiteAssignmentProbability (fun x => ∃ j, event j x) ≤
      ((∑ j, (p j).totalDegree : ℕ) : ℚ≥0) / Fintype.card F := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability

theorem OAI.UniqueGamesTheorem.Quadratic.finrank_le_one_of_nonzero_unique line 373
Source documentation
A vector space with at most one nonzero vector has dimension at most one. The statement is deliberately independent of any characteristic assumption.
```
theorem finrank_le_one_of_nonzero_unique
    (h : ∀ v w : V, v ≠ 0 → w ≠ 0 → v = w) :
    Module.finrank R V ≤ 1 := by
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_ker_le_one_of_nonzero_unique line 393
Source documentation
Nonproportionality of a generic character space makes every child kernel at most one-dimensional once the field-line kernel criterion is applied.
```
theorem finrank_ker_le_one_of_nonzero_unique (f : V →ₗ[R] W)
    (h : ∀ v w : V, v ≠ 0 → w ≠ 0 → f v = 0 → f w = 0 → v = w) :
    Module.finrank R f.ker ≤ 1 := by
…
```

theorem OAI.UniqueGamesTheorem.Quadratic.finrank_source_le_range_add_one line 410

Source documentation

Consequently the image rank can lose at most one dimension.

theorem finrank_source_le_range_add_one [FiniteDimensional R V]
    (f : V →ₗ[R] W)
    (h : ∀ v w : V, v ≠ 0 → w ≠ 0 → f v = 0 → f w = 0 → v = w) :
    Module.finrank R V ≤ Module.finrank R f.range + 1 := by
…

def OAI.UniqueGamesTheorem.Quadratic.lossIndices line 421
Source documentation
The actual finite event of a child map having a nonzero kernel.
```
def lossIndices (f : I → V →ₗ[R] W) : Finset I := by
…
```
def OAI.UniqueGamesTheorem.Quadratic.alignedCharacters line 425
theorem OAI.UniqueGamesTheorem.Quadratic.lossIndices_subset_image line 429
theorem OAI.UniqueGamesTheorem.Quadratic.card_lossIndices_le_card_aligned line 441
Source documentation
The cardinality bound does not union over lifts or orientations.
```
theorem card_lossIndices_le_card_aligned (f : I → V →ₗ[R] W)
    (aligned : V → Prop) (lineOf : V → I)
    (hkernel : ∀ i v, v ≠ 0 → f i v = 0 → aligned v ∧ lineOf v = i) :
    (lossIndices f).card ≤ (alignedCharacters aligned).card := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.lossIndices, OAI.UniqueGamesTheorem.Quadratic.alignedCharacters
theorem OAI.UniqueGamesTheorem.Quadratic.card_lossIndices_le line 449
theorem OAI.UniqueGamesTheorem.Quadratic.card_lossIndices_le_nonzero line 456
theorem OAI.UniqueGamesTheorem.Quadratic.squareMap_injective line 478
def OAI.UniqueGamesTheorem.Quadratic.squareRoot line 487
Source documentation
The unique square root, obtained by bijectivity of the finite square map.
```
noncomputable def squareRoot (c : F) : F :=
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.squareRoot_sq line 490
theorem OAI.UniqueGamesTheorem.Quadratic.squareRoot_of_sq line 493
theorem OAI.UniqueGamesTheorem.Quadratic.squareRoot_unique line 497
def OAI.UniqueGamesTheorem.Quadratic.alignmentEvent line 523
Source documentation
Nonzero inputs aligned by a specified linear lift.
```
def alignmentEvent (z : V → n → F) (g : V →ₗ[R] (n → F)) (c : V → F) :
    Finset V := by
…
```

theorem OAI.UniqueGamesTheorem.Quadratic.all_lifts_bound_iff_subsets line 530

Source documentation

Exact finite bad-set reduction. Its right hand side quantifies only over input sets, while column membership already accounts for every linear lift.

theorem all_lifts_bound_iff_subsets (b : Basis ι R V) (z : V → n → F)
    (c : V → F) (k : ℕ) :
    (∀ g : V →ₗ[R] (n → F), (alignmentEvent z g c).card ≤ k) ↔
      ∀ E : Finset V, 0 ∉ E → E.card = k + 1 →
        (fun e : E => c e) ∉
          LinearMap.range (alignmentMatrix b (fun e : E => (e : V)) z).mulVecLin := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.alignmentEvent, OAI.UniqueGamesTheorem.Quadratic.alignmentMatrix

theorem OAI.UniqueGamesTheorem.Quadratic.all_lifts_bound_of_card_le line 563
def OAI.UniqueGamesTheorem.Quadratic.alignmentRightHandSide line 580
Source documentation
The cubic square-root right hand side of the alignment equation.
```
def alignmentRightHandSide (z : Fin 3 → F) : F := squareRoot (z 0 * z 1 * z 2)
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.squareRoot
def OAI.UniqueGamesTheorem.Quadratic.IsGeneric line 584
Source documentation
The complete genericity predicate. The universal linear map quantifier occurs inside the property of the selected subspace.
```
def IsGeneric (S : Submodule (ZMod 2) (Fin 3 → F)) : Prop := by
…
```

theorem OAI.UniqueGamesTheorem.Quadratic.isGeneric_range_of_injective line 623

Source documentation

The actual range of an injective parametrization is generic when its nonproportionality and all-lifts alignment bounds hold on the domain.

theorem isGeneric_range_of_injective
    (z : V →ₗ[ZMod 2] (Fin 3 → F)) (hz : Function.Injective z)
    (hseparate : ∀ v w : V, v ≠ 0 → w ≠ 0 →
      (∃ t : F, z v = t • z w) → v = w)
    (halign : ∀ g : V →ₗ[ZMod 2] (Fin 3 → F),
      (alignmentEvent z g (fun v => alignmentRightHandSide (z v))).card ≤
        3 * Module.finrank (ZMod 2) V) :
    IsGeneric (LinearMap.range z) := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.alignmentEvent, OAI.UniqueGamesTheorem.Quadratic.alignmentRightHandSide, OAI.UniqueGamesTheorem.Quadratic.IsGeneric

theorem OAI.UniqueGamesTheorem.Quadratic.finrank_range_binary_parameters line 693

Source documentation

In the basis-parametrized case, the image rank is the number of binary input coordinates.

theorem finrank_range_binary_parameters {J : Type*} [Fintype J]
    (z : (J → ZMod 2) →ₗ[ZMod 2] (Fin 3 → F)) (hz : Function.Injective z) :
    Module.finrank (ZMod 2) (LinearMap.range z) = Fintype.card J := by
…

def OAI.UniqueGamesTheorem.Quadratic.nongenericFraction line 720
Source documentation
The actual uniform fraction of nongeneric rank-r binary subspaces.
```
def nongenericFraction (F : Type*) [Field F] [Fintype F] [CharP F 2]
    [Algebra (ZMod 2) F] (r : ℕ) : ℚ :=
…
```
def OAI.UniqueGamesTheorem.Quadratic.parameterMap line 745
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.UniqueGamesTheorem.Quadratic.parameterMap_apply line 748
theorem OAI.UniqueGamesTheorem.Quadratic.parameterMap_basis line 753
theorem OAI.UniqueGamesTheorem.Quadratic.eval_universalLinearForm line 759
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.UniqueGamesTheorem.Quadratic.universalLinearForm, OAI.UniqueGamesTheorem.Quadratic.parameterMap

theorem OAI.UniqueGamesTheorem.Quadratic.dot_parameter_lift line 767

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

theorem OAI.UniqueGamesTheorem.Quadratic.alignmentRightHandSide_sq line 782
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.UniqueGamesTheorem.Quadratic.alignmentRightHandSide, OAI.UniqueGamesTheorem.Quadratic.parameterMap, OAI.UniqueGamesTheorem.Quadratic.universalLinearForm