OAI/Computability/MaxCut/PCP/RawInitialTables.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

Explicit structural numberings of the raw 3SAT incidence graph. Unused declared variable names are retained; their unary input header pays for them. The graph has one dummy vertex and one tautological loop, even for an empty formula. No input-dependent choice of a finite enumeration is made.

  1. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.unitOrder line 16
  2. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.slotOrder line 22
  3. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.binaryOrder line 31
  4. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.labelOrder line 40
  5. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.vertexOrder line 42
  6. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.eventOrder line 46
  7. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.dartOrder line 49
  8. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.raw64 line 53
  9. def OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table line 57
  10. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table_vertices line 60
  11. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table_darts line 63
  12. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table_vertices_positive line 65
  13. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table_darts_positive line 68
  14. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.raw64_satisfiable_iff line 71
  15. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table_semantics line 76
  16. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.table_satisfiable_iff line 84
  17. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.initial_rejection line 90
  18. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialTables.initial_size line 96
  19. structure OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle line 116

    Source documentation

    Graphs of different finite sizes inhabit one fixed type for iteration.

    structure Bundle (A : Type) where
…
  20. instance OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 130
  21. instance OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 131
  22. instance OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 132
  23. instance OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 133
  24. instance OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 134
  25. instance OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 137

    Source documentation

    A dart supplies a vertex through the actual tail map.

    instance instNonemptyVertex (G : Bundle A) : Nonempty G.Vertex := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle

  26. def OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 141
  27. def OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.size line 153
  28. def OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 155
  29. def OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 157
  30. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.size_positive line 160
  31. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 163
  32. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 166
  33. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 170
  34. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 174
  35. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 178
  36. def OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 185
  37. def OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.gap line 187
  38. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 189
  39. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 193
  40. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 195
  41. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 197
  42. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 200
  43. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 205
  44. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 209
  45. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 216

    Source documentation

    The actual total graph size supplies the initial inverse-size gap.

    theorem one_le_size_mul_gap (G : Bundle A) (unsat : ¬ G.Satisfiable) :
    1 ≤ (G.size : ℝ) * G.gap := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle

  46. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 223
  47. theorem OAI.MaxCutGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 227
  48. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.alphabet line 239
  49. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.compositionLoss line 240
  50. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.denominator line 241
  51. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf line 242
  52. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowSize line 243
  53. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.smoothingScale line 244
  54. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.endpointLength line 245
  55. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.walkLength line 246
  56. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.gain line 248
  57. def OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap line 249
  58. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.denominator_positive line 251
  59. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf_positive line 254
  60. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.walkLength_positive line 257
  61. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.gain_large line 260
  62. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap_positive line 267
  63. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap_le_one line 270
  64. theorem OAI.MaxCutGames.Foundations.PCP.FinalConstants.composed_gap line 276

    Source documentation

    The exact fixed constants make a whole round double the input gap until the fixed positive threshold cap is reached.

    theorem composed_gap (epsilon : ℝ) (he : 0 ≤ epsilon) :
    min (2 * epsilon) cap ≤
      gain * min (epsilon / (Preprocessing.sizeFactor : ℝ))
        (1 / (walkLength : ℝ)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap, OAI.MaxCutGames.Foundations.PCP.FinalConstants.gain, OAI.MaxCutGames.Foundations.PCP.Preprocessing.sizeFactor, OAI.MaxCutGames.Foundations.PCP.FinalConstants.walkLength

  65. abbrev OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable line 304
  66. opaque OAI.MaxCutGames.Foundations.PCP.RoundTables.fixedWalkParameter line 308

    Source documentation

    Initialized fixed data keep enormous constant powers symbolic in the kernel. The stored equality proves the exact requested parameter; no value is assumed.

    opaque fixedWalkParameter : {n : Nat // n = 2 * FinalConstants.endpointLength} :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.FinalConstants.endpointLength

  67. def OAI.MaxCutGames.Foundations.PCP.RoundTables.walkParameter line 311
  68. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.walkParameter_eq line 313
  69. def OAI.MaxCutGames.Foundations.PCP.RoundTables.alphabet line 316
  70. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.alphabet_positive line 318
  71. def OAI.MaxCutGames.Foundations.PCP.RoundTables.powered line 322
  72. def OAI.MaxCutGames.Foundations.PCP.RoundTables.build line 325
  73. def OAI.MaxCutGames.Foundations.PCP.RoundTables.sizeFactor line 328
  74. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.degree_positive line 331
  75. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.dartFactor_positive line 335
  76. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.sizeFactor_positive line 339
  77. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.powered_vertices line 346
  78. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.powered_darts line 349
  79. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.build_darts_positive line 353
  80. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.build_size_le line 361
  81. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.build_completeness line 388
  82. abbrev OAI.MaxCutGames.Foundations.PCP.RoundTables.Input line 397
  83. instance OAI.MaxCutGames.Foundations.PCP.RoundTables.(instance at line 399) line 399
  84. def OAI.MaxCutGames.Foundations.PCP.RoundTables.step line 401
  85. def OAI.MaxCutGames.Foundations.PCP.RoundTables.initial line 404
  86. def OAI.MaxCutGames.Foundations.PCP.RoundTables.size line 407
  87. def OAI.MaxCutGames.Foundations.PCP.RoundTables.Satisfiable line 409
  88. def OAI.MaxCutGames.Foundations.PCP.RoundTables.gap line 411
  89. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.size_positive line 413
  90. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.gap_nonnegative line 416
  91. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.gap_eq_zero_iff line 419
  92. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.one_le_size_mul_gap line 422
  93. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.initial_satisfiable_iff line 434
  94. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.step_completeness line 437
  95. theorem OAI.MaxCutGames.Foundations.PCP.RoundTables.step_size line 440
  96. def OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run line 454
  97. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.min_double_min_inline_AmplificationIteration line 458
  98. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run_gap line 466
  99. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run_preserves line 481
  100. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run_size line 488
  101. def OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.rounds line 498

    Source documentation

    A concrete logarithmic iteration count, including the zero input.

    def rounds (n : Nat) : Nat := Nat.log2 n + 1
  102. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.rounds_large line 500
  103. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.rounds_power_le line 504
  104. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.blowup_rounds_le line 510

    Source documentation

    The constant blowup raised to the actual iteration count is polynomial in n.

    theorem blowup_rounds_le {C degree n : Nat} (hn : 0 < n) (hC : C ≤ 2 ^ degree) :
    C ^ rounds n ≤ (2 * n) ^ degree := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.rounds

  105. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run_size_polynomial line 518
  106. theorem OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run_reaches_cap line 526

    Source documentation

    An inverse-size initial gap reaches the fixed threshold after the concrete loop.

    theorem run_reaches_cap {X : Type*} (step : X → X) (gap : X → ℝ)
    (cap : ℝ) (hc : 0 ≤ cap) (hc1 : cap ≤ 1)
    (amplifies : ∀ x, min (2 * gap x) cap ≤ gap (step x))
    (n : Nat) (x : X) (hg : 0 ≤ gap x) (hstart : 1 ≤ (n : ℝ) * gap x) :
    cap ≤ gap (run step (rounds n) x) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.run, OAI.MaxCutGames.Foundations.PCP.AmplificationIteration.rounds

  107. abbrev OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.BoolTriple line 544
  108. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.tripleValue line 546
  109. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.chainView line 548
  110. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.fillBits line 553
  111. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.chainView_length line 561
  112. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.chainView_sound line 585
  113. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.fillBits_length line 612
  114. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.fillBits_correct line 628
  115. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 647
  116. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.chainView_failed line 653
  117. abbrev OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.Pattern line 665
  118. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.patterns line 668

    Source documentation

    The enumeration visits only the fixed-size truth table, never proof assignments.

    def patterns : (q : Nat) → List (Pattern q)
  | 0 => [Fin.elim0]
  | q + 1 => (patterns q).flatMap (fun p => [Fin.cases false p, Fin.cases true p])

    Mentions: OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.Pattern

  119. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 672
  120. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.patterns_length line 681
  121. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mem_patterns line 688
  122. abbrev OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.PatternIndex line 709
  123. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.patternAt line 710
  124. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.patternAt_surjective line 712
  125. structure OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.FiniteVerifier line 718

    Source documentation

    Finite test data, with no soundness or complexity assumption.

    structure FiniteVerifier (q : Nat) where
…
  126. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.eventValue line 724
  127. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.rejectedEventCount line 727
  128. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.auxiliaryCount line 730
  129. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.outputVariables line 733
  130. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.oldIndex line 735
  131. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.freshIndex line 738
  132. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.freshIndex_value line 742
  133. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.liftLiteral line 748
  134. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 751
  135. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.forbiddenClause line 755
  136. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.auxiliaryNames line 759
  137. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.splitLong line 763
  138. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.tautology line 769
  139. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.block line 774
  140. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.eventBlock line 779
  141. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.convert line 783
  142. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.clauseFailures line 787
  143. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.splitLong_values line 790
  144. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.splitLong_length line 813
  145. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.restrictAssignment line 822
  146. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mismatchBits line 826
  147. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mismatchBits_length line 830
  148. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 834
  149. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 840
  150. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mismatchBits_false line 847
  151. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mismatchBits_true line 857
  152. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mismatchFill_length line 876
  153. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.mismatchFill line 883
  154. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.extendAssignment line 892

    Source documentation

    A computable assignment extension: finite-sum splitting and quotient/remainder decoding recover the event, pattern, and auxiliary-bit indices.

    def extendAssignment {q : Nat} (V : FiniteVerifier q) (hq : 3 ≤ q)
    (A : Fin V.«variables» → Bool) : Fin (outputVariables V) → Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.FiniteVerifier, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.outputVariables

  155. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.extend_old line 899
  156. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.extend_fresh line 904
  157. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.restrict_extend line 912
  158. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 917
  159. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 922
  160. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.tautology_satisfied line 928
  161. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.block_length line 933
  162. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.block_honest line 946
  163. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 962
  164. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.eventBlock_length line 973
  165. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.convert_clause_count line 978
  166. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.convert_nonempty line 984
  167. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.convert_completeness line 993
  168. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.clauseFailures_append line 1001
  169. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 1005
  170. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.block_failed line 1021

    Source documentation

    The actual answer pattern forces a failed chain, even when queried names repeat and regardless of the labels on all allocated auxiliary «variables».

    theorem block_failed {q : Nat} (V : FiniteVerifier q) (hq : 3 ≤ q)
    (B : Fin (outputVariables V) → Bool) (e : Fin V.events) (p : PatternIndex q)
    (rejected : V.accepts e (patternAt q p) = false)
    (actual : ∀ i, restrictAssignment V B (V.query e i) = patternAt q p i) :
    1 ≤ clauseFailures (block V hq e p) B := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.FiniteVerifier, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.outputVariables, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.PatternIndex, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.patternAt, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.restrictAssignment, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.clauseFailures, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.block

  171. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.eventBlock_failed line 1038
  172. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.count_false_map_sum line 1050
  173. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 1056
  174. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 1064
  175. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.convert_count_bridge line 1072
  176. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.convert_gap line 1085
  177. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.twelve_query_factor line 1100
  178. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 1102
  179. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padLiteral line 1106
  180. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padClause line 1109
  181. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padTautology line 1112
  182. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padInput line 1116
  183. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padClause_eval line 1120
  184. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 1123
  185. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 1127
  186. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padInput_clause_count line 1148
  187. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.padInput_nonempty line 1151
  188. def OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.prepareInput line 1157
  189. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 1159
  190. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 1163
  191. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 1167
  192. theorem OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 1173