OAI/Computability/MaxCut/Machines/AlphabetGraph.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

Explicit orders for the alphabet-reduction table

All executable maps use Boolean digits, finite sums, and division/remainder. No enumeration is chosen from a cardinality proof. Cube coordinate zero is the least significant bit; pairs of coordinates use row-major order. Event blocks are ordered by their original dart, followed by the local event. Vertices put events before vertex addresses before edge addresses. Each event has twelve ordered darts: six slots, with false then true orientation at each slot.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Address line 14
  2. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent line 16
  3. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Event line 19
  4. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.legal line 23
  5. instance OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.legalDecidable line 26
  6. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.restrictTape line 30
  7. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.extendTape line 33
  8. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.globalizeQuery line 37
  9. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.verifier line 42
  10. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.vertexBlock line 49
  11. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.edgeOracle line 52
  12. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 57
  13. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.response_eq_local line 69
  14. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.eventReject line 82
  15. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 87
  16. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.expect_prod line 100
  17. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.localAverage line 105
  18. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.expect_restrict_five line 109

    Source documentation

    Iterating the checked one-tape restriction identity preserves independence.

    theorem expect_restrict_five {B : Type*} [Fintype B] [DecidableEq B]
    (p : B → Prop) [DecidablePred p]
    (h : ({b // p b} → Bool) → ({b // p b} → Bool) → ({b // p b} → Bool) →
      ({b // p b} → Bool) → ({b // p b} → Bool) → ℝ) :
    (𝔼 f : B → Bool, 𝔼 g : B → Bool, 𝔼 r₀ : B → Bool,
      𝔼 r₁ : B → Bool, 𝔼 r₂ : B → Bool,
        h (UniformRestriction.restrict p f) (UniformRestriction.restrict p g)
          (UniformRestriction.restrict p r₀) (UniformRestriction.restrict p r₁)
          (UniformRestriction.restrict p r₂)) =
    𝔼 f : {b // p b} → Bool, 𝔼 g : {b // p b} → Bool,
      𝔼 r₀ : {b // p b} → Bool, 𝔼 r₁ : {b // p b} → Bool,
        𝔼 r₂ : {b // p b} → Bool, h f g r₀ r₁ r₂ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict

  19. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 147

    Source documentation

    Five independent full tapes restrict to five independent uniform legal tapes.

    theorem localAverage_eq_tester (G : ConstraintGraph V E A)
    (assignment : Address V E A → Bool) (e : E) :
    localAverage G assignment e = AlphabetReduction.edgeTesterReject (G.accepts e)
      (vertexBlock assignment (G.tail e)) (vertexBlock assignment (G.head e))
      (edgeOracle G assignment e) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Address, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.localAverage, OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.edgeTesterReject, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.vertexBlock, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.edgeOracle

  20. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.average line 165
  21. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.average_eq_testers line 170
  22. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.decodedLabeling line 179
  23. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.local_gap line 182
  24. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.average_gap line 199
  25. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 207
  26. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.average_eq_count line 220
  27. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.card_event line 227
  28. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.card_localEvent line 233

    Source documentation

    This factor depends only on the old alphabet, never on a dart predicate.

    theorem card_localEvent :
    Fintype.card (LocalEvent A) =
      4 * (2 * 2 ^ Fintype.card A) * (2 ^ (Fintype.card A * Fintype.card A)) ^ 5 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent

  29. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.card_address line 240
  30. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.rejection_count_bound line 248

    Source documentation

    The actual event count has a uniform loss of 2048, with no edge-dependent sample multiplicities. This count statement also permits an empty dart type.

    theorem rejection_count_bound [Fintype E] (G : ConstraintGraph V E A)
    (assignment : Address V E A → Bool) :
    Fintype.card (LocalEvent A) * G.rejectionCount (decodedLabeling assignment) ≤
      2048 * QueryIncidence.verifierRejectionCount (verifier G) assignment := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Address, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.decodedLabeling, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.verifierRejectionCount, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.verifier

  31. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.honestAssignment line 275
  32. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 280
  33. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 284
  34. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.honest_event line 293
  35. def OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph line 305
  36. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.perfect_completeness line 310
  37. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.gap_transfer line 317

    Source documentation

    The combined tester and incidence losses are 2048 × 6 = 12288.

    theorem gap_transfer [Fintype E] [DecidableEq V] [DecidableEq E]
    (G : ConstraintGraph V E A) (a b : Nat)
    (source : ∀ labeling : V → A,
      a * Fintype.card E ≤ b * G.rejectionCount labeling)
    (labeling : QueryIncidence.Vertex (Event E A) (Address V E A) → QueryIncidence.Label 6) :
    a * Fintype.card (QueryIncidence.Dart (Event E A) 6) ≤
      (b * 12288) * (graph G).rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Vertex, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Event, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Address, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Label, OAI.MaxCutGames.Foundations.PCP.QueryIncidence.Dart, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.graph

  38. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.alphabet_card line 343
  39. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 365
  40. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 367
  41. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 369
  42. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 373

    Source documentation

    Left component first, with the right component varying fastest.

    def productEquiv {A B : Type*} {a b : Nat} (left : A ≃ Fin a) (right : B ≃ Fin b) :
    A × B ≃ Fin (a * b) :=
…
  43. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 377
  44. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 384

    Source documentation

    The complete left block precedes the complete right block.

    def sumEquiv {A B : Type*} {a b : Nat} (left : A ≃ Fin a) (right : B ≃ Fin b) :
    A ⊕ B ≃ Fin (a + b) :=
…
  45. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 388
  46. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 392
  47. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 396
  48. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 397
  49. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 398
  50. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localCount line 399
  51. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 400
  52. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 401
  53. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 402
  54. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 403
  55. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 407

    Source documentation

    Explicit binary rank/unrank; the inverse extracts digits by division and remainder, as supplied by the executable finFunctionFinEquiv.

    def cubeEquiv (q : Nat) : Cube (Fin q) ≃ Fin (tapeCount q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount

  56. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 410
  57. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 411
  58. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 414
  59. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 417
  60. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 420
  61. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 428
  62. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 434
  63. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 436
  64. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 441
  65. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 444
  66. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 447
  67. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 450
  68. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 453
  69. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 456
  70. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 461
  71. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 465
  72. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 474
  73. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 479
  74. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 483
  75. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 488
  76. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 493
  77. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 498
  78. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 500
  79. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 504
  80. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 509
  81. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 517
  82. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 526
  83. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 533
  84. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 540
  85. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 547
  86. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 551
  87. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 558
  88. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 566
  89. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 574
  90. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered line 581

    Source documentation

    A reusable explicit increasing-index enumeration.

    def ordered {A : Type*} {count : Nat} (order : A ≃ Fin count) : List A :=
…
  91. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 584
  92. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 587
  93. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 592
  94. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 597
  95. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 599
  96. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 601
  97. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 608

    Source documentation

    Product enumeration visits the right factor completely at each left index.

    theorem ordered_product {A B : Type*} {a b : Nat}
    (left : A ≃ Fin a) (right : B ≃ Fin b) :
    ordered (productEquiv left right) =
      (ordered left).flatMap (fun x => (ordered right).map (fun y => (x, y))) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv

  98. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 625

    Source documentation

    Sum enumeration puts the whole left block before the whole right block.

    theorem ordered_sum {A B : Type*} {a b : Nat}
    (left : A ≃ Fin a) (right : B ≃ Fin b) :
    ordered (sumEquiv left right) =
      (ordered left).map Sum.inl ++ (ordered right).map Sum.inr := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv

  99. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 645
  100. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 648
  101. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 651
  102. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 660

    Source documentation

    Exact serialized occurrence order, including both orientations and every repeated local query: edge, local event, slot, then false and true.

    theorem ordered_dart (m q : Nat) :
    ordered (dartEquiv m q) =
      (List.finRange m).flatMap (fun edge =>
        (localEvents q).flatMap (fun event =>
          (List.finRange 6).flatMap (fun slot =>
            [(((edge, event), slot), false), (((edge, event), slot), true)]))) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents

  103. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 671
  104. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 674
  105. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 678
  106. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_event line 682
  107. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_address line 686
  108. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 690
  109. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 695
  110. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 700
  111. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.RawQuery line 714
  112. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent line 717
  113. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.mask line 720

    Source documentation

    Canonical full-cube proof address: every illegal coordinate is false.

    def mask {q : Nat} (P : Fin q → Fin q → Bool) (f : Cube (Fin q × Fin q)) :
    Cube (Fin q × Fin q) := fun p => if P p.1 p.2 then f p else false
  114. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.xorTape line 723
  115. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.andTape line 725
  116. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.inputPairTape line 728

    Source documentation

    The coordinate value of the paired input codeword before masking.

    def inputPairTape {q : Nat} (k : Bool × Cube (Fin q)) : Cube (Fin q × Fin q) :=
…
  117. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.query line 733

    Source documentation

    Actual six queries, computed directly from fixed full tapes and P. Padding slots repeat precisely the addresses used by eventQueries.

    def query {q : Nat} (P : Fin q → Fin q → Bool) (event : LocalEvent q)
    (slot : Fin 6) : RawQuery q :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.RawQuery

  118. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.globalize line 755

    Source documentation

    Attach the actual endpoints and edge identifier to a local raw address.

    def globalize {q : Nat} {V E : Type*} (tail head : V) (edge : E) :
    RawQuery q → AlphabetGraph.Address V E (Fin q)
  | .inl (side, tape) => .inl ((if side then head else tail), tape)
  | .inr tape => .inr (edge, tape)

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.RawQuery, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.Address

  119. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.mask_idempotent line 760
  120. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.mask_of_empty line 765
  121. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.query_is_masked line 772

    Source documentation

    Every joint-table query is already a canonical masked full tape.

    theorem query_is_masked {q : Nat} (P : Fin q → Fin q → Bool)
    (event : LocalEvent q) (slot : Fin 6) :
    match query P event slot with
    | .inl _ => True
    | .inr tape => mask P tape = tape := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.query, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.mask

  122. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.extendQuery line 784

    Source documentation

    Proof-only comparison map: extend the original legal-coordinate addresses. The executable query function above never calls this map.

    def extendQuery {q : Nat} (P : Fin q → Fin q → Bool) :
    AlphabetReduction.InputCoordinate (Fin q) ⊕ Cube (AlphabetReduction.LegalPair P) →
      RawQuery q
  | .inl k => .inl k
  | .inr tape => .inr (UniformRestriction.extend (fun p : Fin q × Fin q => P p.1 p.2 = true) tape)

/-- Pointwise equality with the existing tester after restricting all five
full input tapes and canonically extending the resulting query. The statement
does not require any legal pair to exist. -/

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.InputCoordinate, OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.LegalPair, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.RawQuery, OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend

  123. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.query_eq_extend_eventQueries line 793

    Source documentation

    Pointwise equality with the existing tester after restricting all five full input tapes and canonically extending the resulting query. The statement does not require any legal pair to exist.

    theorem query_eq_extend_eventQueries {q : Nat} (P : Fin q → Fin q → Bool)
    (kind : Fin 4) (k : AlphabetReduction.InputCoordinate (Fin q))
    (f g r₀ r₁ r₂ : Cube (Fin q × Fin q)) (slot : Fin 6) :
    query P (kind, k, f, g, r₀, r₁, r₂) slot =
      extendQuery P (AssignmentTester.eventQueries (AlphabetReduction.pairEncoding P) kind k
        (UniformRestriction.restrict (fun p : Fin q × Fin q => P p.1 p.2 = true) f)
        (UniformRestriction.restrict (fun p : Fin q × Fin q => P p.1 p.2 = true) g)
        (UniformRestriction.restrict (fun p : Fin q × Fin q => P p.1 p.2 = true) r₀)
        (UniformRestriction.restrict (fun p : Fin q × Fin q => P p.1 p.2 = true) r₁)
        (UniformRestriction.restrict (fun p : Fin q × Fin q => P p.1 p.2 = true) r₂) slot) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.InputCoordinate, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.query, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.extendQuery, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventQueries, OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.pairEncoding, OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict

  124. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.globalize_extendQuery line 808
  125. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.globalize_query line 821

    Source documentation

    The executable raw queries are exactly the actual verifier queries after attaching the endpoints and edge tag. This includes self-loops, duplicate queries, empty legal relations, and every original five-tape event.

    theorem globalize_query {q : Nat} {V E : Type*}
    (G : ConstraintGraph V E (Fin q)) (e : E) (event : LocalEvent q) (slot : Fin 6) :
    globalize (G.tail e) (G.head e) e (query (G.accepts e) event slot) =
      (AlphabetGraph.verifier G).query (e, event) slot := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.globalize, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Queries.query, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.verifier