OAI/Computability/UniqueGames/PCP/AlphabetTableBoundsLemmas.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.gap_transfer_real line 18

    Source documentation

    The actual table output obeys the real gap bound, with no rational approximation and with empty input dart sets allowed.

    theorem gap_transfer_real (hq : 0 < q) (input : GenericGraphTables.Table q)
    (eps : ℝ) (eps_nonnegative : 0 ≤ eps)
    (source : ∀ labeling : Fin input.vertices → Fin q,
      eps * (input.darts : ℝ) ≤
        ((GenericGraphTables.semantics input).rejectionCount labeling : ℝ))
    (labeling : Fin (Table.build input).vertices → GraphTables.Label) :
    (eps / 12288) * ((Table.build input).darts : ℝ) ≤
      ((GraphTables.semantics (Table.build input)).rejectionCount labeling : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics

  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.build_vertices line 47

    Source documentation

    Exact output vertex count; this arithmetic identity also permits q = 0.

    theorem build_vertices (input : GenericGraphTables.Table q) :
    (Table.build input).vertices = input.vertices * 2 ^ q +
      input.darts * AlphabetGraphBounds.vertexFactor q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.vertexFactor

  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.build_darts line 58

    Source documentation

    Exact output dart count, including orientation and query multiplicity.

    theorem build_darts (input : GenericGraphTables.Table q) :
    (Table.build input).darts = input.darts * AlphabetGraphBounds.dartFactor q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.dartFactor

  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.build_total line 66
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.build_total_le line 74

    Source documentation

    A fixed alphabet gives one linear bound on the actual output table size.

    theorem build_total_le (input : GenericGraphTables.Table q) :
    (Table.build input).vertices + (Table.build input).darts ≤
      AlphabetGraphBounds.sizeFactor q * (input.vertices + input.darts) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.sizeFactor

  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.build_vertices_le line 91
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.build_darts_le line 96
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTableBounds.sizeFactor_positive line 101
  9. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.BoolTriple line 114
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.tripleValue line 116
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.chainView line 118
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.fillBits line 123
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.chainView_length line 131
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.chainView_sound line 155
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.fillBits_length line 182
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.fillBits_correct line 198
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.zero_false_count_iff_all line 217
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.chainView_failed line 223
  19. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.Pattern line 235
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.patterns line 238

    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.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.Pattern

  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.flatMap_pair_length line 242
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.patterns_length line 251
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mem_patterns line 258
  24. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.PatternIndex line 279
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.patternAt line 280
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.patternAt_surjective line 282
  27. structure OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.FiniteVerifier line 288

    Source documentation

    Finite test data, with no soundness or complexity assumption.

    structure FiniteVerifier (q : Nat) where
…
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.eventValue line 294
  29. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.rejectedEventCount line 297
  30. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.auxiliaryCount line 300
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.outputVariables line 303
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.oldIndex line 305
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.freshIndex line 308
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.freshIndex_value line 312
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.liftLiteral line 318
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.forbiddenLiteral line 321
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.forbiddenClause line 325
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.auxiliaryNames line 329
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.splitLong line 333
  40. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.tautology line 339
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.block line 344
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.eventBlock line 349
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.convert line 353
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.clauseFailures line 357
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.splitLong_values line 360
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.splitLong_length line 383
  47. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.restrictAssignment line 392
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mismatchBits line 396
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mismatchBits_length line 400
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.forbiddenLiteral_false line 404
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.forbiddenClause_values line 410
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mismatchBits_false line 417
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mismatchBits_true line 427
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mismatchFill_length line 446
  55. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.mismatchFill line 453
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.extendAssignment line 462

    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.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.FiniteVerifier, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.outputVariables

  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.extend_old line 469
  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.extend_fresh line 474
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.restrict_extend line 482
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.ofFn_getElem_of_length line 487
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.extended_auxiliary_values line 492
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.tautology_satisfied line 498
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.block_length line 503
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.block_honest line 516
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.length_flatMap_constant line 532
  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.eventBlock_length line 543
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.convert_clause_count line 548
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.convert_nonempty line 554
  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.convert_completeness line 563
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.clauseFailures_append line 571
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.clauseFailures_le_flatMap line 575
  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.block_failed line 591

    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.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.FiniteVerifier, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.outputVariables, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.PatternIndex, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.patternAt, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.restrictAssignment, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.clauseFailures, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.block

  73. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.eventBlock_failed line 608
  74. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.count_false_map_sum line 620
  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.clauseFailures_flatMap line 626
  76. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.nat_sum_map_le line 634
  77. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.convert_count_bridge line 642
  78. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.convert_gap line 655
  79. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.twelve_query_factor line 670
  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.twelve_query_clause_count line 672
  81. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padLiteral line 676
  82. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padClause line 679
  83. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padTautology line 682
  84. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padInput line 686
  85. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padClause_eval line 690
  86. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padTautology_satisfied line 693
  87. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padInput_satisfiable_iff line 697
  88. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padInput_clause_count line 718
  89. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.padInput_nonempty line 721
  90. def OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.prepareInput line 727
  91. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.prepareInput_satisfiable_iff line 729
  92. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.prepareInput_clause_count line 733
  93. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.prepareInput_nonempty line 737
  94. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.prepareInput_variable_bound line 743