OAI/Computability/UniqueGames/Machines/MachineClone100Loop.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.Record line 17
2. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordWords line 23
3. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordBits line 24
4. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordsBits line 25
5. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.clonedRecordBits line 27
6. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.clonedRecordsBits line 30
7. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordFields line 33
8. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.tapes line 38

   Source documentation

   The frame records all tapes, including untouched header and output tapes. At every loop guard the four fields are empty and scratch is empty.

   def tapes (base : Tape → List Bool) (input counter accumulator : List Bool)
       (fields : Fin 4 → List Bool) : Tape → List Bool
     | .input => input
     | .header => base .header
     | .counter => counter
     | .field j => fields j
     | .scratch => []
     | .reversed => accumulator
     | .output => base .output

9. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.update_reversed line 48
10. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.counterTapes_eq line 55
11. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.fourTapes_eq line 63
12. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.clearFields_eq line 78
13. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.cleanupSteps_eq line 85
14. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordBits_length line 92
15. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.bodyCost line 97
16. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.bodyCost_eq line 100
17. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.bodyInTime line 107
18. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopCost line 156
19. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopCost_eq line 160
20. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopInTime line 173

    Source documentation

    The complete record loop consumes exactly the specified occurrence list. The final zero guard retains the counter delimiter for the final cleanup stage. Arbitrary suffixes and already emitted prefixes are preserved explicitly.

    def loopInTime (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
        (base : Tape → List Bool) (suffix : List Bool) (rs : List Record) (acc : List Bool) :
        StateTransition.EvalsToInTime (TM2.step (program triples nonempty))
          ⟨some .guard, initialState _,
            tapes base (recordsBits rs ++ suffix) (encodeWord rs.length) acc (fun _ => [])⟩
          (some ⟨some .finalCounter, initialState _,
            tapes base suffix (encodeWord 0) ((clonedRecordsBits triples rs).reverse ++ acc)
              (fun _ => [])⟩)
          (loopCost triples.length rs) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.Record, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.tapes, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordsBits, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.clonedRecordsBits, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopCost

21. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.loopInTime_linear line 208

    Source documentation

    A linear bound derived from the actual composed execution.

    def loopInTime_linear (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
        (base : Tape → List Bool) (suffix : List Bool) (rs : List Record) (acc : List Bool) :
        StateTransition.EvalsToInTime (TM2.step (program triples nonempty))
          ⟨some .guard, initialState _,
            tapes base (recordsBits rs ++ suffix) (encodeWord rs.length) acc (fun _ => [])⟩
          (some ⟨some .finalCounter, initialState _,
            tapes base suffix (encodeWord 0) ((clonedRecordsBits triples rs).reverse ++ acc)
              (fun _ => [])⟩)
          ((2 + 3 * triples.length) * (recordsBits rs).length +
            (9 + 12 * triples.length) * rs.length + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.Record, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.tapes, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordsBits, OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.clonedRecordsBits

22. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordOfEquation line 220
23. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.recordsBits_equations line 223
24. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.clonedRecordsBits_equations_table line 233
25. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Loop.sourceLoopInTime_table line 244