OAI/Computability/MaxCut/PCP/RoundGap.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Size of the actual fixed amplification round

All constants below depend only on the fixed port alphabet and walk length. The round itself is the checked preprocessing, powering, and alphabet graph construction in AmplificationRound; no second graph constructor is introduced. Closed constants are kept symbolic rather than evaluated.

  1. def OAI.MaxCutGames.Foundations.PCP.RoundGap.poweredLower line 16
  2. theorem OAI.MaxCutGames.Foundations.PCP.RoundGap.poweredLower_nonnegative line 20
  3. theorem OAI.MaxCutGames.Foundations.PCP.RoundGap.powered_count_gap line 28
  4. theorem OAI.MaxCutGames.Foundations.PCP.RoundGap.amplifies line 56
  5. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.card_padded_alphabet line 88
  6. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.card_powered_dart line 95
  7. opaque OAI.MaxCutGames.Foundations.PCP.RoundSize.lockedNat line 106

    Source comment

    An opaque value with a checked equality prevents the kernel's closed-numeral evaluator from expanding the astronomical powers. Its body is proved once for an arbitrary natural number; no axiom or trusted evaluator is introduced. Only size bounds use these constants, not the graph's algorithm definitions.
    private opaque lockedNat (n : Nat) : {m : Nat // m = n} := ⟨n, rfl⟩
  8. def OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredAlphabetSize line 108
  9. def OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredDartFactor line 112
  10. def OAI.MaxCutGames.Foundations.PCP.RoundSize.sizeFactor line 115
  11. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredAlphabetSize_eq line 119
  12. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredDartFactor_eq line 123
  13. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.sizeFactor_eq line 127
  14. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.coefficient_positive_inline_RoundSize line 131
  15. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredAlphabet_card line 136
  16. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.sizeFactor_positive line 145
  17. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.factor_total_inline_RoundSize line 151
  18. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.nat_card_output_vertex_inline_RoundSize line 154
  19. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.nat_card_output_dart_inline_RoundSize line 162
  20. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.nat_card_output_total_le_inline_RoundSize line 169
  21. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredDart_card line 181
  22. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.output_vertex_card line 192

    Source documentation

    The exact cardinality of the round's output vertex type.

    theorem output_vertex_card (G : ConstraintGraph V E AmplificationRound.Label) :
    Fintype.card (AmplificationRound.Vertex G) =
      Fintype.card (Preprocessing.Vertex G) * 2 ^ poweredAlphabetSize +
        (Fintype.card (Preprocessing.Vertex G) * poweredDartFactor) *
          AlphabetGraphBounds.vertexFactor poweredAlphabetSize := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Label, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Vertex, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredAlphabetSize, OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredDartFactor, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor

  23. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.output_dart_card line 207

    Source documentation

    The exact cardinality of the round's output dart type.

    theorem output_dart_card (G : ConstraintGraph V E AmplificationRound.Label) :
    Fintype.card (AmplificationRound.Dart G) =
      (Fintype.card (Preprocessing.Vertex G) * poweredDartFactor) *
        AlphabetGraphBounds.dartFactor poweredAlphabetSize := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Label, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Dart, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredDartFactor, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.dartFactor, OAI.MaxCutGames.Foundations.PCP.RoundSize.poweredAlphabetSize

  24. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.output_total_le_darts line 219

    Source documentation

    The actual round has linear total size, even in the old dart count alone.

    theorem output_total_le_darts (G : ConstraintGraph V E AmplificationRound.Label) :
    Fintype.card (AmplificationRound.Vertex G) + Fintype.card (AmplificationRound.Dart G) ≤
      sizeFactor * Fintype.card E := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Label, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Vertex, OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Dart, OAI.MaxCutGames.Foundations.PCP.RoundSize.sizeFactor

  25. theorem OAI.MaxCutGames.Foundations.PCP.RoundSize.output_total_le line 245
  26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNonempty.real_clause_gap_of_count line 260

    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
…
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNonempty.clauseGap_of_count line 274
  28. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNonempty.cnf_nonempty_of_nonempty_darts line 287

    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
…
  29. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap line 298

    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.MaxCutGames.Foundations.Hastad.SourceGap.ClauseGap

  30. theorem OAI.MaxCutGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap_unit line 312

    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.MaxCutGames.Foundations.Hastad.SourceGap.ClauseGap

  31. abbrev OAI.MaxCutGames.Foundations.PCP.PCPIteration.Label line 343
  32. abbrev OAI.MaxCutGames.Foundations.PCP.PCPIteration.Graph line 344
  33. abbrev OAI.MaxCutGames.Foundations.PCP.PCPIteration.Addresses line 345
  34. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.step line 347
  35. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.run line 351
  36. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.initial line 354
  37. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.iterationCount line 356
  38. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.output line 358
  39. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.polynomialDegree line 362

    Source documentation

    Fixed exponent; the enormous fixed graph constants remain unevaluated.

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

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

  40. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalClauseGap line 364
  41. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalClauseGap_positive line 366
  42. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.sizeFactor_le_power line 370
  43. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 373
  44. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.initial_size_positive line 377
  45. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.initial_size_bound line 380
  46. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.step_completeness line 388
  47. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.step_gap line 392
  48. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.step_size line 396
  49. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.run_completeness line 400
  50. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.run_gap line 406
  51. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.run_size line 412
  52. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.output_completeness line 418
  53. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.output_gap line 426

    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.MaxCutGames.Foundations.PCP.PCPIteration.Addresses, OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap, OAI.MaxCutGames.Foundations.PCP.PCPIteration.output

  54. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.output_satisfiable_iff line 436
  55. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.output_size_polynomial line 446
  56. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.output_size_clause_bound line 453
  57. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.output_count_gap line 461
  58. def OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF line 485
  59. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 488
  60. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_clause_count line 493
  61. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_variable_count line 497
  62. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_nonempty line 501
  63. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_gap line 508
  64. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 520
  65. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_total_size line 526
  66. theorem OAI.MaxCutGames.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 543
  67. def OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.output line 563
  68. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.satisfiable_iff line 566
  69. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.variable_count line 573
  70. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.clause_count line 577
  71. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.nonempty line 581
  72. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 586

    Source documentation

    Boolean labels and numeric labels have exactly the same rejected darts.

    theorem tableGraph_rejectionCount (table : GraphTables.Table)
    (labeling : Fin table.vertices → FinalBooleanVerifier.Label) :
    (FinalCNFPattern.tableGraph table).rejectionCount labeling =
      (GraphTables.semantics table).rejectionCount
        (fun v => FinalCNFPattern.labelEquiv (labeling v)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics

  73. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 597

    Source documentation

    A uniform numeric-label count bound transfers to the machine's Boolean-label graph.

    theorem tableGraph_count_lower (table : GraphTables.Table) (walkLength : Nat)
    (hgap : ∀ labeling : Fin table.vertices → GraphTables.Label,
      table.darts ≤ walkLength * (GraphTables.semantics table).rejectionCount labeling)
    (labeling : Fin table.vertices → FinalBooleanVerifier.Label) :
    Fintype.card (Fin table.darts) ≤
      walkLength * (FinalCNFPattern.tableGraph table).rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.Label

  74. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.clauseGap line 606
  75. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.total_size_le line 616
  76. def OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.sizePolynomial line 624

    Source documentation

    A fixed quadratic in the full serialized input length.

    noncomputable def sizePolynomial : Polynomial Nat :=
…
  77. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 629
  78. theorem OAI.MaxCutGames.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 633