OAI/Computability/UniqueGames/PCP/SourceOccurrences.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Executable radix numbering of padded global long-code tables and an ordered equation occurrence list. The code enumerates random tapes, not distinct equations: coinciding equations and repeated variable occurrences are retained.

  1. structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding line 25

    Source documentation

    A concrete, reversible finite encoding. Constructors below specify the actual arithmetic; no arbitrary Fintype.equivFin is used.

    structure Encoding (α : Type) where
…
  2. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.fin line 31
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.bool line 32
  4. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.unit line 33
  5. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.prod line 36

    Source documentation

    The second component is the low-order block coordinate.

    def prod {α β : Type} (a : Encoding α) (b : Encoding β) : Encoding (α × β) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding

  6. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.sum line 40

    Source documentation

    The right summand follows the whole left block.

    def sum {α β : Type} (a : Encoding α) (b : Encoding β) : Encoding (α ⊕ β) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding

  7. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.function line 44

    Source documentation

    Function coordinate zero is the least significant radix digit.

    def function {α β : Type} (a : Encoding α) (b : Encoding β) : Encoding (α → β) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding

  8. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 52
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 54
  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 57
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 61
  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 64
  13. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.GlobalKey line 72

    Source documentation

    Distinct table vertices and the three side tags never share storage. Unused ambient query positions are harmless explicit padding.

    abbrev GlobalKey (V C I J : Type) := (V × Cube I) ⊕ ((C × Cube J) ⊕ Unit)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  14. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.globalEncoding line 74
  15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 80
  16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendRestricted line 86

    Source documentation

    Extending by false gives a unique padded address to a restricted query.

    def extendRestricted {J : Type} (valid : J → Bool)
    (f : Cube {j : J // valid j = true}) : Cube J :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 90
  18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 94
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 101
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 107
  21. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 114

    Source documentation

    The global index map is an explicit equivalence, including all padding.

    def assignmentOfKey {V C I J : Type}
    (v : Encoding V) (c : Encoding C) (i : Encoding I) (j : Encoding J)
    (bits : GlobalKey V C I J → Bool) : Fin (globalEncoding v c i j).size → Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.GlobalKey, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.globalEncoding

  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 119
  23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 125
  24. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.localAddress line 137
  25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.localAddress_injective line 144
  26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 169
  27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 178
  28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.findValid line 208

    Source documentation

    A terminating first-valid search on the explicitly ordered ambient list.

    def findValid {J : Type} (valid : J → Bool) : List J → Option {j : J // valid j = true}
  | [] => none
  | j :: rest => if h : valid j = true then some ⟨j, h⟩ else findValid valid rest
  29. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 212
  30. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.firstValid line 221
  31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 224
  32. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.occurrenceList line 230

    Source documentation

    Mapping the ordered enumeration preserves all sampled occurrences.

    def occurrenceList {Tape Name : Type} (tape : Encoding Tape)
    (emit : Tape → Equation Name) : List (Equation Name) := tape.enumerate.map emit

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding

  33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 233
  34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum line 237
  35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.countP_enumerate line 243
  36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 252

    Source documentation

    Exact satisfaction fraction of the actual ordered equation list equals the uniform random-tape expectation, even when equations or addresses repeat.

    theorem occurrenceList_acceptance {Tape Name : Type} [Fintype Tape]
    (tape : Encoding Tape) (emit : Tape → Equation Name) (bits : Name → Bool) :
    ((occurrenceList tape emit).countP (fun e => satisfied e bits) : ℝ) /
        (occurrenceList tape emit).length =
      𝔼 x, if satisfied (emit x) bits then (1 : ℝ) else 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.occurrenceList

  37. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 267
  38. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.slotEncoding line 269
  39. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.iEncoding line 277
  40. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.jEncoding line 278
  41. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.variableEncoding line 279
  42. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.clauseEncoding line 281
  43. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 283
  44. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.proofEncoding line 286
  45. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.nBits line 290
  46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.nBits_eq line 292
  47. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.dummyIndex line 296
  48. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.leftAnchor line 299
  49. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rightAnchor line 301
  50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 304
  51. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 310

    Source documentation

    Independent actual half-tables extend to the explicit padded key space. Only the canonically selected right anchor is read at each clause context.

    def halfTableKeyAssignment (F : Target.Formula) (u : ℕ)
    (a : VariableContext F u → HalfCube (leftAnchor u) → Bool)
    (b : ∀ c : ClauseContext F u, ∀ j₀ : {j : J u // validJ F c j = true},
      HalfCube j₀ → Bool) :
    GlobalKey (VariableContext F u) (ClauseContext F u) (I u) (J u) → Bool
  | .inl (v, f) => a v (canonicalInput (leftAnchor u) f)
  | .inr (.inl (c, g)) =>
    match rightAnchor F c with
    | none => false
    | some j₀ => b c j₀ (canonicalInput j₀ (restrictQuery (validJ F c) g))
  | .inr (.inr _) => false

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.leftAnchor, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.GlobalKey, OAI.UniqueGamesTheorem.Foundations.Hastad.canonicalInput, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rightAnchor, OAI.UniqueGamesTheorem.Foundations.Hastad.restrictQuery

  52. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendHalfTables line 322
  53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 329
  54. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 340
  55. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.emptyAddress line 357
  56. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.contextEquation line 364

    Source documentation

    The private query law depends only on the two visible contexts. In particular, the hidden sampled slots are not inputs to pi.

    def contextEquation (F : Target.Formula) (u D : ℕ)
    (c : ClauseContext F u) (v : VariableContext F u)
    (t : SourceTape.TestTape (I u) (J u) D) : Equation (Fin (nBits F u)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.nBits

  57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.leftResponse line 373
  58. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rightResponse line 377
  59. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 384
  60. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 401
  61. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.SourceIndex line 405
  62. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 408
  63. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceEquation line 411
  64. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rawSourceList line 417

    Source documentation

    The entire finite random-tape population, including repeated visible contexts and all equation multiplicities, in a fixed explicit order.

    def rawSourceList (F : Target.Formula) (u D : ℕ) : List (Equation (Fin (nBits F u))) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.nBits

  65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 420
  66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 427
  67. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 452

    Source documentation

    A satisfiable totalization for the empty input formula, without changing or diluting the occurrence list of a nonempty formula.

    def emptyFormulaEquation (F : Target.Formula) (u : ℕ) : Equation (Fin (nBits F u)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.nBits

  68. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceList line 455
  69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceList_empty line 458
  70. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 461
  71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 467
  72. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 476
  73. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.sourceInput line 487
  74. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 491