OAI/Computability/MaxCut/Games/FiniteFieldChoice.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

A concrete mathematical family of finite binary fields of unbounded size. The extension degree is chosen from numerical thresholds alone, before the logical output dimension of the latent gadget is selected.

  1. abbrev OAI.MaxCutGames.Quadratic.BinaryField line 17

    Source documentation

    The degree-d binary Galois field. Cardinality statements below require d > 0; the degenerate exponent zero is deliberately excluded.

    abbrev BinaryField (d : ℕ) := GaloisField 2 d
  2. theorem OAI.MaxCutGames.Quadratic.card_binaryField line 19
  3. theorem OAI.MaxCutGames.Quadratic.finrank_binaryField line 23
  4. theorem OAI.MaxCutGames.Quadratic.finrank_binaryField_triple line 27
  5. def OAI.MaxCutGames.Quadratic.fieldDegree line 34

    Source documentation

    A deliberately simple explicit upper choice; optimization of the field size is irrelevant because these thresholds are fixed before the input.

    def fieldDegree (cardThreshold rankThreshold : ℕ) : ℕ :=
…
  6. theorem OAI.MaxCutGames.Quadratic.fieldDegree_pos line 37
  7. theorem OAI.MaxCutGames.Quadratic.threshold_lt_two_pow_fieldDegree line 40
  8. theorem OAI.MaxCutGames.Quadratic.rankThreshold_le_triple_fieldDegree line 44
  9. theorem OAI.MaxCutGames.Quadratic.exists_binary_field_degree line 48
  10. theorem OAI.MaxCutGames.Quadratic.chosen_binaryField_thresholds line 54

    Source documentation

    Simultaneous cardinality and rank threshold attainment by the same field.

    theorem chosen_binaryField_thresholds (N r : ℕ) :
    N < Nat.card (BinaryField (fieldDegree N r)) ∧
      r ≤ Module.finrank (ZMod 2) (Fin 3 → BinaryField (fieldDegree N r)) := by
…

    Mentions: OAI.MaxCutGames.Quadratic.BinaryField, OAI.MaxCutGames.Quadratic.fieldDegree

  11. instance OAI.MaxCutGames.Quadratic.binaryFieldFintype line 79
  12. theorem OAI.MaxCutGames.Quadratic.exists_uniform_generic_field line 84

    Source documentation

    Simultaneous quantitative genericity, with the precise threshold order used by the latent gadget. The conclusion covers rank zero as well.

    theorem exists_uniform_generic_field (r₀ : ℕ) (ε : ℚ) (hε : 0 < ε) :
    ∃ d : ℕ, 0 < d ∧ r₀ ≤ 3 * d ∧
      (∀ r : ℕ, r ≤ r₀ → nongenericFraction (BinaryField d) r ≤ ε) ∧
      (∃ S : RankSpace (ZMod 2) (Fin 3 → BinaryField d) r₀, IsGeneric S.1) := by
…

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

  13. theorem OAI.MaxCutGames.Gadget.BaseConstruction.theta_le_one line 165
  14. theorem OAI.MaxCutGames.Gadget.BaseConstruction.rate_eq_one_sub_theta line 171
  15. theorem OAI.MaxCutGames.Gadget.BaseConstruction.quotient_detection line 176

    Source documentation

    Detection for the actual quotient, with every whole-recursion estimate discharged by the adaptive harmonic argument.

    theorem quotient_detection
    (r₀ : ℕ) (ε : ℚ) (hr₀ : 0 < r₀)
    (hbudget : badRankCoefficient r₀ * ε ≤ 1)
    (hgeneric : ∀ r : ℕ, r ≤ r₀ → nongenericFraction F r ≤ ε)
    (S₀ : Submodule (ZMod 2) (Vec F))
    (hrank : Module.finrank (ZMod 2) S₀ = r₀) (hS₀ : IsGeneric S₀)
    {E : Type} [AddCommGroup E] [Module (ZMod 2) E]
    (T : (quotientStage (F := F) (depth r₀ (fieldLineTheta F))).Input →ₗ[ZMod 2] E)
…
  16. theorem OAI.MaxCutGames.Gadget.BaseConstruction.quotient_error_le line 211

    Source documentation

    The exact nonlinear recurrence satisfies the scalar budget fixed before the field was selected.

    theorem quotient_error_le (p : ℚ) (r₀ : ℕ)
    (hgeom : (1 - fieldLineTheta F) ^ depth r₀ (fieldLineTheta F) ≤ p) :
    StageNoiseRecurrence.error
      (quotientStage (F := F) (depth r₀ (fieldLineTheta F))) ≤ p := by
…

    Mentions: OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error

  17. theorem OAI.MaxCutGames.Gadget.BaseConstruction.exists_base line 224

    Source documentation

    The unconditional finite base endpoint. All choices depend only on p; the larger logical alphabet used by the final enlargement is absent here.

    theorem exists_base (p : ℚ) (hp : 0 < p) :
    ∃ d : ℕ, 0 < d ∧ ∃ n : ℕ,
      StageNoiseRecurrence.error (quotientStage (F := BinaryField d) n) ≤ p ∧
…

    Mentions: OAI.MaxCutGames.Gadget.StageNoiseRecurrence.error

  18. def OAI.MaxCutGames.Gadget.Enlargement.probability line 253

    Source documentation

    Uniform finite probability, kept rational because the gadget noise is a pushforward of finite uniform choices.

    def probability {Ω : Type*} [Fintype Ω] (p : Ω → Prop) : ℚ :=
…
  19. theorem OAI.MaxCutGames.Gadget.Enlargement.probability_exists_le_sum line 257

    Source documentation

    A union bound without independence assumptions.

    theorem probability_exists_le_sum {Ω I : Type*} [Fintype Ω] [Fintype I]
    (p : I → Ω → Prop) :
    probability (fun x => ∃ i, p i x) ≤ ∑ i, probability (p i) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.probability

  20. theorem OAI.MaxCutGames.Gadget.Enlargement.probability_preimage_of_fibers line 273

    Source documentation

    Equal-size fibers determine the exact probability of every target event.

    theorem probability_preimage_of_fibers {Ω T : Type*} [Fintype Ω] [Fintype T]
    [Nonempty Ω] [Nonempty T] (f : Ω → T)
    (hf : ∀ x y : T, Nat.card {a : Ω // f a = x} = Nat.card {a : Ω // f a = y})
    (p : T → Prop) : probability (fun a => p (f a)) = probability p := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.probability

  21. theorem OAI.MaxCutGames.Gadget.Enlargement.exists_equiv_map_nonzero line 310

    Source documentation

    Automorphisms act transitively on the nonzero vectors. This follows by extending an isomorphism between the two one-dimensional spans.

    theorem exists_equiv_map_nonzero {F V : Type*} [Field F]
    [AddCommGroup V] [Module F V] (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ e : V ≃ₗ[F] V, e x = y := by
…
  22. abbrev OAI.MaxCutGames.Gadget.Enlargement.LinearInjection line 321
  23. theorem OAI.MaxCutGames.Gadget.Enlargement.linearInjection_nonempty_of_finrank_le line 325
  24. def OAI.MaxCutGames.Gadget.Enlargement.postcompose line 335

    Source documentation

    Postcomposition permutes all linear injections, including their uniform finite distribution.

    def postcompose {F B K : Type*} [Field F] [AddCommGroup B] [Module F B]
    [AddCommGroup K] [Module F K] (e : K ≃ₗ[F] K) :
    LinearInjection F B K ≃ LinearInjection F B K where
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection

  25. theorem OAI.MaxCutGames.Gadget.Enlargement.injection_eval_ne_zero line 349
  26. theorem OAI.MaxCutGames.Gadget.Enlargement.exists_injection_hitting_nonzero line 360

    Source documentation

    Every nonzero target vector is hit by an injection at any prescribed nonzero base vector. This is the surjectivity ingredient of the product-shift map used before taking the quotient.

    theorem exists_injection_hitting_nonzero {F B K : Type*} [Field F]
    [AddCommGroup B] [Module F B] [FiniteDimensional F B]
    [AddCommGroup K] [Module F K] [FiniteDimensional F K]
    (h : Module.finrank F B ≤ Module.finrank F K)
    (b : B) (hb : b ≠ 0) (x : K) (hx : x ≠ 0) :
    ∃ L : LinearInjection F B K, L.1 b = x := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection

  27. def OAI.MaxCutGames.Gadget.Enlargement.productShift line 372

    Source documentation

    The product-shift map before the final quotient.

    def productShift {F B K : Type*} [Field F] [AddCommGroup B] [Module F B]
    [AddCommGroup K] [Module F K] [Fintype (LinearInjection F B K)] :
    (LinearInjection F B K → B) →ₗ[F] K where
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection

  28. theorem OAI.MaxCutGames.Gadget.Enlargement.productShift_surjective line 379
  29. def OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput line 395

    Source documentation

    Sum of the injectively relabeled base outputs before quotienting.

    def enlargedOutput {F B K V : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [Fintype (LinearInjection F B K)] (C : V → B)
    (x : LinearInjection F B K → V) : K := ∑ L : LinearInjection F B K, L.1 (C (x L))

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection

  30. theorem OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput_shift line 401

    Source documentation

    Equivariance of the nonlinear sum under the full product of base shifts.

    theorem enlargedOutput_shift {F B K V : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [AddCommGroup V] [Module F V] [Fintype (LinearInjection F B K)]
    (C : V → B) (i : B →ₗ[F] V)
    (hC : ∀ x b, C (x + i b) = C x + b)
    (x : LinearInjection F B K → V) (b : LinearInjection F B K → B) :
    enlargedOutput C (fun L => x L + i (b L)) =
      enlargedOutput C x + productShift b := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection, OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput, OAI.MaxCutGames.Gadget.Enlargement.productShift

  31. theorem OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput_update line 414

    Source documentation

    Updating only one copy changes the output by its relabeled base-output difference. This identity retains all summands and does not assume they are independent.

    theorem enlargedOutput_update {F B K V : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [Fintype (LinearInjection F B K)] (C : V → B)
    (x : LinearInjection F B K → V) (L : LinearInjection F B K) (y : V) :
    enlargedOutput C (Function.update x L y) =
      enlargedOutput C x + L.1 (C y - C (x L)) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection, OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput

  32. theorem OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput_update_ne_iff line 436

    Source documentation

    Injectivity of the selected relabeling makes the enlargement output change exactly when that copy's base output changes.

    theorem enlargedOutput_update_ne_iff {F B K V : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [Fintype (LinearInjection F B K)] (C : V → B)
    (x : LinearInjection F B K → V) (L : LinearInjection F B K) (y : V) :
    enlargedOutput C (Function.update x L y) ≠ enlargedOutput C x ↔ C y ≠ C (x L) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection, OAI.MaxCutGames.Gadget.Enlargement.enlargedOutput

  33. theorem OAI.MaxCutGames.Gadget.Enlargement.injection_eval_uniform line 444
  34. theorem OAI.MaxCutGames.Gadget.Enlargement.pullback_ne_top_iff line 477

    Source documentation

    Failure of the pullback family to span the full dual has a nonzero vector witness in its common annihilator.

    theorem pullback_ne_top_iff {F B K : Type*} [Field F] [AddCommGroup B]
    [Module F B] [FiniteDimensional F B] [AddCommGroup K] [Module F K]
    (L : B →ₗ[F] K) (S : Submodule F (Module.Dual F K)) :
    S.map L.dualMap ≠ ⊤ ↔ ∃ b : B, b ≠ 0 ∧ L b ∈ S.dualCoannihilator := by
…
  35. theorem OAI.MaxCutGames.Gadget.Enlargement.nonzero_density_le line 514

    Source documentation

    The nonzero part of a codimension-r subspace has density at most 2⁻ʳ among all nonzero ambient vectors. The dimensions are written additively to avoid truncated subtraction.

    theorem nonzero_density_le (d r : ℕ) (h : 0 < d + r) :
    ((2 : ℚ) ^ d - 1) / ((2 : ℚ) ^ (d + r) - 1) ≤ 1 / (2 : ℚ) ^ r := by
…
  36. theorem OAI.MaxCutGames.Gadget.Enlargement.card_nonzero_binary line 523

    Source documentation

    Cardinality of all nonzero vectors in a finite binary vector space.

    theorem card_nonzero_binary (K : Type*) [AddCommGroup K] [Module (ZMod 2) K]
    [Fintype K] :
    Nat.card {x : K // x ≠ 0} = 2 ^ Module.finrank (ZMod 2) K - 1 := by
…
  37. theorem OAI.MaxCutGames.Gadget.Enlargement.probability_nonzero_subspace line 531

    Source documentation

    Exact density of the nonzero part of a binary subspace.

    theorem probability_nonzero_subspace (K : Type*) [AddCommGroup K]
    [Module (ZMod 2) K] [Fintype K] (W : Submodule (ZMod 2) K) :
    probability (fun x : {x : K // x ≠ 0} => x.1 ∈ W) =
      ((2 : ℚ) ^ Module.finrank (ZMod 2) W - 1) /
        ((2 : ℚ) ^ Module.finrank (ZMod 2) K - 1) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.probability

  38. theorem OAI.MaxCutGames.Gadget.Enlargement.probability_annihilator_le line 557

    Source documentation

    The annihilator dimension identity gives precisely the exponent needed by the enlargement, without any loss depending on the ambient dimension.

    theorem probability_annihilator_le (K : Type*) [AddCommGroup K]
    [Module (ZMod 2) K] [Fintype K] [FiniteDimensional (ZMod 2) K]
    (S : Submodule (ZMod 2) (Module.Dual (ZMod 2) K))
    (hK : 0 < Module.finrank (ZMod 2) K) :
    probability (fun x : {x : K // x ≠ 0} => x.1 ∈ S.dualCoannihilator) ≤
      1 / (2 : ℚ) ^ Module.finrank (ZMod 2) S := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.probability

  39. theorem OAI.MaxCutGames.Gadget.Enlargement.union_bound_le_quarter line 570

    Source documentation

    The threshold b + 2 is chosen before the ambient dimension.

    theorem union_bound_le_quarter (b r : ℕ) (hr : b + 2 ≤ r) :
    ((2 : ℚ) ^ b - 1) / (2 : ℚ) ^ r ≤ 1 / 4 := by
…
  40. theorem OAI.MaxCutGames.Gadget.Enlargement.pullback_failure_probability_le line 581

    Source documentation

    The enlargement's uniform-injection union bound, including its actual linear-algebraic bad event.

    theorem pullback_failure_probability_le {B K : Type*}
    [AddCommGroup B] [Module (ZMod 2) B] [Fintype B]
    [FiniteDimensional (ZMod 2) B]
    [AddCommGroup K] [Module (ZMod 2) K] [Fintype K]
    [FiniteDimensional (ZMod 2) K]
    [Fintype (LinearInjection (ZMod 2) B K)]
    [Nonempty (LinearInjection (ZMod 2) B K)]
    (S : Submodule (ZMod 2) (Module.Dual (ZMod 2) K))
    (hK : 0 < Module.finrank (ZMod 2) K) :
    probability (fun L : LinearInjection (ZMod 2) B K => S.map L.1.dualMap ≠ ⊤) ≤
      ((2 : ℚ) ^ Module.finrank (ZMod 2) B - 1) /
        (2 : ℚ) ^ Module.finrank (ZMod 2) S := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection, OAI.MaxCutGames.Gadget.Enlargement.probability

  41. theorem OAI.MaxCutGames.Gadget.Enlargement.pullback_failure_probability_le_quarter line 622

    Source documentation

    At least three quarters of the injection copies restrict onto the full base dual when the restriction rank is at least dim B + 2.

    theorem pullback_failure_probability_le_quarter {B K : Type*}
    [AddCommGroup B] [Module (ZMod 2) B] [Fintype B]
    [FiniteDimensional (ZMod 2) B]
    [AddCommGroup K] [Module (ZMod 2) K] [Fintype K]
    [FiniteDimensional (ZMod 2) K]
    [Fintype (LinearInjection (ZMod 2) B K)]
    [Nonempty (LinearInjection (ZMod 2) B K)]
    (S : Submodule (ZMod 2) (Module.Dual (ZMod 2) K))
    (hr : Module.finrank (ZMod 2) B + 2 ≤ Module.finrank (ZMod 2) S) :
    probability (fun L : LinearInjection (ZMod 2) B K => S.map L.1.dualMap ≠ ⊤) ≤
      1 / 4 := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.LinearInjection, OAI.MaxCutGames.Gadget.Enlargement.probability

  42. theorem OAI.MaxCutGames.Gadget.Enlargement.probability_not line 637
  43. theorem OAI.MaxCutGames.Gadget.Enlargement.average_detection_lower_bound line 653

    Source documentation

    Averaging a nonnegative detection rate which is at least one quarter on each good copy. This is the last finite probability step of enlargement.

    theorem average_detection_lower_bound {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (bad : Ω → Prop) (detected : Ω → ℚ)
    (hnonneg : ∀ x, 0 ≤ detected x)
    (hgood : ∀ x, ¬bad x → 1 / 4 ≤ detected x) :
    (1 - probability bad) * (1 / 4) ≤
      (∑ x, detected x) / (Fintype.card Ω : ℚ) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Enlargement.probability

  44. theorem OAI.MaxCutGames.Gadget.Enlargement.detection_constants line 681

    Source documentation

    The enlargement retains 3/16 detection, and hence the advertised 1/8. The hypotheses are the bad-copy probability and the average lower bound from the base gadget; they make no independence assertion.

    theorem detection_constants {bad detected : ℚ} (hbad : bad ≤ 1 / 4)
    (hdetected : (1 - bad) * (1 / 4) ≤ detected) :
    3 / 16 ≤ detected ∧ 1 / 8 ≤ detected := by
…
  45. theorem OAI.MaxCutGames.Gadget.Enlargement.enlarged_detection line 686
  46. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_equiv line 716
  47. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_eq_sum_indicator line 723
  48. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_prod_average line 734

    Source documentation

    Uniform probability on a product is the average of the second-coordinate probabilities. No nonemptiness hypotheses are needed for this identity.

    theorem probability_prod_average {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]
    (p : Ω → Ξ → Prop) :
    probability (fun z : Ω × Ξ => p z.1 z.2) =
      (∑ x : Ω, probability (p x)) / (Fintype.card Ω : ℚ) := by
…
  49. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_prod_average_right line 746

    Source documentation

    The same product identity, averaging in the other order.

    theorem probability_prod_average_right {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]
    (p : Ω → Ξ → Prop) :
    probability (fun z : Ω × Ξ => p z.1 z.2) =
      (∑ y : Ξ, probability (fun x : Ω => p x y)) /
        (Fintype.card Ξ : ℚ) := by
…
  50. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_coordinate line 758

    Source documentation

    Every coordinate of a uniformly chosen function has the uniform marginal. Pointwise transpositions biject the evaluation fibers.

    theorem probability_coordinate {I X : Type*} [Fintype I] [Fintype X]
    (i : I) (p : X → Prop) :
    probability (fun g : I → X => p (g i)) = probability p := by
…
  51. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_coordinate_prod line 788

    Source documentation

    Coordinate projection preserves the joint uniform law with an independent finite noise sample.

    theorem probability_coordinate_prod {I X N : Type*}
    [Fintype I] [Fintype X] [Fintype N] (i : I) (p : X → N → Prop) :
    probability (fun z : (I → X) × N => p (z.1 i) z.2) =
      probability (fun z : X × N => p z.1 z.2) := by
…
  52. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_prod_reorder line 800

    Source documentation

    Grouping the same three uniform choices in another order.

    theorem probability_prod_reorder {Ω I N : Type*}
    [Fintype Ω] [Fintype I] [Fintype N] (p : Ω → I → N → Prop) :
    probability (fun z : Ω × (I × N) => p z.1 z.2.1 z.2.2) =
      probability (fun z : I × (Ω × N) => p z.2.1 z.1 z.2.2) := by
…
  53. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_prod_eq_of_const line 813

    Source documentation

    If each conditional probability is the same, their uniform average is that common value.

    theorem probability_prod_eq_of_const {Ω Ξ : Type*}
    [Fintype Ω] [Fintype Ξ] [Nonempty Ω]
    (p : Ω → Ξ → Prop) (q : ℚ) (h : ∀ x, probability (p x) = q) :
    probability (fun z : Ω × Ξ => p z.1 z.2) = q := by
…
  54. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.enlarged_single_copy_probability line 826

    Source documentation

    For a fixed selected injection, the enlargement's change event has exactly the base input/noise probability.

    theorem enlarged_single_copy_probability {F B K V N : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [AddCommGroup V] [Fintype V] [Fintype N]
    [Fintype (LinearInjection F B K)]
    (C : V → B) (a : N → V) (L : LinearInjection F B K) :
    probability (fun z : (LinearInjection F B K → V) × N =>
      enlargedOutput C (Function.update z.1 L (z.1 L + a z.2)) ≠
        enlargedOutput C z.1) =
      probability (fun z : V × N => C (z.1 + a z.2) ≠ C z.1) := by
…
  55. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.enlarged_random_copy_probability line 845

    Source documentation

    The same equality after selecting the injection uniformly as part of the noise sample. Its sample space is exactly product-input × (copy × base-noise).

    theorem enlarged_random_copy_probability {F B K V N : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [AddCommGroup V] [Fintype V] [Fintype N]
    [Fintype (LinearInjection F B K)] [Nonempty (LinearInjection F B K)]
    (C : V → B) (a : N → V) :
    probability (fun z : (LinearInjection F B K → V) ×
        (LinearInjection F B K × N) =>
      enlargedOutput C
        (Function.update z.1 z.2.1 (z.1 z.2.1 + a z.2.2)) ≠
          enlargedOutput C z.1) =
      probability (fun z : V × N => C (z.1 + a z.2) ≠ C z.1) := by
…
  56. abbrev OAI.MaxCutGames.Gadget.EnlargementConstruction.Copies line 873
  57. def OAI.MaxCutGames.Gadget.EnlargementConstruction.copiesFintype line 879

    Source documentation

    A concrete finite enumeration exists because an injection is determined by its finite function table.

    noncomputable def copiesFintype : Fintype (Copies B K) :=
…

    Mentions: OAI.MaxCutGames.Gadget.EnlargementConstruction.Copies

  58. def OAI.MaxCutGames.Gadget.EnlargementConstruction.productEmbed line 887
  59. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.productEmbed_injective line 894
  60. def OAI.MaxCutGames.Gadget.EnlargementConstruction.productStage line 903

    Source documentation

    The product before the quotient. Its finite noise sampler first chooses an injection uniformly, then independently chooses the original base noise.

    def productStage (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) : Stage (ZMod 2) K := by
…

    Mentions: OAI.MaxCutGames.Gadget.Stage

  61. def OAI.MaxCutGames.Gadget.EnlargementConstruction.build line 921

    Source documentation

    The final finite gadget, with K embedded as its actual shift space.

    def build (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) : Stage (ZMod 2) K :=
…

    Mentions: OAI.MaxCutGames.Gadget.Stage

  62. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.update_canonical line 927
  63. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_pointwise line 933
  64. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.add_single_eq_update line 940
  65. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.change_iff line 950

    Source documentation

    The quotient and injection preserve each individual nonlinear change event exactly, before taking any finite averages.

    theorem change_iff (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) (x : Copies B K → V) (L : Copies B K) (n : N) :
    let s := productStage i hi C hC noise hdim b₀ hb₀
…

    Mentions: OAI.MaxCutGames.Gadget.EnlargementConstruction.Copies, OAI.MaxCutGames.Gadget.EnlargementConstruction.productStage

  66. def OAI.MaxCutGames.Gadget.EnlargementConstruction.copyObserver line 968

    Source documentation

    Restriction of a linear observer on the quotient to one base-input copy.

    def copyObserver {E : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    (T : StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀) →ₗ[ZMod 2] E)
    (L : Copies B K) : V →ₗ[ZMod 2] E :=
…

    Mentions: OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.EnlargementConstruction.productStage, OAI.MaxCutGames.Gadget.EnlargementConstruction.Copies

  67. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.copyObserver_shift line 978
  68. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.dual_pullback_eq_top_iff line 1005
  69. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.detection_average line 1013

    Source documentation

    Average detection over the actual injection-indexed base copies. The restriction threshold is the rank on the final embedded logical space.

    theorem detection_average {E : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    (hbase : ∀ U : V →ₗ[ZMod 2] E, Function.Injective (U.comp i) →
      1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0))
    (T : StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀) →ₗ[ZMod 2] E)
    (hr : Module.finrank (ZMod 2) B + 2 ≤ Module.finrank (ZMod 2)
      (LinearMap.range (T.comp (StageQuotient.shift
        (productStage i hi C hC noise hdim b₀ hb₀))))) :
    1 / 8 ≤
…

    Mentions: OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.EnlargementConstruction.productStage, OAI.MaxCutGames.Gadget.StageQuotient.shift

  70. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_projection line 1042

    Source documentation

    Passing uniform input through the actual quotient preserves its law.

    theorem probability_projection (s : Stage (ZMod 2) K)
    [Fintype s.Input] [Fintype (StageQuotient.Space s)]
    (p : StageQuotient.Space s → Prop) :
    probability (fun x : s.Input => p (StageQuotient.projection s x)) = probability p := by
…

    Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.StageQuotient.projection

  71. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.probability_projection_prod line 1053
  72. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.change_probability line 1067

    Source documentation

    Nonlinear change probability is exactly the base probability after both the single-copy enlargement and quotient, on uniform quotient input.

    theorem change_probability (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    [Fintype (StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀))] :
    let s := productStage i hi C hC noise hdim b₀ hb₀
…

    Mentions: OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.EnlargementConstruction.productStage

  73. theorem OAI.MaxCutGames.Gadget.EnlargementConstruction.detection_probability line 1106

    Source documentation

    The final noise sample is the actual product sampler and meets the stated rank-detection bound. No detection premise about the enlarged gadget is assumed.

    theorem detection_probability {E : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    (hbase : ∀ U : V →ₗ[ZMod 2] E, Function.Injective (U.comp i) →
      1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0))
    (T : StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀) →ₗ[ZMod 2] E)
    (hr : Module.finrank (ZMod 2) B + 2 ≤ Module.finrank (ZMod 2)
      (LinearMap.range (T.comp (StageQuotient.shift
        (productStage i hi C hC noise hdim b₀ hb₀))))) :
    1 / 8 ≤ probability (fun t : Copies B K × N =>
…

    Mentions: OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.EnlargementConstruction.productStage, OAI.MaxCutGames.Gadget.StageQuotient.shift, OAI.MaxCutGames.Gadget.EnlargementConstruction.Copies