OAI/Computability/MaxCut/PCP/Gap.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

An executable finite-noise denominator for a positive rational target error. Using the stored rational denominator avoids rounding, searches, and choice.

  1. def OAI.MaxCutGames.Foundations.Hastad.SourceGap.ClauseGap line 15

    Source documentation

    A clause gap includes nonemptiness: a cross-multiplied inequality alone would hold vacuously for a formula with no clauses.

    def ClauseGap (F : Formula) (η : ℚ) : Prop :=
…
  2. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.third_pos line 20
  3. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.third_le_one line 22
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceGap.repetitionCount line 26

    Source documentation

    The repetition count is computed once from the gap, target error, and noise denominator, independently of the input formula.

    def repetitionCount (η ξ : ℚ) (hη : 0 < η) (hη1 : η ≤ 1) (hξ : 0 < ξ)
    (D : ℕ) (hD : 0 < D) : ℕ :=
…
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.repetitionCount_pos line 30
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.repeated_game_bound line 35
  7. def OAI.MaxCutGames.Foundations.Hastad.SourceGap.source line 52

    Source documentation

    The actual nonempty, numbered occurrence list at the fixed parameters.

    def source (η ξ : ℚ) (hη : 0 < η) (hη1 : η ≤ 1) (hξ : 0 < ξ)
    (D : ℕ) (hD : 0 < D) (F : Formula) : SourceEncoding.Input :=
…
  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.source_complete line 56
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.source_sound line 69
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.source_size line 80
  11. def OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator line 99

    Source documentation

    A positive rational has numerator at least one, so its reciprocal denominator is no larger than the rational itself. Adding two also ensures the noise parameter is at most one half for every input.

    def noiseDenominator (ξ : ℚ) : ℕ := ξ.den + 2
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_ge_two line 101
  13. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_pos line 105
  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_pos line 108
  15. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le_half line 113
  16. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le line 120

    Source documentation

    The actual computed reciprocal noise is below every positive target.

    theorem noiseDenominator_inv_le {ξ : ℚ} (hξ : 0 < ξ) :
    (noiseDenominator ξ : ℚ)⁻¹ ≤ ξ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator

  17. def OAI.MaxCutGames.Foundations.Hastad.SourceGap.forError line 143
  18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.forError_complete line 147
  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.forError_sound line 156
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGap.forError_size line 165
  21. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorContract.NonemptyFormula line 177
  22. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorContract.inputEncoding line 179
  23. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorContract.sourceMap line 181
  24. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorContract.errorMap line 185
  25. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorContract.inputEncoding_mk line 189
  26. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.Tape line 200
  27. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.Ambient line 201
  28. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.State line 202
  29. inductive OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.Label line 206
  30. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.bodyEntry line 215
  31. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.next line 217
  32. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.sourceStateEquiv line 220
  33. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.program line 226
  34. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.main line 243
  35. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.machine line 245
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.finite_work_alphabets line 256
  37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.atCheck line 261
  38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.atReset line 265
  39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.source_initial line 281
  40. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.initial_configuration line 285
  41. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.startupInTime line 298
  42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.clauseRank_le_power line 327
  43. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.variableRank_le_power line 333
  44. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.leftValue_le_numberBound line 340
  45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.rightValue_le_numberBound line 346
  46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.leftBlock_le_numberBound line 351
  47. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.rankPolynomial line 359
  48. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.numberPolynomial line 360
  49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.rankPolynomial_eval line 363
  50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.numberPolynomial_eval line 365
  51. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.slotPolynomial line 369
  52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.slotPolynomial_eval line 376
  53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.slotBudget_le line 385
  54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.prefixBudget_le line 404
  55. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.preparePolynomial line 418
  56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.preparePolynomial_eval line 423
  57. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.setupPolynomial line 430
  58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.setupPolynomial_eval line 436
  59. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.finishPolynomial line 444
  60. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.finishPolynomial_eval line 448
  61. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial line 454
  62. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.setupBudget_le line 457
  63. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.finishBudget_le line 474
  64. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyBudget_le line 482

    Source documentation

    One fixed polynomial bounds the actual tuple-body budget for every tuple.

    theorem bodyBudget_le (F : Target.Formula) (c : ClauseContext F u) :
    bodyBudget (D := D) F c ≤ (bodyPolynomial u D).eval (formulaBits F).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  65. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.fixed_parameters_body_bound line 491
  66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyInPolynomialTime line 497

    Source documentation

    The actual body execution with the same fixed polynomial for every tuple.

    theorem bodyInPolynomialTime {Extra : Type} [DecidableEq Extra]
    (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : SourceRuntimeModel.Arena u Extra → List Bool) (h : Ready F c base) :
    Nonempty (StateTransition.EvalsToInTime (Turing.TM2.step (program initialQuery exit))
      ⟨some main, SourceRuntimeModel.canonicalState initialQuery, base⟩
      (some ⟨exit, SourceRuntimeModel.canonicalState initialQuery,
        SourceTestAppend.resultTapes SourceRuntimeModel.queryLayout base
          (SourceQueryOrder.tupleBits F u D c)⟩)
      ((bodyPolynomial u D).eval (formulaBits F).length)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.Arena, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.canonicalState, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.queryLayout, OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  67. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.accumulatorRole line 526
  68. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.leafTapes line 529
  69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_accumulator line 534
  70. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_work_blank line 538
  71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_ready line 549

    Source documentation

    Every concrete tuple and arbitrary accumulated prefix satisfies the actual body's representation invariant after startup.

    theorem leaf_ready (F : Target.Formula) (c : ClauseContext F u) (output : List Bool) :
    SourceTupleBody.Ready F c (leafTapes (D := D) F c output) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.leafTapes

  72. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.body_result_leaf line 578

    Source documentation

    The actual body's accumulator update has exactly the endpoint expected by the nested odometer schedule.

    theorem body_result_leaf (F : Target.Formula) (c : ClauseContext F u)
    (output bits : List Bool) :
    SourceTestAppend.resultTapes queryLayout (leafTapes (D := D) F c output) bits =
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.leafTapes

  73. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.source_initial line 588
  74. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.actual_bodies line 594

    Source documentation

    The body-run premise of the odometer is discharged by the checked body machine and its fixed polynomial bound, in this same final generator program.

    theorem actual_bodies (F : Target.Formula) (hD : 0 < D) :
    BodyTrace (SourceGeneratorProgram.program u D hD) (bodyEntry u D) (next u D 0)
      (initialAmbient u D hD) (accumulatorRole u D) (SourceStartup.readyTapes F)
      (SourceQueryOrder.tupleBits F u D)
      ((SourceTupleBound.bodyPolynomial u D).eval (formulaBits F).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.program, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.accumulatorRole, OAI.MaxCutGames.Foundations.Hastad.SourceStartup.readyTapes, OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  75. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.resetDigits_ready line 618

    Source documentation

    Startup already supplies exactly the reset odometer digits.

    theorem resetDigits_ready (F : Target.Formula) :
    setDigits F.clauses.length (fun _ : Fin u => 0)
      (SourceStartup.readyTapes (u := u) (D := D) F) = SourceStartup.readyTapes F := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceStartup.readyTapes

  76. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.allBits_eq_records line 624
  77. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.accumulated_eq_input line 636

    Source documentation

    Include the exact reversed header already emitted by startup.

    theorem accumulated_eq_input (F : Target.Formula) (hD : 0 < D) (hne : F.clauses ≠ []) :
    (allBits (SourceQueryOrder.tupleBits F u D)).reverse ++
        SourceStartup.readyTapes F (accumulatorTape u D) =
      (MaxCutGames.Reduction.SourceEncoding.inputBits (sourceInput F u D hD)).reverse := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.MaxCutGames.Foundations.Hastad.SourceStartup.readyTapes, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits

  78. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput line 648
  79. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_accumulator line 652
  80. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_frame line 657
  81. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.resetLabel line 662
  82. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalInTime line 667

    Source documentation

    Actual traversal of every clause tuple, with each digit physically reset. All nonaccumulator tapes have exactly their startup-ready contents.

    theorem traversalInTime (F : Target.Formula) (hm : 0 < F.clauses.length) (hD : 0 < D) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step (SourceGeneratorProgram.program u D hD))
      ⟨some (bodyEntry u D), (initialAmbient u D hD, none), SourceStartup.readyTapes F⟩
      (some ⟨some .finishEnter, (initialAmbient u D hD, none), traversalOutput F hD⟩)
      (((SourceTupleBound.bodyPolynomial u D).eval (formulaBits F).length + 2 * u) *
        F.clauses.length ^ u)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorProgram.program, OAI.MaxCutGames.Foundations.Hastad.SourceStartup.readyTapes, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  83. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.timePolynomial line 711
  84. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorTraversal.traversalInPolynomialTime line 714