OAI/Computability/MaxCut/PCP/PoweringTableSemantics.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Exact semantics of the executable powering tables

The explicit label and dart bijections preserve every actual edge test and every rejected directed occurrence. The inverse label map covers all encoded assignments, so satisfiability and uniform rejection-count bounds transport without any consistency restriction on padded labels.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.RawLabeling line 20
  2. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 23
  3. def OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 26
  4. def OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 30
  5. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 34
  6. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 40
  7. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 49

    Source documentation

    Each enumerated directed occurrence evaluates its actual powering test.

    theorem edgeSatisfied_encoded {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : RawLabeling vertices d n)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n) :
    (GenericGraphTables.semantics (table input n)).edgeSatisfied
      (encodeLabeling d n labels) (encodeDart vertices d n e) =
        (mathematicalGraph input n).edgeSatisfied labels e := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling

  8. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 62

    Source documentation

    The equality also holds for every encoded assignment and every stored row.

    theorem edgeSatisfied_decoded {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : EncodedLabeling vertices d n) (i : Fin (dartCount vertices d n)) :
    (GenericGraphTables.semantics (table input n)).edgeSatisfied labels i =
      (mathematicalGraph input n).edgeSatisfied (decodeLabeling d n labels)
        (decodeDart vertices d n i) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling

  9. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 74

    Source documentation

    The stored Boolean test is exactly the path test at the recorded endpoints.

    theorem edgeSatisfied_eq_path {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : EncodedLabeling vertices d n) (direction : Bool)
    (w : Walk (Fin vertices) (Fin d) (n + 1)) :
    (GenericGraphTables.semantics (table input n)).edgeSatisfied labels
      (encodeDart vertices d n (direction, w)) =
    PoweringTest.pathAccepts (PortTables.portGraph input) (PortTables.accepts input) n
      (finitePortSelector (PortTables.portGraph input) (n + 1)) w
      (decodeLabeling d n labels w.1)
      (decodeLabeling d n labels (endpoint (PortTables.portGraph input) w)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling

  10. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 90

    Source documentation

    Exact rejected-dart counting, retaining both orientations and repeated walks.

    theorem rejectionCount_encoded {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : RawLabeling vertices d n) :
    (GenericGraphTables.semantics (table input n)).rejectionCount
      (encodeLabeling d n labels) = (mathematicalGraph input n).rejectionCount labels := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling

  11. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 100
  12. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 109

    Source documentation

    The denominator equality comes from the same explicit dart bijection.

    theorem card_darts_eq_table {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) :
    Fintype.card (PoweringTest.Dart (Fin vertices) (Fin d) n) = (table input n).darts := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart

  13. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 117

    Source documentation

    The table has a satisfying encoded assignment exactly when the powered graph does.

    theorem satisfiable_iff {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat) :
    (GenericGraphTables.semantics (table input n)).Satisfiable ↔
      (mathematicalGraph input n).Satisfiable := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics

  14. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 135

    Source documentation

    Perfect completeness from the actual stored base predicates.

    theorem preserves_satisfiability {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (h : (PortTables.baseGraph input).Satisfiable) :
    (GenericGraphTables.semantics (table input n)).Satisfiable := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics

  15. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 144

    Source documentation

    The path rejection average equals the encoded table's actual rejection fraction.

    theorem path_rejection_mean_eq_table_fraction {vertices d : Nat}
    (input : PortTables.Table vertices d) (n : Nat) (labels : EncodedLabeling vertices d n) :
    SpectralReturn.mean (fun w : Walk (Fin vertices) (Fin d) (n + 1) =>
      PoweringMoment.bit
        (PoweringTest.pathAccepts (PortTables.portGraph input) (PortTables.accepts input) n
          (finitePortSelector (PortTables.portGraph input) (n + 1)) w
          (decodeLabeling d n labels w.1)
          (decodeLabeling d n labels (endpoint (PortTables.portGraph input) w)) = false)) =
      ((GenericGraphTables.semantics (table input n)).rejectionCount labels : ℝ) /
        ((table input n).darts : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit, OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics

  16. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 160

    Source documentation

    Uniform actual rejection-count gaps are invariant under the executable encoding.

    theorem uniform_count_gap_iff {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (epsilon : ℝ) :
    (∀ labels : EncodedLabeling vertices d n,
      epsilon * ((table input n).darts : ℝ) ≤
        ((GenericGraphTables.semantics (table input n)).rejectionCount labels : ℝ)) ↔
    (∀ labels : RawLabeling vertices d n,
      epsilon * (Fintype.card (PoweringTest.Dart (Fin vertices) (Fin d) n) : ℝ) ≤
        ((mathematicalGraph input n).rejectionCount labels : ℝ)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart

  17. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 180

    Source documentation

    Apply an established powering count bound to every encoded table labeling.

    theorem uniform_count_gap {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (epsilon : ℝ)
    (hgap : ∀ labels : RawLabeling vertices d n,
      epsilon * (Fintype.card (PoweringTest.Dart (Fin vertices) (Fin d) n) : ℝ) ≤
        ((mathematicalGraph input n).rejectionCount labels : ℝ)) :
    ∀ labels : EncodedLabeling vertices d n,
      epsilon * ((table input n).darts : ℝ) ≤
        ((GenericGraphTables.semantics (table input n)).rejectionCount labels : ℝ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics

  18. structure OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Verifier line 210
  19. abbrev OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Label line 214
  20. abbrev OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Vertex line 215
  21. abbrev OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Dart line 216
  22. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.response line 220
  23. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.zeroSlot line 223
  24. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.decodeRight line 225
  25. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.encodeRight line 227
  26. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.decode_encodeRight line 229
  27. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.canonicalSlot line 232
  28. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.canonicalSlot_query line 235
  29. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.RepeatedConsistent line 239
  30. instance OAI.MaxCutGames.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 242
  31. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.LeftValid line 248
  32. instance OAI.MaxCutGames.Foundations.PCP.QueryIncidence.leftValidDecidable line 251
  33. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.incidenceAccept line 257
  34. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.reverse line 262
  35. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.reverse_involutive line 264
  36. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.reverseEquiv line 268
  37. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.tail line 274
  38. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.predicate line 278
  39. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.graph line 283
  40. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 293
  41. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.honestLabeling line 301
  42. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.honest_leftValid line 305
  43. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.honest_incidence line 312
  44. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.perfect_completeness line 323
  45. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 331
  46. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.decodedAssignment line 339
  47. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.incidenceAccept_true line 342
  48. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 351
  49. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 366
  50. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.rejectedEvents line 384
  51. def OAI.MaxCutGames.Foundations.PCP.QueryIncidence.verifierRejectionCount line 387
  52. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.rejection_count_bound line 392

    Source documentation

    Every rejected event contributes two distinct rejected darts, one in each orientation. A classical witness is used only in this counting proof.

    theorem rejection_count_bound [Fintype E] [DecidableEq X]
    (T : Verifier E X q) (positive : 0 < q) (labeling : Vertex E X → Label q) :
    2 * verifierRejectionCount T (decodedAssignment positive labeling) ≤
      (graph T positive).rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Verifier, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Vertex, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Label, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.verifierRejectionCount, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.decodedAssignment, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.graph

  53. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.card_label line 421
  54. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.card_vertex line 424
  55. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.card_dart line 428
  56. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.gap_transfer line 432
  57. theorem OAI.MaxCutGames.Foundations.PCP.QueryIncidence.six_query_alphabet line 447
  58. def OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement line 461
  59. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement_self line 463
  60. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement_nonnegative line 466
  61. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement_le_one line 469
  62. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement_comm line 472
  63. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement_triangle line 475
  64. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.disagreement_eq_sign line 479
  65. def OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance line 483
  66. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance_self line 486
  67. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance_nonnegative line 490
  68. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance_comm line 494
  69. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance_triangle line 498
  70. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance_eq_sign line 504
  71. def OAI.MaxCutGames.Foundations.PCP.CodeComposition.codeword line 512

    Source documentation

    The encoding is a literal coordinate read from a finite Boolean truth table.

    def codeword {A : Type*} (a : A) : Cube A → Bool := fun x => x a
  72. def OAI.MaxCutGames.Foundations.PCP.CodeComposition.singletonMask_inline_CodeComposition line 514
  73. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.walsh_singletonMask_inline_CodeComposition line 517
  74. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.singletonMask_ne_inline_CodeComposition line 527
  75. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.codeword_distance line 533
  76. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.exists_nearest line 544
  77. def OAI.MaxCutGames.Foundations.PCP.CodeComposition.nearest line 553

    Source documentation

    Classical choice is used only for the soundness analysis, not the output algorithm.

    def nearest {A : Type*} [Fintype A] [DecidableEq A] [Nonempty A] (f : Cube A → Bool) : A :=
…
  78. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.nearest_minimal line 556
  79. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.distance_from_other_codeword line 561
  80. def OAI.MaxCutGames.Foundations.PCP.CodeComposition.pairWord line 570

    Source documentation

    Two equal-sized blocks, indexed by a side bit and a common coordinate.

    def pairWord {X : Type*} (left right : X → Bool) : Bool × X → Bool :=
…
  81. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.pairWord_distance line 573
  82. theorem OAI.MaxCutGames.Foundations.PCP.CodeComposition.rejected_pair_far line 583

    Source documentation

    Every satisfying encoded pair is far from a pair whose nearest decoding rejects.

    theorem rejected_pair_far {A : Type*} [Fintype A] [DecidableEq A] [Nonempty A]
    (accepts : A → A → Bool) (left right : Cube A → Bool)
    (hbad : accepts (nearest left) (nearest right) = false)
    (a b : A) (hgood : accepts a b = true) :
    1 / 8 ≤ relativeDistance (pairWord left right)
      (pairWord (codeword a) (codeword b)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.CodeComposition.nearest, OAI.MaxCutGames.Foundations.PCP.CodeComposition.relativeDistance, OAI.MaxCutGames.Foundations.PCP.CodeComposition.pairWord, OAI.MaxCutGames.Foundations.PCP.CodeComposition.codeword