OAI/Computability/UniqueGames/Machines/MachineSubdivisionBodySpecLemmas.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.resultTapes line 27
2. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.bodyResult_eq line 38

   Source documentation

   Every tape at the body boundary, including all preserved headers and counters.

   theorem bodyResult_eq {q : Nat} (base : Tape → List Bool) (u v : Nat)
       (table : Target.PermutationTable q) (suffix : List Bool)
       (ready : Ready base u v table suffix) :
       bodyResult base u v table suffix = resultTapes base u v table suffix := by
   …

   Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.resultTapes

3. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.result_input line 49
4. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.result_locals line 56
5. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.result_accumulator line 67
6. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.encodeWord_succ line 75
7. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.result_indices line 78
8. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.rowBits line 93

   Source documentation

   Four whole rows, with the final table already in left-to-right orientation.

   def rowBits {q : Nat} (u middle first last v : Nat) (table : Target.PermutationTable q) :
       List Bool :=
   …

9. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.rowPayload_eq line 101
10. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.rowBits_eq_dynamic line 116

    Source documentation

    The natural-word description is literally the established finite-target constraint codec, rather than an alternative encoding.

    theorem rowBits_eq_dynamic {N q : Nat} (vertices : Fin 5 → Fin N)
        (table : Target.PermutationTable q) :
        rowBits (vertices 0).val (vertices 2).val (vertices 1).val (vertices 3).val
          (vertices 4).val table = MachineSubdivisionDynamicRows.rowBits vertices table := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.rowBits, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.rowBits

11. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBodySpec.bodyBudget_le line 125

    Source documentation

    One conservative bound uniform over all occurrences in this output. Only the fixed alphabet and the runtime header sizes appear in the polynomial.

    theorem bodyBudget_le {q : Nat} (base : Tape → List Bool) (u v : Nat)
        (table : Target.PermutationTable q) (suffix : List Bool)
        (ready : Ready base u v table suffix) (n Q e : Nat)
        (hu : u < n) (hv : v < n) (he : e ≤ Q)
        (middle : base .middle = encodeWord (n + e))
        (first : base .first = encodeWord (n + Q + 2 * e))
        (last : base .last = encodeWord (n + Q + 2 * e + 1)) :
        bodyBudget base u v table suffix ≤ 100 * (n + 3 * Q + q * (q + 1) + 1) := by
    …

12. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.bodyBits line 155
13. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.bodyBits_nil line 158
14. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.bodyBits_cons line 160
15. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.identityBits line 167
16. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.rowBits line 170
17. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.outputRows line 177
18. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.frame line 181
19. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.afterGuard line 192
20. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.frame_prepared line 196
21. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.guard_cons line 203
22. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.guard_nil line 224
23. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoopFrame.ready line 241
24. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.Involutive line 266
25. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.inverseTable_eq line 270
26. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.translations_involutive line 278
27. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.rowBits_eq_semantic line 299
28. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.outputRows_eq_ofFn line 318
29. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.outputRows_eq_semantic line 327
30. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.output_eq_gameBits line 338

    Source documentation

    Exact complete serialized output, including the changed headers and every forward permutation-table entry, in occurrence order.

    theorem output_eq_gameBits {q : Nat} (H : Instance q) (involutive : Involutive H) :
        MachineSubdivisionEmission.headerBits H.vertices q H.constraints.length ++
          outputRows H.constraints.length 0 H.constraints =
          gameBits (SubdivisionTarget.subdivide H) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCorrespondence.Involutive, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.headerBits, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide

31. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.rowPayload_eq line 356
32. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.bodyResult_eq_frame line 365
33. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.bodyBound line 388
34. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.bodyInTime line 390
35. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.loopInTime line 406

    Source documentation

    Every list occurrence is read once, emits exactly its four rows, and advances the three private numeric names. The loop includes its final zero-counter test.

    def loopInTime {n q : Nat} (Q e : Nat) (edges : List (Constraint n q))
        (emitted : List Bool) (fit : e + edges.length ≤ Q) :
        StateTransition.EvalsToInTime (machine q).step
          ⟨some .guard, initialState, frame Q e edges emitted⟩
          (some ⟨some .finishStart, initialState,
            frame Q (e + edges.length) ([] : List (Constraint n q))
              (emitted ++ outputRows Q e edges)⟩)
          (edges.length * (bodyBound n q Q + 1) + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionLoop.bodyBound

36. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.prefixPolynomial line 463
37. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.timePolynomial line 468
38. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.input_eq line 471
39. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.input_size line 475
40. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.finalTapes line 482
41. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.final_outputEmpty line 487
42. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.final_accumulator line 489
43. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.prefixInTime line 497

    Source documentation

    The prefix contains every actual header read, fresh-name initialization, header emission, complete four-row body, and occurrence-counter test.

    def prefixInTime {q : Nat} (H : Instance q) :
        StateTransition.EvalsToInTime (machine q).step
          (initList (machine q) (gameBits H))
          (some ⟨some .finishStart, initialState, finalTapes H⟩)
          ((prefixPolynomial q).eval (gameBits H).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.finalTapes, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.prefixPolynomial

44. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.fullRunInTime line 530

    Source documentation

    Literal initialization to literal clean halting configuration, with exact semantic subdivision output. No execution or runtime premise is assumed.

    def fullRunInTime {q : Nat} (H : Instance q) (involutive : Involutive H) :
        TM2OutputsInTime (machine q) (gameBits H)
          (some (gameBits (SubdivisionTarget.subdivide H)))
          ((timePolynomial q).eval (gameBits H).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.timePolynomial

45. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.computableInPolyTime line 540

    Source documentation

    The input subtype records the mathematical involution property, while the same finite transition program is used for every instance of the fixed alphabet.

    def computableInPolyTime (q : Nat) :
        TM2ComputableInPolyTime
          (fun H : {H : Instance q // Involutive H} => gameBits H.val)
          gameBits (fun H => SubdivisionTarget.subdivide H.val) where
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide

46. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.familyComputableInPolyTime line 555
47. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRuntime.workAlphabetFinite line 570
48. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCompose.certifiedOutput line 586
49. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCompose.certify line 591

    Source documentation

    Attach the already-proved property without executing anything or changing the input or output codec.

    def certify (upstream : TM2ComputableInPolyTime encode gameBits f)
        (involutive : ∀ a, Involutive (f a)) :
        TM2ComputableInPolyTime encode (fun H : {H : Instance q // Involutive H} => gameBits H.val)
          (certifiedOutput involutive) where
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCompose.certifiedOutput

50. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCompose.computableInPolyTime line 601
51. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCompose.finiteAlphabet line 609
52. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionCompose.translationComputableInPolyTime line 618

    Source documentation

    Binary-translation producers discharge the only table-law condition.

    def translationComputableInPolyTime {s : Nat}
        (coordinates : Fin q ≃ Integration.BinaryLinear.Vector s)
        (upstream : TM2ComputableInPolyTime encode gameBits f)
        (translations : ∀ a, Integration.TranslationTarget.IsTranslationInstance coordinates (f a)) :
        TM2ComputableInPolyTime encode gameBits (fun a => SubdivisionTarget.subdivide (f a)) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector, OAI.UniqueGamesTheorem.Integration.TranslationTarget.IsTranslationInstance, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide

53. inductive OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.Tape line 637
54. abbrev OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.Tape.enumList line 642
55. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.Tape.enumList_getElem?_ctorIdx_eq line 645
56. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.Tape.enumList_nodup line 649
57. instance OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.(instance at line 651) line 651
58. abbrev OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.State line 655
59. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.initialState line 657
60. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.headerField line 659
61. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.emitField line 664
62. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.tokens line 670
63. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.clearKeys line 673
64. inductive OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.Label line 677
65. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.headerNext line 686
66. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.emitEntry line 689
67. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.program line 692
68. def OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.machine line 708
69. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.covers line 719
70. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.accumulator_not_mem_clearKeys line 723
71. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformProgram.output_not_mem_clearKeys line 724
72. def OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.inputTapes line 737
73. def OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.afterVertices line 740
74. def OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.afterAlphabet line 743
75. def OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.resultTapes line 747
76. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.initList_eq line 752
77. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.first_result line 758
78. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.second_result line 766
79. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.third_result line 774
80. def OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.headersInTime line 784

    Source documentation

    The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number.

    def headersInTime (C q n Q : Nat) (body : List Bool) :
        StateTransition.EvalsToInTime (machine C).step
          (initList (machine C) (encodeWords [n, q, Q] ++ body))
          (some ⟨some (.scale 0), initialState, resultTapes n q Q body⟩)
          (n + q + Q + 6) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.resultTapes

81. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformHeaders.headers_budget line 819