OAI/Computability/MaxCut/PCP/Generator.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

Executable directed-dart tables for the fixed 64-label alphabet

The header gives vertex and dart counts. Every dart has one ordered row: tail index, reverse-dart index, and 4096 Boolean predicate entries. Entry b + 64 * a is the predicate at labels (a,b). All fields, including bits as 0/1 words, use the existing zero-delimited unary natural-word codec.

The decoder checks all index bounds, row counts, predicate lengths, reverse involution, predicate transpose, and absence of trailing fields. Directed rows preserve loops, self-reversing darts, and repeated constraint occurrences. The size theorems concern the full encoded table, not a machine runtime.

  1. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.prefixPolynomial line 17
  2. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.timePolynomial line 20
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.beforeFinish line 24
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.enterFinishInTime line 28
  5. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.prefixInTime line 44
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.output_empty line 60
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.halted_configuration line 67
  8. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.outputInTime line 86
  9. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.computableInPolyTime line 112
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.finite_work_alphabets line 127
  11. def OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.forErrorComputableInPolyTime line 133
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGenerator.forError_finite_work_alphabets line 141
  13. structure OAI.MaxCutGames.Foundations.PCP.ConstraintGraph line 153
  14. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.head line 164
  15. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.head_reverse line 166
  16. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.edgeSatisfied line 170
  17. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.edgeSatisfied_reverse line 173
  18. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.Satisfiable line 179
  19. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectedDarts line 182
  20. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCount line 185
  21. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.mem_rejectedDarts line 188
  22. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCount_le line 193
  23. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejected_exists_of_not_satisfiable line 197
  24. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCount_positive line 209
  25. abbrev OAI.MaxCutGames.Foundations.PCP.GraphTables.Label line 237
  26. abbrev OAI.MaxCutGames.Foundations.PCP.GraphTables.RelationTable line 238
  27. def OAI.MaxCutGames.Foundations.PCP.GraphTables.relationIndex line 241

    Source documentation

    The fixed row-major ordering of the complete predicate table.

    def relationIndex : Label × Label ≃ Fin 4096 := finProdFinEquiv

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Label

  28. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.relationIndex_val line 243
  29. def OAI.MaxCutGames.Foundations.PCP.GraphTables.relationAt line 246
  30. def OAI.MaxCutGames.Foundations.PCP.GraphTables.relationOf line 249
  31. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.relationAt_relationOf line 252
  32. structure OAI.MaxCutGames.Foundations.PCP.GraphTables.DartRow line 257

    Source documentation

    The row itself is finite data; index bounds are checked while parsing.

    structure DartRow (vertices darts : Nat) where
…
  33. abbrev OAI.MaxCutGames.Foundations.PCP.GraphTables.Rows line 262
  34. def OAI.MaxCutGames.Foundations.PCP.GraphTables.reverseAt line 264
  35. def OAI.MaxCutGames.Foundations.PCP.GraphTables.acceptsAt line 267
  36. def OAI.MaxCutGames.Foundations.PCP.GraphTables.Valid line 271

    Source documentation

    The two graph laws are decidable finite checks on the stored rows.

    def Valid {n m : Nat} (rows : Rows n m) : Prop :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Rows

  37. instance OAI.MaxCutGames.Foundations.PCP.GraphTables.(instance at line 275) line 275
  38. structure OAI.MaxCutGames.Foundations.PCP.GraphTables.Table line 279
  39. def OAI.MaxCutGames.Foundations.PCP.GraphTables.rowList line 286

    Source documentation

    The ordered list serialized by the codec. Equal rows remain separate.

    def rowList (table : Table) : List (DartRow table.vertices table.darts) := table.rows.toList

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.DartRow

  40. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.rowList_length line 288
  41. def OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics line 292

    Source documentation

    Decode validated finite data into the actual constraint-graph semantics.

    def semantics (table : Table) : ConstraintGraph (Fin table.vertices) (Fin table.darts) Label where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label

  42. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_reverse line 303
  43. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_tail line 306
  44. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_accepts line 309
  45. def OAI.MaxCutGames.Foundations.PCP.GraphTables.graphRows line 312
  46. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.reverseAt_graphRows line 315
  47. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.acceptsAt_graphRows line 320
  48. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.graphRows_valid line 325
  49. def OAI.MaxCutGames.Foundations.PCP.GraphTables.ofGraph line 333
  50. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 336
  51. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 341
  52. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 347
  53. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 352
  54. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.constraintGraph_ext_inline_GraphTables line 357
  55. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_ofGraph line 372

    Source documentation

    Complete semantic graph roundtrip, including its actual reversal map.

    @[simp] theorem semantics_ofGraph {n m : Nat}
    (G : ConstraintGraph (Fin n) (Fin m) Label) : semantics (ofGraph G) = G := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.GraphTables.ofGraph

  56. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 381
  57. def OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph line 389

    Source documentation

    Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made.

    def enumeratedGraph {V E A : Type*} {n m : Nat} (G : ConstraintGraph V E A)
    (vertexOrder : V ≃ Fin n) (dartOrder : E ≃ Fin m) (labelOrder : A ≃ Label) :
    ConstraintGraph (Fin n) (Fin m) Label where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label

  58. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 405
  59. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 414

    Source documentation

    Every directed occurrence contributes once before and after enumeration.

    theorem enumeratedGraph_rejectionCount {V E A : Type*} [Fintype E] {n m : Nat}
    (G : ConstraintGraph V E A) (vertexOrder : V ≃ Fin n) (dartOrder : E ≃ Fin m)
    (labelOrder : A ≃ Label) (labeling : V → A) :
    (enumeratedGraph G vertexOrder dartOrder labelOrder).rejectionCount
      (fun v => labelOrder (labeling (vertexOrder.symm v))) = G.rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph

  60. def OAI.MaxCutGames.Foundations.PCP.GraphTables.ofEnumeratedGraph line 426
  61. def OAI.MaxCutGames.Foundations.PCP.GraphTables.bitWord line 430
  62. def OAI.MaxCutGames.Foundations.PCP.GraphTables.parseBit line 432
  63. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.parseBit_bitWord line 437
  64. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.parseBits_bitWords line 440
  65. def OAI.MaxCutGames.Foundations.PCP.GraphTables.relationWords line 446
  66. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.relationWords_length line 448
  67. def OAI.MaxCutGames.Foundations.PCP.GraphTables.parseRelation line 451
  68. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.parseRelation_encoded line 457
  69. def OAI.MaxCutGames.Foundations.PCP.GraphTables.rowWords line 464
  70. def OAI.MaxCutGames.Foundations.PCP.GraphTables.parseRow line 467
  71. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.parseRow_encoded line 475
  72. def OAI.MaxCutGames.Foundations.PCP.GraphTables.parseRows line 483
  73. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.parseRows_encoded line 491
  74. def OAI.MaxCutGames.Foundations.PCP.GraphTables.tableWords line 497
  75. def OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits line 500
  76. def OAI.MaxCutGames.Foundations.PCP.GraphTables.decodeTableWords line 502
  77. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.decodeTableWords_encoded line 513
  78. def OAI.MaxCutGames.Foundations.PCP.GraphTables.decodeTableBits line 521
  79. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.decodeTableBits_encoded line 524
  80. def OAI.MaxCutGames.Foundations.PCP.GraphTables.encoding line 529

    Source documentation

    A concrete encoding suitable for the existing TM2 computation interface.

    def encoding : Computability.Encoding Table Bool where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table

  81. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits_injective line 534
  82. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.rowWords_length line 536
  83. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.rowsWords_length line 539
  84. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.tableWords_length line 545
  85. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.tableWords_length_le_bits line 552

    Source documentation

    At least one unary delimiter is stored for every field, including all 4096 entries of every predicate table.

    theorem tableWords_length_le_bits (table : Table) :
    2 + 4098 * table.darts ≤ (tableBits table).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits

  86. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.relationBits_length_le line 557
  87. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.rowBits_length_le line 565
  88. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.rowsBits_length_le line 574
  89. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits_length_le line 586

    Source documentation

    Full unary size bound: headers, both bounded indices in every row, and every Boolean predicate entry are counted. This is not a runtime assertion.

    theorem tableBits_length_le (table : Table) :
    (tableBits table).length ≤ table.vertices + table.darts + 2 +
      table.darts * (table.vertices + table.darts + 8192) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits

  90. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 595
  91. theorem OAI.MaxCutGames.Foundations.PCP.GraphTables.darts_le_tableBits_length line 601
  92. structure OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph line 615
  93. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Edge line 619
  94. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk line 620
  95. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.next line 624
  96. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rot_rot line 626
  97. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.walkEnd line 629
  98. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.walkEnd_nil line 633
  99. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.walkEnd_cons line 635
  100. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.walkEnd_append line 638
  101. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.splitHead line 645

    Source documentation

    Exposes the first dart and the independent remaining port word.

    def splitHead (V D : Type*) (n : Nat) :
    Walk V D (n + 1) ≃ ((V × D) × (Fin n → D)) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk

  102. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rotateHead line 657

    Source documentation

    Advance across the first edge while retaining its reverse port.

    def rotateHead (G : PortGraph V D) (n : Nat) : Walk V D (n + 1) ≃ Walk V D (n + 1) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk

  103. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rotateHead_vertex line 661
  104. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rotateHead_zero line 664
  105. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rotateHead_succ line 667
  106. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.permutePorts line 672

    Source documentation

    Relabeling time coordinates is a bijection on actual port words.

    def permutePorts {t : Nat} (σ : Fin t ≃ Fin t) : Walk V D t ≃ Walk V D t where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk

  107. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.wordEnd line 686
  108. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.endpoint line 690
  109. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.natCard_walk line 693
  110. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.headTailEquiv line 697
  111. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.advanceTail line 708
  112. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.edgeAt line 712

    Source documentation

    The dart at the indicated time, computed by the actual preceding steps.

    def edgeAt (G : PortGraph V D) :
    (n : Nat) → Walk V D (n + 1) → Fin (n + 1) → Edge V D
  | 0, w, _ => (w.1, w.2 0)
  | n + 1, w, k => Fin.cases (w.1, w.2 0)
      (fun j => edgeAt G n (advanceTail G w) j) k

/-- Isolate any actual path edge. Previously traversed ports are replaced by
their arrival ports, so the change of coordinates remains invertible. -/

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Edge, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.advanceTail

  113. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.pivotEquiv line 720

    Source documentation

    Isolate any actual path edge. Previously traversed ports are replaced by their arrival ports, so the change of coordinates remains invertible.

    def pivotEquiv (G : PortGraph V D) :
    (n : Nat) → Fin (n + 1) →
      (Walk V D (n + 1) ≃ (Edge V D × (Fin n → D)))
  | 0, _ => splitHead V D 0
  | n + 1, k => Fin.cases (splitHead V D (n + 1))
      (fun j => (rotateHead G (n + 1)).trans
        ((headTailEquiv V D (n + 1)).trans
          ((Equiv.prodCongr (pivotEquiv G n j) (Equiv.refl D)).trans
            (headTailEquiv (Edge V D) D n).symm))) k

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Edge, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.splitHead, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rotateHead, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.headTailEquiv

  114. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 730
  115. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.edgeAt_port line 744
  116. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 760
  117. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 764
  118. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 771
  119. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.projectedEventEquiv line 783
  120. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 802

    Source documentation

    Every fixed dart has exactly the same number of path realizations.

    theorem natCard_edgeAt_fiber (G : PortGraph V D) (n : Nat) (k : Fin (n + 1))
    (a : Edge V D) :
    Nat.card {w : Walk V D (n + 1) // edgeAt G n w k = a} = Nat.card D ^ n := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Edge, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.edgeAt

  121. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 812

    Source documentation

    The exact event count underlying the uniform-pivot probability law.

    theorem natCard_edgeAt_event (G : PortGraph V D) (n : Nat) (k : Fin (n + 1))
    (P : Edge V D → Prop) :
    Nat.card {w : Walk V D (n + 1) // P (edgeAt G n w k)} =
      Nat.card {a : Edge V D // P a} * Nat.card D ^ n := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Edge, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.Walk, OAI.MaxCutGames.Foundations.PCP.PoweringWalks.edgeAt

  122. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.leftFromPivot line 822
  123. def OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rightFromPivot line 828
  124. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 835
  125. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 839
  126. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 844
  127. theorem OAI.MaxCutGames.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 863