OAI/Computability/MaxCut/Machines/Relations.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.sameAddress line 16

   Source documentation

   Exact local address comparison. A loop identifies the two endpoint tables; the joint edge table is always disjoint from every endpoint table.

   def sameAddress (selfLoop : Bool) : RawQuery q → RawQuery q → Bool
     | .inl (side, f), .inl (side', g) => ((side == side') || selfLoop) && decide (f = g)
     | .inr f, .inr g => decide (f = g)
     | _, _ => false

2. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.sameAddress_refl line 21
3. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.globalize_eq_iff line 25
4. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.eqProfile line 41
5. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_refl line 44
6. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot line 48

   Source documentation

   Search the fixed six positions for the least occurrence of an address.

   def canonicalSlot (selfLoop : Bool) (queries : Fin 6 → RawQuery q) (i : Fin 6) : Fin 6 :=
   …

7. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_profile line 51
8. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_le line 57
9. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.RepeatedConsistent line 62
10. instance OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistentDecidable line 66
11. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept line 71
12. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.predicate line 77
13. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relation line 84

    Source documentation

    A complete 64-by-64 Boolean relation in the shared row-major table format.

    def relation (P : Fin q → Fin q → Bool) (selfLoop : Bool)
        (event : AlphabetGraph.LocalEvent (Fin q)) (slot : Fin 6) (orientation : Bool) :
        GraphTables.RelationTable :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.MaxCutGames.Foundations.PCP.GraphTables.RelationTable

14. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation line 91
15. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relation_reverse line 99
16. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate line 108

    Source documentation

    The old predicate is read in the same row-major order as a graph row.

    def oldPredicate (old : Vector Bool (q * q)) (a b : Fin q) : Bool :=
    …

17. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable line 111
18. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate_relationAt line 115
19. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable_eq line 118
20. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_query_iff line 127
21. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_eq line 135
22. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistent_iff line 144
23. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.verifier_accepts line 155
24. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept_eq line 162
25. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation_graph line 176

    Source documentation

    Every stored bit is the actual six-query incidence predicate under the canonical explicit six-bit label enumeration, including loops and repeats.

    theorem relationAt_relation_graph (G : ConstraintGraph V E (Fin q)) (e : E)
        (event : AlphabetGraph.LocalEvent (Fin q)) (slot : Fin 6) (orientation : Bool)
        (a b : GraphTables.Label) :
        GraphTables.relationAt
            (relation (G.accepts e) (decide (G.tail e = G.head e)) event slot orientation) a b =
          (AlphabetGraph.graph G).accepts (((e, event), slot), orientation)
            (Enumeration.labelEquiv.symm a) (Enumeration.labelEquiv.symm b) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.relationAt, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Relations.relation, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph, OAI.MaxCutGames.Foundations.PCP.accepts

26. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart line 196

    Source documentation

    One directed occurrence, without merging repeated queries or equal rows.

    def rowFromDart (input : GenericGraphTables.Table q)
        (dart : QueryIncidence.Dart (AlphabetGraph.Event (Fin input.darts) (Fin q)) 6) :
        GraphTables.DartRow (Enumeration.vertexCount input.vertices input.darts q)
          (Enumeration.dartCount input.darts q) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Dart, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Event, OAI.MaxCutGames.Foundations.PCP.GraphTables.DartRow, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount

27. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows line 215

    Source documentation

    The row number decodes to precisely one event/slot/orientation occurrence.

    def rows (input : GenericGraphTables.Table q) :
        GraphTables.Rows (Enumeration.vertexCount input.vertices input.darts q)
          (Enumeration.dartCount input.darts q) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.Rows, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount

28. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows_at line 221
29. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 228

    Source documentation

    Reversal changes only the occurrence's orientation, preserving event and slot.

    theorem rows_reverseIndex (input : GenericGraphTables.Table q)
        (index : Fin (Enumeration.dartCount input.darts q)) :
        (rows input)[index].reverseIndex =
          Enumeration.dartEquiv input.darts q
            (((Enumeration.dartEquiv input.darts q).symm index).1,
              !((Enumeration.dartEquiv input.darts q).symm index).2) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv

30. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.dartRow_ext_inline_Table line 236
31. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.relation_ext_inline_Table line 246
32. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 260

    Source documentation

    The three stored fields agree with the actual alphabet graph at this dart.

    theorem rowFromDart_eq_graphRow (input : GenericGraphTables.Table q)
        (dart : QueryIncidence.Dart (AlphabetGraph.Event (Fin input.darts) (Fin q)) 6) :
        rowFromDart input dart =
          { tail := Enumeration.vertexEquiv input.vertices input.darts q
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Dart, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Event, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv

33. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 301

    Source documentation

    Equality of the full row vector, including all multiplicities and reversal indices.

    theorem rows_eq_graphRows (input : GenericGraphTables.Table q) :
        rows input = GraphTables.graphRows
          (GraphTables.enumeratedGraph (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows, OAI.MaxCutGames.Foundations.PCP.GraphTables.graphRows, OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

34. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rows_valid line 312
35. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build line 317

    Source documentation

    Actual executable output table. Its validity proof is erased at execution.

    def build (input : GenericGraphTables.Table q) : GraphTables.Table where
    …

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

36. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build_vertices line 323
37. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build_darts line 326
38. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.table_rows_congr_inline_Table line 329
39. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr_inline_Table line 335
40. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 343

    Source documentation

    Exact table equality in the explicit enumerations, without a representation choice.

    theorem build_eq_ofEnumeratedGraph (input : GenericGraphTables.Table q) :
        build input =
          GraphTables.ofEnumeratedGraph (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.GraphTables.ofEnumeratedGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

41. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.semantics_build line 352

    Source documentation

    Full decoded graph equality, including reversal, endpoints, and every predicate bit.

    theorem semantics_build (input : GenericGraphTables.Table q) :
        GraphTables.semantics (build input) =
          GraphTables.enumeratedGraph (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.GraphTables.enumeratedGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

42. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.decode_build line 361

    Source documentation

    Encoding and decoding the executable output recovers the full intended table.

    theorem decode_build (input : GenericGraphTables.Table q) :
        GraphTables.decodeTableBits (GraphTables.tableBits (build input)) =
          some (GraphTables.ofEnumeratedGraph
            (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.decodeTableBits, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.GraphTables.ofEnumeratedGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

43. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 369
44. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 382
45. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 393
46. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.gap_transfer line 408

    Source documentation

    The gap statement transfers to every labeling of the actual numbered table.

    theorem gap_transfer [Nonempty (Fin q)] (input : GenericGraphTables.Table q) (a b : Nat)
        (source : ∀ labeling : Fin input.vertices → Fin q,
          a * input.darts ≤ b * (GenericGraphTables.semantics input).rejectionCount labeling)
        (labeling : Fin (build input).vertices → GraphTables.Label) :
        a * (build input).darts ≤
          (b * 12288) * (GraphTables.semantics (build input)).rejectionCount labeling := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics

47. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 433

    Source documentation

    The serialized row list follows the same explicit occurrence order as the vector.

    theorem rowList_eq_ordered (input : GenericGraphTables.Table q) :
        GraphTables.rowList (build input) =
          (Enumeration.ordered (Enumeration.dartEquiv input.darts q)).map
            (rowFromDart input) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.rowList, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart

48. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 443

    Source documentation

    Complete output words: two headers followed by every ordered row block.

    theorem tableWords_eq_ordered (input : GenericGraphTables.Table q) :
        GraphTables.tableWords (build input) =
          [Enumeration.vertexCount input.vertices input.darts q,
            Enumeration.dartCount input.darts q] ++
            (Enumeration.ordered (Enumeration.dartEquiv input.darts q)).flatMap
              (fun dart => GraphTables.rowWords (rowFromDart input dart)) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableWords, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.GraphTables.rowWords, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart

49. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowList_length line 452
50. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.tableWords_length line 456
51. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 461
52. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 486
53. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.OutputDart line 489
54. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 492

    Source documentation

    The number of local verifier events for an alphabet with q symbols.

    def localEventFactor (q : Nat) : Nat :=
    …

55. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 495
56. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.dartFactor line 497
57. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 499
58. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 501
59. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 510

    Source documentation

    Real gaps transfer without rational approximation, including an empty old dart type. The loss is exactly 2048 * 6 = 12288.

    theorem gap_transfer_real [Fintype E] [DecidableEq V] [DecidableEq E]
        (G : ConstraintGraph V E A) (eps : ℝ) (_eps_nonnegative : 0 ≤ eps)
        (source : ∀ labeling : V → A,
          eps * (Fintype.card E : ℝ) ≤ (G.rejectionCount labeling : ℝ))
        (labeling : OutputVertex V E A → QueryIncidence.Label 6) :
        (eps / 12288) * (Fintype.card (OutputDart E A) : ℝ) ≤
          ((AlphabetGraph.graph G).rejectionCount labeling : ℝ) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.OutputDart, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph

60. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 549
61. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 559
62. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.card_output_total line 566
63. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 576

    Source documentation

    One coefficient depending only on the alphabet bounds the actual total number of output vertices and darts.

    theorem card_output_total_le :
        Fintype.card (OutputVertex V E A) + Fintype.card (OutputDart E A) ≤
          sizeFactor (Fintype.card A) * (Fintype.card V + Fintype.card E) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.OutputDart, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor

64. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 594
65. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 600
66. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.gap_transfer_real line 618

    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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics

67. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.build_vertices line 647

    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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor

68. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.build_darts line 658

    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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.dartFactor

69. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.build_total line 666
70. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.build_total_le line 674

    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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor

71. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.build_vertices_le line 691
72. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.build_darts_le line 696
73. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTableBounds.sizeFactor_positive line 701