OAI/Computability/UniqueGames/PCP/SourceGapLemmas.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

The actual finite graph iteration used by the mathematical PCP construction. One fixed, explicitly supplied complete address list is shared by every round. Each round constructs a new constraint graph. The scalar gap and size are the actual minimum rejection fraction and actual finite cardinalities of that graph.

The final Boolean formula uses supplied vertex and dart numberings. These theorems establish the finite objects and their size/gap properties, not a machine running-time theorem or an independently encoded NP-hardness theorem.

  1. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.ClauseGap line 32

    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.UniqueGamesTheorem.Foundations.Hastad.SourceGap.third_pos line 37
  3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.third_le_one line 39
  4. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.repetitionCount line 43

    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.UniqueGamesTheorem.Foundations.Hastad.SourceGap.repetitionCount_pos line 47
  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.repeated_game_bound line 52
  7. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.source line 69

    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.UniqueGamesTheorem.Foundations.Hastad.SourceGap.source_complete line 73
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.source_sound line 86
  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.source_size line 97
  11. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.forError line 108
  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.forError_complete line 112
  13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.forError_sound line 121
  14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.forError_size line 130
  15. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorContract.NonemptyFormula line 144
  16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorContract.inputEncoding line 146
  17. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorContract.sourceMap line 148
  18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorContract.errorMap line 152
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorContract.inputEncoding_mk line 156
  20. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.Tape line 170
  21. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.Ambient line 171
  22. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.State line 172
  23. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.Label line 176
  24. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.bodyEntry line 185
  25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.next line 187
  26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.sourceStateEquiv line 190
  27. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.program line 196
  28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.main line 213
  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.machine line 215
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.finite_work_alphabets line 226
  31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.atCheck line 231
  32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.atReset line 235
  33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.source_initial line 252
  34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.initial_configuration line 256
  35. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.startupInTime line 269
  36. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.accumulatorRole line 302
  37. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.leafTapes line 305
  38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.leaf_accumulator line 310
  39. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.leaf_work_blank line 314
  40. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.leaf_ready line 325

    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.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.leafTapes

  41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.body_result_leaf line 354

    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.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.leafTapes

  42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.source_initial line 364
  43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.actual_bodies line 370

    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.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.accumulatorRole, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.readyTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.resetDigits_ready line 394

    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.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.readyTapes

  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.allBits_eq_records line 400
  46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.accumulated_eq_input line 412

    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) =
      (UniqueGamesTheorem.Reduction.SourceEncoding.inputBits (sourceInput F u D hD)).reverse := by
…

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

  47. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput line 424
  48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_accumulator line 428
  49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_frame line 433
  50. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.resetLabel line 438
  51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.traversalInTime line 443

    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.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorProgram.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.readyTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  52. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.timePolynomial line 487
  53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorTraversal.traversalInPolynomialTime line 490
  54. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.prefixPolynomial line 521
  55. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.timePolynomial line 524
  56. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.beforeFinish line 528
  57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.enterFinishInTime line 532
  58. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.prefixInTime line 548
  59. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.output_empty line 564
  60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.halted_configuration line 571
  61. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.outputInTime line 590
  62. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.computableInPolyTime line 616
  63. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.finite_work_alphabets line 635
  64. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.forErrorComputableInPolyTime line 641
  65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGenerator.forError_finite_work_alphabets line 649
  66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNonempty.real_clause_gap_of_count line 667

    Source documentation

    Convert an actual natural-number clause-count inequality to the real inequality used by the clause-variable game.

    theorem real_clause_gap_of_count (F : Formula) (a b : ℕ) (hb : 0 < b)
    (hgap : ∀ assignment : Fin F.variables → Bool,
      a * F.clauses.length ≤ b * NameCompaction.failedCount F assignment)
    (assignment : Fin F.variables → Bool) :
    (a : ℝ) / (b : ℝ) * F.clauses.length ≤
      (failureCount F assignment (allIndices F) : ℝ) := by
…
  67. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNonempty.clauseGap_of_count line 681
  68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNonempty.cnf_nonempty_of_nonempty_darts line 694

    Source documentation

    The actual final graph bundle carries a nonempty dart type, so its explicitly numbered Boolean CNF is nonempty even before using any gap.

    theorem cnf_nonempty_of_nonempty_darts [Fintype E] [Nonempty E]
    (G : ConstraintGraph V E FinalBooleanVerifier.Label)
    (vertices : V ≃ Fin n) (edges : E ≃ Fin m) :
    (FinalBooleanVerifier.cnf G vertices edges).clauses ≠ [] := by
…
  69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNonempty.cnf_clauseGap line 705

    Source documentation

    The checked final Boolean-verifier count bound produces exactly the nonempty clause-gap premise of SourceGap, with denominator 40960 * b.

    theorem cnf_clauseGap [Fintype E] [Nonempty E]
    (G : ConstraintGraph V E FinalBooleanVerifier.Label)
    (vertices : V ≃ Fin n) (edges : E ≃ Fin m) (a b : ℕ) (hb : 0 < b)
    (hgap : ∀ labeling : V → FinalBooleanVerifier.Label,
      a * Fintype.card E ≤ b * G.rejectionCount labeling) :
    SourceGap.ClauseGap (FinalBooleanVerifier.cnf G vertices edges)
      ((a : ℚ) / ((b : ℚ) * 40960)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.ClauseGap

  70. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNonempty.cnf_clauseGap_unit line 719

    Source documentation

    The unit-numerator gap supplied by the final powering stage has the fixed rational clause gap 1 / (40960 * walkLength).

    theorem cnf_clauseGap_unit [Fintype E] [Nonempty E]
    (G : ConstraintGraph V E FinalBooleanVerifier.Label)
    (vertices : V ≃ Fin n) (edges : E ≃ Fin m) (walkLength : ℕ)
    (hwalk : 0 < walkLength)
    (hgap : ∀ labeling : V → FinalBooleanVerifier.Label,
      Fintype.card E ≤ walkLength * G.rejectionCount labeling) :
    SourceGap.ClauseGap (FinalBooleanVerifier.cnf G vertices edges)
      (1 / (40960 * (walkLength : ℚ))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGap.ClauseGap

  71. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.Label line 753
  72. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.Graph line 754
  73. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.Addresses line 755
  74. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.step line 757
  75. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.run line 761
  76. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.initial line 764
  77. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.iterationCount line 766
  78. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output line 768
  79. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.polynomialDegree line 772

    Source documentation

    Fixed exponent; the enormous fixed graph constants remain unevaluated.

    def polynomialDegree : Nat := AmplificationIteration.rounds RoundSize.sizeFactor

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.rounds, OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.sizeFactor

  80. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalClauseGap line 774
  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalClauseGap_positive line 776
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.sizeFactor_le_power line 780
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 783
  84. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.initial_size_positive line 787
  85. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.initial_size_bound line 790
  86. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.step_completeness line 798
  87. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.step_gap line 802
  88. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.step_size line 806
  89. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.run_completeness line 810
  90. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.run_gap line 816
  91. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.run_size line 822
  92. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output_completeness line 828
  93. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output_gap line 836

    Source documentation

    The actual graph reaches the fixed positive gap after the concrete number of rounds determined by its initial total size.

    theorem output_gap (addresses : List Addresses) (complete : ∀ w, w ∈ addresses)
    (F : Target.Formula) (unsat : ¬ F.Satisfiable) :
    FinalConstants.cap ≤ (output addresses complete F).gap := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.Addresses, OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap, OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output

  94. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output_satisfiable_iff line 846
  95. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output_size_polynomial line 856
  96. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output_size_clause_bound line 863
  97. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.output_count_gap line 871
  98. def OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF line 897
  99. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 900
  100. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_clause_count line 905
  101. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_variable_count line 909
  102. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_nonempty line 913
  103. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_gap line 920
  104. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 932
  105. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_total_size line 938
  106. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 955