OAI/Computability/MaxCut/PCP/Game.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

The actual numbered equation list has exactly the acceptance bounded by the private Fourier decoder. Only the repeated base-game value is an input here; list semantics and all finite sampling laws are supplied.

  1. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.event_nonempty line 15
  2. def OAI.MaxCutGames.Foundations.Hastad.SourceGame.eventLaw line 19
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceGame.visibleQuestion line 24
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceGame.baseGame line 28
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.baseGame_accepts line 33
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.eventLaw_probability line 37
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.sum_slots line 50
  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.sum_slot_accepts line 60
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 74
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.failureCount_allIndices line 82
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 91

    Source documentation

    The local three-slot rejection inequality controls the actual uniform incidence law, including repeated variable names and repeated clauses.

    theorem verifier_probability_plus_failure (F : Formula) (hne : F.clauses ≠ [])
    (alice : AliceStrategy F) (bob : BobStrategy F) :
    (eventLaw F hne).probability (accepts F alice bob) +
      (failureCount F bob (allIndices F) : ℝ) / (3 * F.clauses.length : ℕ) ≤ 1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGame.eventLaw

  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.base_success_le_verifier line 112
  13. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 123

    Source documentation

    A concrete clause-count gap supplies the base-game value bound.

    theorem base_value_le_of_clause_gap (F : Formula) (hne : F.clauses ≠ [])
    (δ : ℝ) (hgap : ∀ bob : BobStrategy F,
      δ * F.clauses.length ≤ (failureCount F bob (allIndices F) : ℝ)) :
    (baseGame F hne).value ≤ 1 - δ / 3 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGame.baseGame

  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.pushforward_comp line 143
  15. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.expectation_pushforward line 158
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceGame.repeatedVisible line 169
  17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.repeated_questions line 176

    Source documentation

    This identifies the repeated game law with the actual uniformly sampled incidence tuples, retaining all collisions of their visible questions.

    theorem repeated_questions (F : Formula) (hne : F.clauses ≠ []) (u : ℕ) :
    ((baseGame F hne).repetition u).questions =
      ((eventLaw F hne).iid u).pushforward (repeatedVisible F u) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGame.baseGame, OAI.MaxCutGames.Foundations.Hastad.SourceGame.eventLaw, OAI.MaxCutGames.Foundations.Hastad.SourceGame.repeatedVisible

  18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.repeated_expectation line 185
  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.repeated_expectation_split line 198

    Source documentation

    The concrete constructor enumerates clause tuples and slot tuples as separate lexicographic factors; this is exactly the same question law.

    theorem repeated_expectation_split (F : Formula) (hne : F.clauses ≠ []) (u : ℕ)
    (H : VariableContext F u × ClauseContext F u → ℝ) :
    ((baseGame F hne).repetition u).questions.expectation H =
      𝔼 c : ClauseContext F u, 𝔼 s : SlotContext u,
        H (sampledVariables F c s, c) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGame.baseGame

  20. def OAI.MaxCutGames.Foundations.Hastad.SourceGame.sourceProjectionGame line 212
  21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.projection_value_le_repetition line 219

    Source documentation

    The projection game has exactly the repeated question law, and its legal right answers satisfy every coordinate of the original game.

    theorem projection_value_le_repetition (F : Formula) (hne : F.clauses ≠ [])
    (u : ℕ) :
    (sourceProjectionGame F hne u).value ≤ ((baseGame F hne).repetition u).value := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGame.sourceProjectionGame, OAI.MaxCutGames.Foundations.Hastad.SourceGame.baseGame

  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.source_acceptance_le line 238
  23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGame.source_acceptance_le_split line 253
  24. def OAI.MaxCutGames.Foundations.Hastad.SourceSoundness.leftTable line 280
  25. def OAI.MaxCutGames.Foundations.Hastad.SourceSoundness.rightOracle line 284
  26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSoundness.rightOracle_answer line 292
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSoundness.leftTable_answer line 298
  28. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSoundness.sourceList_sound line 304

    Source documentation

    Exact finite occurrence-list soundness, including arbitrary assignments to unused padded proof bits and to the dummy bit.

    theorem sourceList_sound (F : Formula) (hne : F.clauses ≠ []) (u D : ℕ)
    (hD : 0 < D) (hDtwo : 2 ≤ D) (δ : ℝ) (hδ : 0 ≤ δ)
    (hvalue : ((baseGame F hne).repetition u).value ≤
      4 * (D : ℝ)⁻¹ * δ ^ 2)
    (bits : Fin (nBits F u) → Bool) :
    ((sourceList F u D).countP (fun e => MaxCutGames.Reduction.CloneGap.satisfied e bits) : ℝ) /
      (sourceList F u D).length ≤ (1 + δ) / 2 := by
…

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.satisfied

  29. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSoundness.sourceList_sound_rat line 323

    Source documentation

    The direct uniform reduction consumes rational occurrence fractions.

    theorem sourceList_sound_rat (F : Formula) (hne : F.clauses ≠ []) (u D : ℕ)
    (hD : 0 < D) (hDtwo : 2 ≤ D) (δ : ℚ) (hδ : 0 ≤ δ)
    (hvalue : ((baseGame F hne).repetition u).value ≤
      4 * (D : ℝ)⁻¹ * (δ : ℝ) ^ 2)
    (bits : Fin (nBits F u) → Bool) :
    ((sourceList F u D).countP (fun e => MaxCutGames.Reduction.CloneGap.satisfied e bits) : ℚ) /
      (sourceList F u D).length ≤ (1 + δ) / 2 := by
…

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.satisfied

  30. def OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment line 348

    Source documentation

    Padded query tables are evaluated at one coordinate per context. Left and right tables have disjoint tags, and the unused dummy bit is fixed to false.

    def taggedAssignment {V C I J : Type} (left : V → I) (right : C → J) :
    (V × Cube I) ⊕ ((C × Cube J) ⊕ Unit) → Bool
  | .inl (v, f) => f (left v)
  | .inr (.inl (c, g)) => g (right c)
  | .inr (.inr _) => false

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube

  31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment_left line 354
  32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment_right line 358
  33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment_right_restriction line 364

    Source documentation

    Extending a conditioned half-table into padded ambient storage does not change its honest bit. Only correctness on valid coordinates is required.

    theorem taggedAssignment_right_restriction {V C I J : Type}
    (left : V → I) (right : C → J) (c : C) (valid : J → Bool)
    (honest : {j : J // valid j = true}) (hright : right c = honest.val)
    (extend : Cube {j : J // valid j = true} → Cube J)
    (hextend : ∀ (g : Cube {j : J // valid j = true})
      (j : {j : J // valid j = true}), extend g j.val = g j)
    (j₀ : {j : J // valid j = true}) (h : HalfCube j₀) :
    taggedAssignment left right (.inr (.inl (c, extend h.val))) = h.val honest := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment

  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.conditioned_equation_honest_satisfied line 383

    Source documentation

    Each honest emitted equation fails exactly when its selected noise bit is true. This is a pointwise statement, before averaging any random tape.

    theorem conditioned_equation_honest_satisfied
    (valid : J → Bool) (π : J → I) (i₀ i : I)
    (j₀ j : {j : J // valid j = true}) (hπ : π j.val = i)
    (f : Cube I) (g μ : Cube J) :
    satisfied (FoldedEquation.conditionedEquation valid π i₀ j₀ f g μ)
        (FoldedEquation.storedAssignment (fun h => h.val i) (fun h => h.val j)) =
      !(μ j.val) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.storedAssignment

  35. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.mapped_conditioned_equation_honest_satisfied line 397

    Source documentation

    Local table equalities are enough to reuse the same assignment even when different occurrences, contexts, or query positions name the same proof bit.

    theorem mapped_conditioned_equation_honest_satisfied {Name : Type}
    (valid : J → Bool) (π : J → I) (i₀ i : I)
    (j₀ j : {j : J // valid j = true}) (hπ : π j.val = i)
    (rename : FoldedEquation.Address i₀ j₀ → Name) (assignment : Name → Bool)
    (hleft : ∀ h, assignment (rename (.inl h)) = h.val i)
    (hright : ∀ h, assignment (rename (.inr h)) = h.val j)
    (f : Cube I) (g μ : Cube J) :
    satisfied (mapEquation rename
        (FoldedEquation.conditionedEquation valid π i₀ j₀ f g μ)) assignment =
      !(μ j.val) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.Address, OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.mapEquation, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation

  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.tapeAcceptance_conditioned_dictators line 418

    Source documentation

    The exact finite noise law gives honest acceptance for a conditioned right table and an unconditioned left table, with arbitrary fixed folding bases.

    theorem tapeAcceptance_conditioned_dictators {D : ℕ} (positive : 0 < D)
    (valid : J → Bool) (π : J → I) (i₀ i : I)
    (j₀ j : {j : J // valid j = true}) (hπ : π j.val = i) :
    SourceTape.tapeAcceptance D π
      (foldedAnswer i₀ (fun h => h.val i))
      (conditionedFoldedAnswer valid j₀ (fun h => h.val j)) =
        1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeAcceptance, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer, OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer

  37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 438

    Source documentation

    Numbering the global proof and then restricting it to one local table recovers exactly the local honest half-tables.

    theorem numbered_assignment_restriction
    (vE : Encoding V) (cE : Encoding C) (iE : Encoding I) (jE : Encoding J)
    (left : V → I) (right : C → J) (v : V) (c : C)
    (valid : J → Bool) (i₀ : I) (j₀ j : {j : J // valid j = true})
    (hright : right c = j.val) :
    assignmentOfKey vE cE iE jE (taggedAssignment left right) ∘
      localAddress vE cE iE jE v c valid i₀ j₀ =
      FoldedEquation.storedAssignment (fun h => h.val (left v)) (fun h => h.val j) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.storedAssignment

  38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 461

    Source documentation

    The globally numbered honest proof satisfies each actual occurrence precisely when the corresponding noise bit is false.

    theorem conditionedOccurrence_honest_satisfied
    (vE : Encoding V) (cE : Encoding C) (iE : Encoding I) (jE : Encoding J)
    (left : V → I) (right : C → J) (v : V) (c : C)
    (valid : J → Bool) (π : J → I) (i₀ : I)
    (j₀ j : {j : J // valid j = true})
    (hright : right c = j.val) (hπ : π j.val = left v)
    (f : Cube I) (g μ : Cube J) :
    satisfied (conditionedOccurrence vE cE iE jE v c valid π i₀ j₀ f g μ)
      (assignmentOfKey vE cE iE jE (taggedAssignment left right)) = !(μ j.val) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.SourceHonest.taggedAssignment

  39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 476

    Source documentation

    Exact normalized accepted count for the actual ordered random-tape list at one incidence context. Equal equations remain separate occurrences.

    theorem conditionedOccurrenceList_honest_acceptance {D : ℕ} (positive : 0 < D)
    (vE : Encoding V) (cE : Encoding C) (iE : Encoding I) (jE : Encoding J)
    (left : V → I) (right : C → J) (v : V) (c : C)
    (valid : J → Bool) (π : J → I) (i₀ : I)
    (j₀ j : {j : J // valid j = true})
    (hright : right c = j.val) (hπ : π j.val = left v)
    (tape : Encoding (SourceTape.TestTape I J D)) :
    let equations := occurrenceList tape (fun t =>
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape

  40. def OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestGlobal line 510

    Source documentation

    A single assignment to the globally tagged padded tables. It is defined from the input assignment alone, before any incidence or test is sampled.

    def honestGlobal (F : Target.Formula) (u : ℕ)
    (assignment : Fin F.«variables» → Bool) :
    (VariableContext F u × Cube (I u)) ⊕
      ((ClauseContext F u × Cube (J u)) ⊕ Unit) → Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.Cube

  41. def OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits line 517

    Source documentation

    The same global proof in the construction's explicit radix numbering.

    def honestBits (F : Target.Formula) (u : ℕ)
    (assignment : Fin F.«variables» → Bool) : Fin (nBits F u) → Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula

  42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits_code line 522
  43. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits_dummy line 530
  44. def OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestValidJ line 538

    Source documentation

    Satisfiability supplies one consistent valid right coordinate in every clause tuple, including tuples with repeated clauses or variable names.

    def honestValidJ (F : Target.Formula) {u : ℕ} (c : ClauseContext F u)
    (assignment : Fin F.«variables» → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true) :
    {j : J u // validJ F c j = true} :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula

  45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 544
  46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.leftResponse_honest line 550
  47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.rightResponse_honest line 558
  48. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 583

    Source documentation

    Actual sampled incidence contexts attain the same honest finite-noise acceptance. Folding bases may be chosen independently of the assignment.

    theorem context_tapeAcceptance {D : ℕ} (positive : 0 < D)
    (F : Target.Formula) {u : ℕ} (c : ClauseContext F u) (s : SlotContext u)
    (assignment : Fin F.«variables» → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true)
    (i₀ : I u) (j₀ : {j : J u // validJ F c j = true}) :
    SourceTape.tapeAcceptance D (pi F c (sampledVariables F c s))
      (foldedAnswer i₀ (fun h => h.val (honestI F (sampledVariables F c s) assignment)))
      (conditionedFoldedAnswer (validJ F c) j₀
        (fun h => h.val (honestValidJ F c assignment hs))) =
      1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeAcceptance, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer, OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer, OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestValidJ

  49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 599

    Source documentation

    The emitted equation, under the one global honest assignment, reads the noise coordinate corresponding to the honest tuple of clause answers.

    theorem sourceEquation_honest_satisfied (F : Target.Formula) (u D : ℕ)
    (assignment : Fin F.«variables» → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true)
    (p : SourceIndex F u D) :
    satisfied (sourceEquation F u D p) (honestBits F u assignment) =
      !(realizedNoise p.2.2.1 (honestJ F p.1.1 assignment)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits

  50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 611

    Source documentation

    Every actual occurrence is counted, even when its visible context, equation, or one of its three addresses repeats.

    theorem rawSourceList_honest_acceptance (F : Target.Formula) (u D : ℕ)
    (hD : 0 < D) (hF : F.clauses ≠ [])
    (assignment : Fin F.«variables» → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true) :
    ((rawSourceList F u D).countP
      (fun e => satisfied e (honestBits F u assignment)) : ℝ) /
        (rawSourceList F u D).length = 1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits

  51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 630
  52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 640
  53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 655

    Source documentation

    Rational acceptance form used by the finite reduction interface.

    theorem sourceList_honest_acceptance_rat (F : Target.Formula) (u D : ℕ)
    (hD : 0 < D) (assignment : Fin F.«variables» → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true) :
    1 - (D : ℚ)⁻¹ ≤ ((sourceList F u D).countP
      (fun e => satisfied e (honestBits F u assignment)) : ℚ) /
        (sourceList F u D).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceHonest.honestBits

  54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 665
  55. def OAI.MaxCutGames.Foundations.Repetition.logTwo line 680
  56. theorem OAI.MaxCutGames.Foundations.Repetition.logTwo_one line 682
  57. theorem OAI.MaxCutGames.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 684
  58. theorem OAI.MaxCutGames.Foundations.Repetition.contraction_step line 697

    Source documentation

    A nonzero step below the cutoff contracts by (1+v)/2.

    theorem contraction_step {v ell : ℝ} {n m : ℕ} {p next : ℝ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hm : 1 ≤ m) (hmn : m < n) (hp : 0 ≤ p)
    (hmono : next ≤ p)
    (hprev : p ≤ ((1 + v) / 2) ^ m)
    (hcut : 2700 * (m : ℝ) * ell ≤ (1 - v) ^ 2 * ((n : ℝ) - m))
    (hstep : next ≤ p * (v + 15 * Real.sqrt
      (((m : ℝ) * ell + logTwo (1 / p)) / ((n : ℝ) - m)))) :
    next ≤ ((1 + v) / 2) ^ (m + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.logTwo

  59. theorem OAI.MaxCutGames.Foundations.Repetition.initial_step line 737

    Source documentation

    The m=0 case does not use the estimate m+1 ≤ 2*m*ell.

    theorem initial_step {v ell next : ℝ} {n : ℕ}
    (hstep : next ≤ 1 * (v + 15 * Real.sqrt
      (((0 : ℝ) * ell + logTwo (1 / 1)) / ((n : ℝ) - 0)))) :
    next ≤ v := by simpa using hstep

    Mentions: OAI.MaxCutGames.Foundations.Repetition.logTwo

  60. theorem OAI.MaxCutGames.Foundations.Repetition.cutoff_step line 743

    Source documentation

    A real cutoff gives a valid step at every integer strictly below it.

    theorem cutoff_step {v ell : ℝ} {n m : ℕ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hm : (m : ℝ) < (n : ℝ) * (1 - v) ^ 2 / (2925 * ell)) :
    2700 * (m : ℝ) * ell ≤ (1 - v) ^ 2 * ((n : ℝ) - m) := by
…
  61. theorem OAI.MaxCutGames.Foundations.Repetition.cutoff_le_length line 755
  62. def OAI.MaxCutGames.Foundations.Repetition.ScalarRecurrence line 764

    Source documentation

    The explicit recurrence obtained from a 15*sqrt embedding error.

    def ScalarRecurrence (p : ℕ → ℝ) (n : ℕ) (v ell : ℝ) : Prop :=
…
  63. theorem OAI.MaxCutGames.Foundations.Repetition.decay_to_cutoff line 770

    Source documentation

    Induction to the ceiling of the real cutoff repairs the integer-rounding omission in the printed scalar proof.

    theorem decay_to_cutoff (p : ℕ → ℝ) (n : ℕ) {v ell : ℝ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hp0 : p 0 = 1) (hpnonneg : ∀ m, 0 ≤ p m)
    (hpmono : Antitone p) (hrec : ScalarRecurrence p n v ell) :
    p n ≤ ((1 + v) / 2) ^
      ((n : ℝ) * (1 - v) ^ 2 / (2925 * ell)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.ScalarRecurrence

  64. theorem OAI.MaxCutGames.Foundations.Repetition.block_contraction line 808

    Source documentation

    The loss in one real-power block is cubic in the initial gap.

    theorem block_contraction {v : ℝ} (hv0 : 0 ≤ v) (hv1 : v < 1) :
    ((1 + v) / 2) ^ ((1 - v) ^ 2 / 2925 : ℝ) ≤
      1 - (1 - v) ^ 3 / 5850 := by
…
  65. theorem OAI.MaxCutGames.Foundations.Repetition.scalar_bound_6000 line 823

    Source documentation

    Numerical endpoint of Holenstein's recurrence, with the published constant 6000. This theorem assumes only a concrete scalar recurrence, not any game value bound. The derivation of that recurrence for games is separate.

    theorem scalar_bound_6000 (p : ℕ → ℝ) (n : ℕ) {v ell : ℝ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hp0 : p 0 = 1) (hpnonneg : ∀ m, 0 ≤ p m)
    (hpmono : Antitone p) (hrec : ScalarRecurrence p n v ell) :
    p n ≤ (1 - (1 - v) ^ 3 / 6000) ^ ((n : ℝ) / ell) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.ScalarRecurrence

  66. def OAI.MaxCutGames.Foundations.Repetition.incidenceRate line 846
  67. theorem OAI.MaxCutGames.Foundations.Repetition.incidenceRate_pos line 848
  68. theorem OAI.MaxCutGames.Foundations.Repetition.incidenceRate_lt_one line 850
  69. theorem OAI.MaxCutGames.Foundations.Repetition.incidenceRate_fourth line 853

    Source documentation

    Exact rational arithmetic verifies the fourth-power comparison.

    theorem incidenceRate_fourth :
    1 - (1 / 192 : ℝ) ^ 3 / 6000 ≤ incidenceRate ^ 4 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.incidenceRate

  70. theorem OAI.MaxCutGames.Foundations.Repetition.incidence_rate_comparison line 859

    Source documentation

    Converting the real exponent n/4 to an integral power loses only the explicit slack already built into incidenceRate.

    theorem incidence_rate_comparison (n : ℕ) :
    (1 - (1 / 192 : ℝ) ^ 3 / 6000) ^ ((n : ℝ) / 4) ≤ incidenceRate ^ n := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.incidenceRate

  71. theorem OAI.MaxCutGames.Foundations.Repetition.scalar_incidence_bound line 872

    Source documentation

    The incidence-game rate follows from its concrete scalar recurrence. The game-to-recurrence proof is deliberately not hidden in this statement.

    theorem scalar_incidence_bound (p : ℕ → ℝ) (n : ℕ) {v : ℝ}
    (hv : v ≤ 1 - (1 / 192 : ℝ))
    (hp0 : p 0 = 1) (hpnonneg : ∀ m, 0 ≤ p m)
    (hpmono : Antitone p) (hrec : ScalarRecurrence p n v 4) :
    p n ≤ incidenceRate ^ n := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.ScalarRecurrence, OAI.MaxCutGames.Foundations.Repetition.incidenceRate