OAI/Computability/MaxCut/Games/FinalParameters.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Existence of the finite numerical choices in Section 4.1. All errors and search tests here are rational, including the fourth-power test in (4.1).

  1. def OAI.MaxCutGames.Integration.FinalParameters.rho line 16
  2. def OAI.MaxCutGames.Integration.FinalParameters.levelConstant line 17
  3. def OAI.MaxCutGames.Integration.FinalParameters.alpha line 18
  4. def OAI.MaxCutGames.Integration.FinalParameters.beta line 19
  5. def OAI.MaxCutGames.Integration.FinalParameters.theta line 20
  6. def OAI.MaxCutGames.Integration.FinalParameters.repetitionRate line 21
  7. theorem OAI.MaxCutGames.Integration.FinalParameters.levelConstant_pos line 23
  8. theorem OAI.MaxCutGames.Integration.FinalParameters.rho_pos line 27
  9. theorem OAI.MaxCutGames.Integration.FinalParameters.theta_pos line 31
  10. theorem OAI.MaxCutGames.Integration.FinalParameters.repetitionRate_bounds line 36
  11. theorem OAI.MaxCutGames.Integration.FinalParameters.exists_symbol_dimension line 41

    Source documentation

    Selecting the exponent as a multiple of four supplies an exact rational fourth root. No approximation of a real root enters the parameter search.

    theorem exists_symbol_dimension (r : Nat) {δ : ℚ} (hδ : 0 < δ) :
    ∃ s : Nat, r + 1 < s ∧ ∃ u : ℚ,
      0 < u ∧ u ^ 4 = rho r s ∧ levelConstant r * u ≤ δ / 8 := by
…

    Mentions: OAI.MaxCutGames.Integration.FinalParameters.rho, OAI.MaxCutGames.Integration.FinalParameters.levelConstant

  12. theorem OAI.MaxCutGames.Integration.FinalParameters.exists_repetition_and_dimension line 59

    Source documentation

    The repetition length is chosen first; the comparison dimension is then large enough for both the subset experiment and its squared error bound.

    theorem exists_repetition_and_dimension (L q : Nat) {θ : ℚ}
    (hθ : 0 < θ) (hq : 0 < q) :
    ∃ t k : Nat, 0 < t ∧ t ≤ k ∧
      (1 - zeroProbability L * (1 - repetitionRate)) ^ t < decoderThreshold θ q ∧
      16 * (t : ℚ) ^ 2 * 2 ^ (t * L) ≤ (k : ℚ) * θ ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Integration.FinalParameters.repetitionRate

  13. def OAI.MaxCutGames.Integration.FinalParameters.gamma line 76
  14. theorem OAI.MaxCutGames.Integration.FinalParameters.gamma_bounds line 78
  15. theorem OAI.MaxCutGames.Integration.FinalParameters.exists_source_error line 88
  16. theorem OAI.MaxCutGames.Integration.FinalParameters.exists_parameters line 97
  17. theorem OAI.MaxCutGames.Integration.FinalParameters.completeness_budget line 122

    Source documentation

    The completeness budget uses the same comparison dimension as the other parameters. This identity is exact, without rounding of rational errors.

    theorem completeness_budget {ε : ℚ} {k : Nat} (hk : 0 < k) :
    (k : ℚ) * gamma ε k + (ε / 2) / 2 = ε / 2 := by
…

    Mentions: OAI.MaxCutGames.Integration.FinalParameters.gamma

  18. abbrev OAI.MaxCutGames.Gadget.ActualGadget.F2 line 138
  19. structure OAI.MaxCutGames.Gadget.ActualGadget.Data line 140
  20. def OAI.MaxCutGames.Gadget.ActualGadget.failureIndicator line 160

    Source documentation

    The actual output-change indicator before taking a finite average.

    noncomputable def failureIndicator (g : Data C) (sample : g.Ambient × g.NoiseIndex) : ℚ := by
…

    Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Data

  21. def OAI.MaxCutGames.Gadget.ActualGadget.stabilityError line 165

    Source documentation

    Uniform ambient input, independently uniform noise-list index.

    noncomputable def stabilityError (g : Data C) : ℚ :=
…

    Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Data

  22. def OAI.MaxCutGames.Gadget.ActualGadget.kernelIndicator line 169

    Source documentation

    The actual zero-image event for a linear map.

    noncomputable def kernelIndicator (g : Data C) {P : Type}
    [AddCommGroup P] [Module F2 P] (S : g.Ambient →ₗ[F2] P) (i : g.NoiseIndex) : ℚ := by
…

    Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Data, OAI.MaxCutGames.Gadget.ActualGadget.F2

  23. def OAI.MaxCutGames.Gadget.ActualGadget.kernelError line 174
  24. theorem OAI.MaxCutGames.Gadget.ActualGadget.stabilityError_nonneg line 178
  25. theorem OAI.MaxCutGames.Gadget.ActualGadget.stabilityError_le_one line 185
  26. theorem OAI.MaxCutGames.Gadget.ActualGadget.kernelError_nonneg line 192
  27. theorem OAI.MaxCutGames.Gadget.ActualGadget.kernelError_le_one line 200
  28. def OAI.MaxCutGames.Gadget.ActualGadget.leaf line 209

    Source documentation

    The actual identity leaf, with every symbol vector used once as noise.

    def leaf (C : Type) [AddCommGroup C] [Module F2 C] [Fintype C] : Data C where
…

    Mentions: OAI.MaxCutGames.Gadget.ActualGadget.F2, OAI.MaxCutGames.Gadget.ActualGadget.Data

  29. def OAI.MaxCutGames.Gadget.ActualGadget.Satisfies line 219

    Source documentation

    The stability and dispersion claim of Theorem 3.4 for fixed errors and rank.

    def Satisfies (g : Data C) (ζ ν : ℚ) (r : Nat) : Prop :=
…

    Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Data

  30. def OAI.MaxCutGames.Gadget.ActualGadget.StableNonlinearDispersion line 225

    Source documentation

    The actual mathematical existence target; no theorem asserts it yet.

    def StableNonlinearDispersion : Prop :=
…
  31. structure OAI.MaxCutGames.Reduction.ActualSource.Source line 237
  32. def OAI.MaxCutGames.Reduction.ActualSource.Source.sourceList line 243
  33. def OAI.MaxCutGames.Reduction.ActualSource.Source.ofList line 247

    Source documentation

    Retain every list position as its own occurrence identifier.

    def Source.ofList {n : Nat} (es : List (CloneGap.Equation (Fin n)))
    (hne : es ≠ []) : Source where
…

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.Equation, OAI.MaxCutGames.Reduction.ActualSource.Source

  34. theorem OAI.MaxCutGames.Reduction.ActualSource.Source.sourceList_ofList line 254
  35. theorem OAI.MaxCutGames.Reduction.ActualSource.Source.sourceList_length line 259
  36. theorem OAI.MaxCutGames.Reduction.ActualSource.Source.sourceList_nonempty line 262
  37. instance OAI.MaxCutGames.Reduction.ActualSource.sourceIndexNonempty line 270
  38. def OAI.MaxCutGames.Reduction.ActualSource.Source.satisfied line 273
  39. def OAI.MaxCutGames.Reduction.ActualSource.Source.failure line 276
  40. def OAI.MaxCutGames.Reduction.ActualSource.Source.DistinctNames line 279
  41. abbrev OAI.MaxCutGames.Reduction.ActualSource.Alphabet line 284
  42. abbrev OAI.MaxCutGames.Reduction.ActualSource.Ambient line 285
  43. def OAI.MaxCutGames.Reduction.ActualSource.alphabetEmbedding line 287
  44. theorem OAI.MaxCutGames.Reduction.ActualSource.alphabetEmbedding_apply line 290
  45. structure OAI.MaxCutGames.Reduction.ActualSource.SplitGadget line 294

    Source documentation

    Noise indices retain multiplicity even if several indices have equal vectors.

    structure SplitGadget (s d : Nat) where
…
  46. def OAI.MaxCutGames.Reduction.ActualSource.SplitGadget.stabilityError line 304
  47. def OAI.MaxCutGames.Reduction.ActualSource.SplitGadget.kernelError line 308
  48. theorem OAI.MaxCutGames.Reduction.ActualSource.SplitGadget.stabilityError_nonneg line 312
  49. theorem OAI.MaxCutGames.Reduction.ActualSource.SplitGadget.stabilityError_le_one line 318
  50. theorem OAI.MaxCutGames.Integration.SplitGadget.exists_split_equiv line 336

    Source documentation

    Any injective symbol embedding admits finite coordinates in which it is the first summand. This is a theorem about the actual ambient vector space.

    theorem exists_split_equiv {s : Nat} (e : Vector s →ₗ[F2] R)
    (he : Function.Injective e) :
    ∃ d : Nat, ∃ φ : R ≃ₗ[F2] (Vector s × Vector d),
      ∀ c, φ (e c) = (c, 0) := by
…
  51. def OAI.MaxCutGames.Integration.SplitGadget.kernelProbability line 355
  52. theorem OAI.MaxCutGames.Integration.SplitGadget.kernelProbability_eq_kernelError line 361
  53. def OAI.MaxCutGames.Integration.SplitGadget.transport line 371

    Source documentation

    Move all ambient vectors through a linear equivalence, retaining the same noise indices and their multiplicities.

    noncomputable def transport {s d : Nat} (g : Data (Vector s))
    (φ : g.Ambient ≃ₗ[F2] Ambient s d)
    (he : ∀ c, φ (g.embed c) = (c, 0)) : SplitGadget s d where
…
  54. theorem OAI.MaxCutGames.Integration.SplitGadget.transport_stabilityError line 385

    Source documentation

    Uniform stability is invariant under the coordinate change.

    theorem transport_stabilityError {s d : Nat} (g : Data (Vector s))
    (φ : g.Ambient ≃ₗ[F2] Ambient s d)
    (he : ∀ c, φ (g.embed c) = (c, 0)) :
    (transport g φ he).stabilityError = stabilityError g := by
…

    Mentions: OAI.MaxCutGames.Integration.SplitGadget.transport

  55. theorem OAI.MaxCutGames.Integration.SplitGadget.transport_kernelError line 395

    Source documentation

    Every zero-image probability is invariant under the same coordinate change.

    theorem transport_kernelError {s d p : Nat} (g : Data (Vector s))
    (φ : g.Ambient ≃ₗ[F2] Ambient s d)
    (he : ∀ c, φ (g.embed c) = (c, 0))
    (S : Ambient s d →ₗ[F2] Vector p) :
    (transport g φ he).kernelError S = kernelError g (S.comp φ.toLinearMap) := by
…

    Mentions: OAI.MaxCutGames.Integration.SplitGadget.transport

  56. theorem OAI.MaxCutGames.Integration.SplitGadget.transport_symbol_map line 406

    Source documentation

    The restriction to the symbol space is exactly the same linear map.

    theorem transport_symbol_map {s d : Nat} (g : Data (Vector s))
    (φ : g.Ambient ≃ₗ[F2] Ambient s d)
    (he : ∀ c, φ (g.embed c) = (c, 0))
    {P : Type} [AddCommGroup P] [Module F2 P]
    (S : Ambient s d →ₗ[F2] P) :
    (S.comp φ.toLinearMap).comp g.embed = S.comp (alphabetEmbedding s d) := by
…
  57. theorem OAI.MaxCutGames.Integration.SplitGadget.transport_kernelProbability line 417
  58. theorem OAI.MaxCutGames.Integration.SplitGadget.transport_satisfies line 427

    Source documentation

    Both numerical gadget guarantees survive the coordinate change.

    theorem transport_satisfies {s d : Nat} (g : Data (Vector s))
    (φ : g.Ambient ≃ₗ[F2] Ambient s d)
    (he : ∀ c, φ (g.embed c) = (c, 0))
    {ζ ν : ℚ} {r : Nat} (hg : Satisfies g ζ ν r) :
    (transport g φ he).stabilityError ≤ ζ ∧
      ∀ p (S : Ambient s d →ₗ[F2] Vector p),
        r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
        (transport g φ he).kernelError S ≤ ν := by
…

    Mentions: OAI.MaxCutGames.Integration.SplitGadget.transport

  59. theorem OAI.MaxCutGames.Integration.SplitGadget.exists_split_gadget line 445

    Source documentation

    Every actual gadget satisfying the quantitative guarantees has a split coordinate representative with exactly those guarantees.

    theorem exists_split_gadget {s : Nat} (g : Data (Vector s))
    {ζ ν : ℚ} {r : Nat} (hg : Satisfies g ζ ν r) :
    ∃ d : Nat, ∃ h : SplitGadget s d,
      h.stabilityError ≤ ζ ∧
      ∀ p (S : Ambient s d →ₗ[F2] Vector p),
        r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
        h.kernelError S ≤ ν := by
…
  60. theorem OAI.MaxCutGames.Integration.SplitGadget.exists_split_gadget_general line 457

    Source documentation

    The coordinate representative preserves dispersion for every target, including the question spaces used directly by the soundness analysis.

    theorem exists_split_gadget_general {s : Nat} (g : Data (Vector s))
    {ζ ν : ℚ} {r : Nat} (hg : Satisfies g ζ ν r) :
    ∃ d : Nat, ∃ h : SplitGadget s d,
      h.stabilityError ≤ ζ ∧
      ∀ (P : Type) [AddCommGroup P] [Module F2 P]
        (S : Ambient s d →ₗ[F2] P),
        r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
        kernelProbability h S ≤ ν := by
…

    Mentions: OAI.MaxCutGames.Integration.SplitGadget.kernelProbability

  61. theorem OAI.MaxCutGames.Integration.RealBounds.rho_eq_two_div_pow line 483
  62. theorem OAI.MaxCutGames.Integration.RealBounds.rho_real_eq_two_div_pow line 490
  63. theorem OAI.MaxCutGames.Integration.RealBounds.beta_eq_div line 494
  64. theorem OAI.MaxCutGames.Integration.RealBounds.theta_real_product line 502

    Source documentation

    The exact signal threshold used by selection, expressed in real scalars. There is no loss between the rational parameter search and this product.

    theorem theta_real_product (δ : ℚ) (r s : Nat) :
    (theta δ r s : ℝ) =
      ((δ : ℝ) / (8 * (2 : ℝ) ^ s * 2 ^ (s * s))) *
        ((rho r s : ℝ) / (2 * (2 : ℝ) ^ (r * s))) := by
…
  65. theorem OAI.MaxCutGames.Integration.RealBounds.fourth_root_as_rpow line 508
  66. theorem OAI.MaxCutGames.Integration.RealBounds.exists_symbol_dimension_real line 515
  67. theorem OAI.MaxCutGames.Integration.RealBounds.kernelProbability_real line 525

    Source documentation

    Casting the finite experiment changes only its scalar values, retaining the same noise indices and the same event.

    theorem kernelProbability_real {s d : Nat}
    (g : MaxCutGames.Reduction.ActualSource.SplitGadget s d)
    {P : Type} [AddCommGroup P] [Module F2 P] [DecidableEq P]
    (S : (Vector s × Vector d) →ₗ[F2] P) :
    (SplitGadget.kernelProbability g S : ℝ) =
      Finset.univ.expect (fun i => if S (g.noise i) = 0 then (1 : ℝ) else 0) := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualSource.SplitGadget, OAI.MaxCutGames.Integration.SplitGadget.kernelProbability

  68. theorem OAI.MaxCutGames.Integration.RealBounds.kernelProbability_real_le line 539
  69. theorem OAI.MaxCutGames.Integration.RealBounds.comparison_square_budget line 549
  70. theorem OAI.MaxCutGames.Soundness.ActualMapComparison.actual_partner_expectation_comparison line 565
  71. theorem OAI.MaxCutGames.Soundness.ActualMapComparison.actual_partner_expectation_comparison_dimension line 594
  72. theorem OAI.MaxCutGames.Soundness.ActualMapComparison.actual_partner_expectation_quarter line 613
  73. def OAI.MaxCutGames.Soundness.ActualMapComparison.sourcePrecomposeEquiv line 633
  74. theorem OAI.MaxCutGames.Soundness.ActualMapComparison.uniformMean_sourcePrecompose line 650
  75. theorem OAI.MaxCutGames.Soundness.ActualMapComparison.actual_partner_expectation_quarter_equiv line 661
  76. theorem OAI.MaxCutGames.Soundness.RawTargetLaw.partnerProjection_congr_slots line 710

    Source documentation

    The genuine partner projection reads retained slots only at active positions.

    theorem partnerProjection_congr_slots {k : Nat} (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot slot' : Fin k → Slot)
    (agree : ∀ j ∈ J, slot j = slot' j) :
    PartnerLinear.projection rhs (activeOf J) slot =
      PartnerLinear.projection rhs (activeOf J) slot' := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerLinear.projection

  77. theorem OAI.MaxCutGames.Soundness.RawTargetLaw.rawProjection_congr_slots line 720

    Source documentation

    The shared raw target also ignores every inactive retained-slot choice.

    theorem rawProjection_congr_slots {k : Nat} (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot slot' : Fin k → Slot)
    (agree : ∀ j ∈ J, slot j = slot' j) :
    RawPartnerTarget.rawProjection rhs J slot =
      RawPartnerTarget.rawProjection rhs J slot' := by
…

    Mentions: OAI.MaxCutGames.Soundness.RawPartnerTarget.rawProjection

  78. theorem OAI.MaxCutGames.Soundness.RawTargetLaw.precompose_rawProjection line 728
  79. theorem OAI.MaxCutGames.Soundness.RawTargetLaw.partner_row_column_expectation line 740

    Source documentation

    Exact nested uniform expectations in partner versus raw coordinates. Any finite enumerations of the four map spaces may be used.

    theorem partner_row_column_expectation {k : Nat} (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot : Fin k → Slot)
    {D C : Type} [AddCommGroup D] [Module F2 D] [AddCommGroup C] [Module F2 C]
    [Fintype (PartnerPoint rhs (activeOf J) →ₗ[F2] D)]
    [Fintype (PartnerPoint rhs (activeOf J) →ₗ[F2] C)]
    [Fintype (RawPoint J →ₗ[F2] D)] [Fintype (RawPoint J →ₗ[F2] C)]
    (H : (ActualHomogeneous.E k →ₗ[F2] D) →
      (ActualHomogeneous.E k →ₗ[F2] C) → ℝ) :
    (𝔼 Z : PartnerPoint rhs (activeOf J) →ₗ[F2] D,
      𝔼 X : PartnerPoint rhs (activeOf J) →ₗ[F2] C,
        let pi := (PartnerLinear.projection rhs (activeOf J) slot).comp
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerLinear.projection