OAI/Computability/MaxCut/Games/SeparationCertificate.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

A single finite polynomial certifies injectivity and pair separation of the actual binary-linear parametrization.

  1. def OAI.MaxCutGames.Quadratic.nonzeroBinaryInputs line 21
  2. def OAI.MaxCutGames.Quadratic.distinctNonzeroBinaryPairs line 25
  3. def OAI.MaxCutGames.Quadratic.separationPolynomial line 29
  4. theorem OAI.MaxCutGames.Quadratic.separationPolynomial_ne_zero line 33
  5. theorem OAI.MaxCutGames.Quadratic.parameterMap_separated_of_eval_ne_zero line 51

    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.MaxCutGames.Quadratic.separationPolynomial, OAI.MaxCutGames.Quadratic.parameterMap

  6. theorem OAI.MaxCutGames.Quadratic.isGeneric_range_of_injective line 113

    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.MaxCutGames.Quadratic.alignmentEvent, OAI.MaxCutGames.Quadratic.alignmentRightHandSide, OAI.MaxCutGames.Quadratic.IsGeneric

  7. theorem OAI.MaxCutGames.Quadratic.finrank_range_binary_parameters line 183

    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
…
  8. def OAI.MaxCutGames.Quadratic.assignmentProbability line 207

    Source documentation

    The exact uniform probability on an explicit finite assignment space.

    def assignmentProbability {n : ℕ} (event : (Fin n → F) → Prop) : ℚ≥0 := by
…
  9. theorem OAI.MaxCutGames.Quadratic.assignmentProbability_mono line 212
  10. theorem OAI.MaxCutGames.Quadratic.assignmentProbability_eval_zero_le line 223

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

  11. theorem OAI.MaxCutGames.Quadratic.totalDegree_map_eq_of_injective line 233

    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
…
  12. theorem OAI.MaxCutGames.Quadratic.assignmentProbability_eval₂_zero_le line 242

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

  13. theorem OAI.MaxCutGames.Quadratic.assignmentProbability_le_of_polynomial line 258

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

  14. theorem OAI.MaxCutGames.Quadratic.assignmentProbability_union_le line 269

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

  15. def OAI.MaxCutGames.Quadratic.reindexAssignments line 309

    Source documentation

    Reindexing an assignment transports it contravariantly along the variable equivalence.

    def reindexAssignments (e : σ ≃ τ) : (σ → F) ≃ (τ → F) where
…
  16. def OAI.MaxCutGames.Quadratic.finiteAssignmentProbability line 316

    Source documentation

    Uniform assignment probability for an arbitrary finite variable set.

    def finiteAssignmentProbability [Fintype σ] (event : (σ → F) → Prop) : ℚ≥0 := by
…
  17. theorem OAI.MaxCutGames.Quadratic.finiteAssignmentProbability_reindex line 322
  18. theorem OAI.MaxCutGames.Quadratic.finiteAssignmentProbability_le_of_polynomial line 340

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

  19. theorem OAI.MaxCutGames.Quadratic.finiteAssignmentProbability_eval₂_zero_le line 363
  20. theorem OAI.MaxCutGames.Quadratic.finiteAssignmentProbability_union_le line 372

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

  21. theorem OAI.MaxCutGames.Quadratic.exists_genericity_polynomial line 409
  22. theorem OAI.MaxCutGames.Quadratic.exists_genericity_error_numerator line 429

    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.MaxCutGames.Quadratic.D, OAI.MaxCutGames.Quadratic.finiteAssignmentProbability, OAI.MaxCutGames.Quadratic.parameterMap, OAI.MaxCutGames.Quadratic.IsGeneric

  23. def OAI.MaxCutGames.Quadratic.parameterMapEquiv line 457

    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
…
  24. theorem OAI.MaxCutGames.Quadratic.parameterMap_event_card line 471
  25. theorem OAI.MaxCutGames.Quadratic.parameterMap_event_probability line 484

    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.MaxCutGames.Quadratic.finiteAssignmentProbability, OAI.MaxCutGames.Quadratic.parameterMap

  26. def OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection line 517

    Source documentation

    A linear parameter map with its injectivity proof.

    def Injection (K V W : Type*) [Field K] [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W] :=
…
  27. instance OAI.MaxCutGames.Quadratic.UniformSubspaces.injectionAction line 521
  28. theorem OAI.MaxCutGames.Quadratic.UniformSubspaces.injection_transitive line 535

    Source documentation

    Every two injections are carried to each other by an automorphism of the ambient space: extend the isomorphism between their two images.

    theorem injection_transitive (J₁ J₂ : Injection K V W) :
    ∃ a : W ≃ₗ[K] W, a • J₁ = J₂ := by
…

    Mentions: OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection

  29. def OAI.MaxCutGames.Quadratic.UniformSubspaces.image line 550

    Source documentation

    The image has the dimension of the parameter space.

    def image (J : Injection K V W) : RankSpace K W (finrank K V) :=
…

    Mentions: OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection

  30. theorem OAI.MaxCutGames.Quadratic.UniformSubspaces.image_action line 554
  31. theorem OAI.MaxCutGames.Quadratic.UniformSubspaces.mean_image line 563

    Source documentation

    Exact uniform image law, conditional only on injectivity of the map.

    theorem mean_image (J₀ : Injection K V W) (f : RankSpace K W (finrank K V) → ℚ) :
    (∑ J : Injection K V W, f (image J)) / Fintype.card (Injection K V W) =
      (∑ S : RankSpace K W (finrank K V), f S) /
        Fintype.card (RankSpace K W (finrank K V)) := by
…

    Mentions: OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection, OAI.MaxCutGames.Quadratic.UniformSubspaces.image

  32. theorem OAI.MaxCutGames.Quadratic.UniformSubspaces.bad_image_count_ratio line 573

    Source documentation

    Indicator specialization of the exact law, without assuming genericity or independence of a subsequently chosen lift.

    theorem bad_image_count_ratio (J₀ : Injection K V W)
    (Bad : RankSpace K W (finrank K V) → Prop) :
    (Nat.card {J : Injection K V W // Bad (image J)} : ℚ) /
        Fintype.card (Injection K V W) =
      (Nat.card {S : RankSpace K W (finrank K V) // Bad S} : ℚ) /
        Fintype.card (RankSpace K W (finrank K V)) := by
…

    Mentions: OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection, OAI.MaxCutGames.Quadratic.UniformSubspaces.image

  33. theorem OAI.MaxCutGames.Quadratic.UniformSubspaces.bad_subspace_bound line 586

    Source documentation

    An unconditional bad-parameter count bound transfers after conditioning on injectivity, paying exactly the usual 1/(1-β) factor. The premises are ordinary count inequalities and can come from polynomial union bounds.

    theorem bad_subspace_bound (J₀ : Injection K V W)
    (Bad : RankSpace K W (finrank K V) → Prop) (α β : ℚ) (hα : 0 ≤ α) (hβ : β < 1)
    (hbad : (Nat.card {J : Injection K V W // Bad (image J)} : ℚ) ≤
      α * Nat.card (V →ₗ[K] W))
    (hinj : (1 - β) * Nat.card (V →ₗ[K] W) ≤ Fintype.card (Injection K V W)) :
    (Nat.card {S : RankSpace K W (finrank K V) // Bad S} : ℚ) /
        Fintype.card (RankSpace K W (finrank K V)) ≤ α / (1 - β) := by
…

    Mentions: OAI.MaxCutGames.Quadratic.UniformSubspaces.Injection, OAI.MaxCutGames.Quadratic.UniformSubspaces.image

  34. theorem OAI.MaxCutGames.Quadratic.conditioning_counts_inline_GenericSubspaceProbability line 621
  35. theorem OAI.MaxCutGames.Quadratic.generic_subspace_and_probability_of_parameter_error line 668

    Source documentation

    Both generic-subspace existence and the conditional Grassmannian bound follow from the single unconditional parameter-map exceptional bound.

    theorem generic_subspace_and_probability_of_parameter_error (α : ℚ)
    (hα₀ : 0 ≤ α) (hα : α < 1)
    (herror : (finiteAssignmentProbability (fun x : (Fin 3 × J) → F =>
      ¬(Function.Injective (parameterMap x) ∧ IsGeneric (parameterMap x).range)) : ℚ) ≤ α) :
    (∃ S : RankSpace (ZMod 2) (Fin 3 → F) (Fintype.card J), IsGeneric S.1) ∧
      nongenericFraction F (Fintype.card J) ≤ α / (1 - α) := by
…

    Mentions: OAI.MaxCutGames.Quadratic.finiteAssignmentProbability, OAI.MaxCutGames.Quadratic.parameterMap, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Quadratic.nongenericFraction

  36. theorem OAI.MaxCutGames.Quadratic.exists_generic_subspace_error_numerator line 712

    Source documentation

    The exact genericity statement with a positive numerator fixed before the extension field. The property quantifies over every binary linear lift.

    theorem exists_generic_subspace_error_numerator (J : Type*) [Fintype J] :
    ∃ D : ℕ, 0 < D ∧
      ∀ (F : Type*) [Field F] [Fintype F] [CharP F 2] [Algebra (ZMod 2) F],
        (D : ℚ) / Fintype.card F < 1 →
        (∃ S : RankSpace (ZMod 2) (Fin 3 → F) (Fintype.card J), IsGeneric S.1) ∧
          nongenericFraction F (Fintype.card J) ≤
            ((D : ℚ) / Fintype.card F) / (1 - (D : ℚ) / Fintype.card F) := by
…

    Mentions: OAI.MaxCutGames.Quadratic.D, OAI.MaxCutGames.Quadratic.IsGeneric, OAI.MaxCutGames.Quadratic.nongenericFraction

  37. theorem OAI.MaxCutGames.Quadratic.conditional_error_le_of_small line 728

    Source documentation

    A convenient numerical threshold for choosing one field for finitely many ranks: α ≤ min(1/2, ε/2) is sufficient.

    theorem conditional_error_le_of_small (α ε : ℚ) (hα : 0 ≤ α)
    (hhalf : α ≤ 1 / 2) (hε : α ≤ ε / 2) : α / (1 - α) ≤ ε := by
…