OAI/Computability/UniqueGames/PCP/SourceQueryLoopLemmas.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.Query line 18
2. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.State line 19
3. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.Label line 21
4. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.finish line 28
5. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.statement line 34
6. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.prefixBits line 46
7. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.prefixSteps line 52
8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.resultTapes_append line 58
9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.prefixTrace line 69
10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.prefixSteps_le line 121
11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.loopInTime line 134

    Source documentation

    The complete finite traversal, including its final exit transition.

    theorem loopInTime (u D n B : Nat) (queries : Nat → Query u D)
        (layout : SourceTestAppend.Layout K) (labels : Label u D n → Λ) (exit : Option Λ)
        (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State u D))
        (atLabels : ∀ l, p (labels l) = statement u D n queries layout labels exit l)
        (signature : Signature u) (initialQuery : Query u D)
        (base : K → List Bool) (values : Fin 3 → Nat)
        (sourceWords : ∀ side, base (layout.sources side) = encodeWord (values side))
        (scratchEmpty : base layout.scratch = []) (temporaryEmpty : base layout.temporary = [])
        (hbound : ∀ i, i < n → SourceTestAppend.steps u D values (signature, queries i) ≤ B) :
        ∃ lastQuery : Query u D,
          Nonempty (StateTransition.EvalsToInTime (TM2.step p)
            ⟨some (labels (.load ⟨0, by omega⟩)), ((signature, initialQuery), none), base⟩
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.State, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.statement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.steps

12. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple line 174

    Source documentation

    Interpret a radix tuple using the declared domain and codomain numbering.

    def decodeTuple {α β : Type} (a : Encoding α) (b : Encoding β)
        (digits : Fin a.size → Fin b.size) : α → β :=
    …

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

13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_function line 180

    Source documentation

    Increasing function rank is exactly the controller's tuple order, followed by the explicit coordinate decoder. This includes empty domains and codomains.

    theorem enumerate_function {α β : Type} (a : Encoding α) (b : Encoding β) :
        (a.function b).enumerate =
          (tupleOrder b.size a.size).map (decodeTuple a b) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.enumerate, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple

14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_fin_function line 186
15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.tupleTapeOrder line 198
16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_eq_tupleTapeOrder line 206
17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_flatMap_tupleTapeOrder line 213
18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.rankedQuery line 221

    Source documentation

    Total extension of the declared tape decoder, for the query loop's natural index register. Out-of-range values are never visited by that loop.

    def rankedQuery (u D : ℕ) (fallback : SourceQueryLoop.Query u D)
        (i : ℕ) : SourceQueryLoop.Query u D :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryLoop.Query

19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.rankedQuery_at line 227
20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_ofFn line 232
21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_enumerate line 247
22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_tupleTapeOrder line 261
23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder line 272

    Source documentation

    Clause, slot, left-query, noise, right-query loops, from outermost to innermost. Within each tuple loop coordinate zero changes fastest.

    def tupleSourceOrder (F : Formula) (u D : ℕ) : List (SourceIndex F u D) :=
    …

24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.sourceIndexEncoding_eq_tupleSourceOrder line 278
25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.rawSourceList_eq_tupleOrder line 297

    Source documentation

    Equality of ordered equation lists preserves every repeated occurrence.

    theorem rawSourceList_eq_tupleOrder (F : Formula) (u D : ℕ) :
        rawSourceList F u D = (tupleSourceOrder F u D).map (sourceEquation F u D) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder

26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.sourceList_eq_tupleOrder line 302
27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.rawSourceList_flatMap_tupleOrder line 306
28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.reverseAppend line 314

    Source documentation

    The stack update performed by one record append.

    def reverseAppend {α β : Type} (encode : α → List β)
        (accumulator : List β) (record : α) : List β :=
    …

29. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend line 320

    Source documentation

    After any ascending prefix, the accumulator is its reversed encoding followed by the original accumulator.

    theorem foldl_reverseAppend {α β : Type} (encode : α → List β)
        (records : List α) (accumulator : List β) :
        records.foldl (reverseAppend encode) accumulator =
          (records.flatMap encode).reverse ++ accumulator := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.reverseAppend

30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_header line 330
31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_prefix line 338

    Source documentation

    The prefix invariant is stated without requiring that the prefix end on the last record. A later suffix continues from exactly this accumulator.

    theorem foldl_reverseAppend_prefix {α β : Type} (encode : α → List β)
        (emitted remaining : List α) (header : List β) :
        (emitted ++ remaining).foldl (reverseAppend encode) header.reverse =
          remaining.foldl (reverseAppend encode)
            (header ++ emitted.flatMap encode).reverse := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.reverseAppend

32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.foldl_resultTapes line 347

    Source documentation

    The actual tape update used by SourceTestAppend has this same invariant; all other tapes remain the original tapes.

    theorem foldl_resultTapes {α K : Type} [DecidableEq K]
        (layout : SourceTestAppend.Layout K) (encode : α → List Bool)
        (records : List α) (base : K → List Bool) :
        records.foldl (fun tapes record =>
            SourceTestAppend.resultTapes layout tapes (encode record)) base =
          Function.update base layout.accumulator
            ((records.flatMap encode).reverse ++ base layout.accumulator) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes

33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.inputBits_eq_header_records line 365
34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.input_reverse_accumulator line 377
35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.sourceInput_tuple_reverse_accumulator line 387

    Source documentation

    The nonempty-formula branch can feed the accumulator directly from the tuple controller's occurrence order. The total-input invariant above also covers the separate singleton empty-formula branch.

    theorem sourceInput_tuple_reverse_accumulator (F : Formula) (u D : ℕ)
        (hD : 0 < D) (hne : F.clauses ≠ []) :
        (tupleSourceOrder F u D).foldl
            (reverseAppend (fun p => encodeWords
              (SourceEncoding.equationWords (sourceEquation F u D p))))
            (encodeWords [nBits F u, (sourceList F u D).length]).reverse =
          (SourceEncoding.inputBits (sourceInput F u D hD)).reverse := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.reverseAppend

36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.finalReverse_steps line 404

    Source documentation

    Applying the existing reversal machine to the accumulated records returns the exact serialized input in inputBits.length + 1 transitions. This is only the final reversal stage, not a bound for generating the records.

    theorem finalReverse_steps (input : SourceEncoding.Input) (register : Option Bool) :
        MachineReverse.next^[(SourceEncoding.inputBits input).length + 1]
          (some (MachineReverse.running
            (input.equations.foldl
              (reverseAppend (fun e => encodeWords (SourceEncoding.equationWords e)))
              (encodeWords [input.variables, input.equations.length]).reverse)
            [] register)) =
          some (MachineReverse.halted (SourceEncoding.inputBits input)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopOrder.reverseAppend

37. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.Tape line 425
38. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.currentAt line 429
39. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.remainingAt line 432
40. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits line 437

    Source documentation

    Set the active low coordinates; higher digits and every other tape retain their original contents. Unary digit stacks have no unread suffix.

    def setDigits (m : ℕ) {q : ℕ} (digits : Fin q → ℕ)
        (base : Tape u Extra → List Bool) : Tape u Extra → List Bool
      | .current i => if h : i.val < q then encodeWord (digits ⟨i.val, h⟩)
          else base (.current i)
      | .remaining i => if h : i.val < q then encodeWord (m - 1 - digits ⟨i.val, h⟩)
          else base (.remaining i)
      | k => base k

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.Tape

41. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setAcc line 445
42. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.putDigit line 448
43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits_zero line 452
44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits_extra line 458
45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setAcc_self line 462
46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setAcc_setAcc line 466
47. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setAcc_apply line 470
48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits_setAcc line 473
49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.putDigit_extra line 479
50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.putDigit_setAcc line 483
51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits_putDigit line 491

    Source documentation

    The low-coordinate assignment commutes with a separate higher digit.

    theorem setDigits_putDigit (m q : ℕ) (hq : q < u) (digits : Fin q → ℕ)
        (base : Tape u Extra → List Bool) (d r : ℕ) :
        setDigits m digits (putDigit ⟨q, hq⟩ base d r) =
          putDigit ⟨q, hq⟩ (setDigits m digits base) d r := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.putDigit

52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc line 512

    Source documentation

    The last coordinate is the outside loop coordinate.

    theorem setDigits_snoc (m q : ℕ) (hq : q < u) (digits : Fin q → ℕ)
        (d : ℕ) (base : Tape u Extra → List Bool) :
        setDigits m (Fin.snoc digits d) base =
          putDigit ⟨q, hq⟩ (setDigits m digits base) d (m - 1 - d) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.putDigit

53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc_base line 548
54. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.allBits line 554
55. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.blockPrefix line 557
56. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_eq_ofFn line 561
57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.blocks line 570
58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_all line 573
59. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.configuration line 580
60. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.BodyTrace line 583
61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.val_snoc line 594
62. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.zeros_snoc line 600
63. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.initialConfiguration line 605
64. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.finalConfiguration line 609
65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.exists_schedule line 615
66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.traversalInTime line 749

    Source documentation

    The time bound is derived from the concrete schedule, not from the number of tuples alone. Dimension zero consists of its single actual body trace.

    theorem traversalInTime
        (program : Λ → TM2.Stmt (fun _ : Tape u Extra => Bool) Λ (σ × Option Bool))
        (bodyLabel : Λ) (next resetLabel : ℕ → Λ) (canonical : σ) (accumulator : Extra)
        (positive : 0 < m) (B : ℕ) (base : Tape u Extra → List Bool)
        (bits : (Fin u → Fin m) → List Bool)
        (atCheck : ∀ i, i < u → program (next i) =
          increment (currentAt accumulator i) (remainingAt accumulator i) bodyLabel (resetLabel i))
        (atReset : ∀ i, i < u → program (resetLabel i) =
          reset (currentAt accumulator i) (remainingAt accumulator i) (resetLabel i) (next (i + 1)))
        (bodies : BodyTrace program bodyLabel (next 0) canonical accumulator base bits B) :
        Nonempty (StateTransition.EvalsToInTime (TM2.step program)
          (initialConfiguration (m := m) u bodyLabel canonical base)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.currentAt, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.remainingAt, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.BodyTrace, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.initialConfiguration

67. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.initial_current line 771
68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.initial_remaining line 777
69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.final_current line 782
70. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.final_remaining line 788
71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOdometerSchedule.final_accumulator line 794