OAI/Computability/UniqueGames/PCP/SourceMachine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.Alphabet line 16
2. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldLoop line 19

   Source documentation

   Read one unary field, stopping at its zero delimiter.

   def fieldLoop (source destination : K) (loopLabel : Λ) (exit : Option Λ) :
       TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.Alphabet

3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStart line 28

   Source documentation

   Seed the destination delimiter before scanning the unary payload.

   def fieldStart (destination : K) (loopLabel : Λ) :
       TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.Alphabet

4. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldTapes line 32
5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldTapes_source line 36
6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldTapes_destination line 41
7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldTapes_self line 46
8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldTapes_other line 50
9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.update_field_source line 56
10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.update_field_destination line 67
11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStep_delimiter line 73
12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStep_true line 87
13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldLoopTrace line 102

    Source documentation

    Exactly one transition per unary bit, including its terminating delimiter.

    theorem fieldLoopTrace (source destination : K) (hne : source ≠ destination)
        (loopLabel : Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.Alphabet

14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStartStep line 134
15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldInTime line 148
16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.afterField line 179

    Source documentation

    Stack state after one completed field, retaining an arbitrary old destination.

    def afterField (source destination : K) (base : K → List Bool)
        (n : Nat) (suffix : List Bool) : K → List Bool :=
    …

17. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldNext line 183
18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourTapes line 190
19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourTapes_source line 197
20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourTapes_other line 203
21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourField_time_eq_length line 209
22. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourFieldsInTime line 216

    Source documentation

    Four fields are separated by actual finite-stack transitions. The stated bound is exactly their serialized length plus four delimiter-seeding steps.

    def fourFieldsInTime (source : K) (destination : Fin 4 → K)
        (hsep : ∀ j, source ≠ destination j)
        (start loopLabel : Fin 4 → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.Alphabet

23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldDestination line 260
24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourTapes_concrete line 262
25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.groupingProgram line 274
26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.groupingMachine line 283

    Source documentation

    One concrete finite machine: five Boolean stacks, eight labels, and three internal states. Four destination stacks hold the four separated fields.

    def groupingMachine : FinTM2 where
    …

27. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.groupingMachineInTime line 296

    Source documentation

    The concrete machine's verified trace includes arbitrary unread input and arbitrary prior destination contents. No assumed algorithm remains here.

    def groupingMachineInTime (base : Fin 5 → List Bool) (a b c d : Nat) (suffix : List Bool)
        (hinput : base 0 = encodeWords [a, b, c, d] ++ suffix) (register : Option Bool) :
        StateTransition.EvalsToInTime groupingMachine.step
          ⟨some (0, false), ((), register), base⟩
          (some ⟨none, ((), none), fourTapes (0 : Fin 5) fieldDestination base a b c d suffix⟩)
          (a + b + c + d + 8) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fourTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldDestination