OAI/Computability/UniqueGames/PCP/QueriesLemmas.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Executable six-query generation on fixed full Boolean cubes. The event type is exactly AlphabetGraph.LocalEvent, including all five full tapes. Only the returned joint-table addresses are masked outside the input relation; no legal-pair enumeration or change of sample multiplicities occurs.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.RawQuery line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.LocalEvent line 20
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.mask line 23

    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
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.xorTape line 26
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.andTape line 28
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.inputPairTape line 31

    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) :=
…
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.query line 36

    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.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.RawQuery

  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.globalize line 58

    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.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.RawQuery, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Address

  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.mask_idempotent line 63
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.mask_of_empty line 68
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.query_is_masked line 75

    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.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.query, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.mask

  12. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.extendQuery line 87

    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.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.InputCoordinate, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.LegalPair, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.RawQuery, OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend

  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.query_eq_extend_eventQueries line 96

    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.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.InputCoordinate, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.query, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.extendQuery, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventQueries, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.pairEncoding, OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict

  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.globalize_extendQuery line 111
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.globalize_query line 124

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.globalize, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Queries.query, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.verifier

  16. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.sameAddress line 147

    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
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.sameAddress_refl line 152
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.globalize_eq_iff line 156
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.eqProfile line 172
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.eqProfile_refl line 175
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.canonicalSlot line 179

    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 :=
…
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_profile line 182
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_le line 188
  24. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.RepeatedConsistent line 193
  25. instance OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.repeatedConsistentDecidable line 197
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.incidenceAccept line 202
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.predicate line 208
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relation line 215

    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.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.RelationTable

  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relationAt_relation line 222
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relation_reverse line 230
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.oldPredicate line 239

    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 :=
…
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relationFromTable line 242
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.oldPredicate_relationAt line 246
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relationFromTable_eq line 249
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.eqProfile_query_iff line 259
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_eq line 267
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.repeatedConsistent_iff line 276
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.verifier_accepts line 287
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.incidenceAccept_eq line 294
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relationAt_relation_graph line 308

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationAt, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Relations.relation, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph, OAI.UniqueGamesTheorem.Foundations.PCP.accepts