OAI/Computability/UniqueGames/Reduction/MachineFieldTemplate.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token line 17
2. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.tokenOutput line 22
3. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateOutput line 26
4. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.tokenSteps line 29
5. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.workSteps line 33
6. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateSteps line 36
7. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.copiedLength line 39
8. inductive OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Label line 42
9. abbrev OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.State line 50
10. abbrev OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Alphabet line 51
11. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.reset line 53
12. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.reset_reset line 55
13. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.startAt line 57
14. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.jump line 60
15. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.identityEmit line 65
16. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.instruction line 69

    Source documentation

    Local finite labels are placed in an arbitrary caller label space, with an explicit continuation. Every instruction is determined by the fixed template.

    def instruction (tokens : List (Token q)) (field : Fin q → K) (scratch output : K)
        (place : Label tokens.length → Λ) (exit : Option Λ) :
        Label tokens.length → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Label, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.State

17. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.program line 89

    Source documentation

    A standalone local program, also usable with a local continuation.

    def program (tokens : List (Token q)) (field : Fin q → K) (scratch output : K)
        (exit : Option (Label tokens.length)) :
        Label tokens.length → TM2.Stmt (Alphabet (K := K)) (Label tokens.length) (State σ) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Label, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.State

18. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes line 96
19. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes_self line 99
20. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes_output line 102
21. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes_other line 105
22. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes_append line 109
23. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.fieldValues_outputTapes line 114
24. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.identity_output line 120
25. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.chain line 126
26. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.doneStep line 142
27. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.literalStep line 149
28. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.copySetupStep line 160
29. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.copyTrace line 170
30. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.tokenTrace line 193
31. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.suffixTrace line 210
32. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.phaseTrace line 256

    Source documentation

    The complete phase is derived from concrete instruction traces. The code placement premise identifies instructions; it assumes no whole-phase run.

    theorem phaseTrace (base : K → List Bool) (scratchEmpty : base scratch = [])
        (state : State σ) :
        (MachineComposition.advance (TM2.step P))^[templateSteps tokens (fun j => base (field j))]
          (some ⟨some (place (startAt tokens.length 0)), state, base⟩) =
          some ⟨exit, reset state,
            outputTapes base output (templateOutput tokens (fun j => base (field j)))⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.State, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateSteps, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.startAt, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.reset, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateOutput

33. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.programTrace line 270

    Source documentation

    Direct execution of the emitted local finite program; its instructions are discharged by construction rather than supplied by the caller.

    theorem programTrace (tokens : List (Token q)) (field : Fin q → K) (scratch output : K)
        (fieldScratch : ∀ j, field j ≠ scratch) (fieldOutput : ∀ j, field j ≠ output)
        (scratchOutput : scratch ≠ output) (exit : Option (Label tokens.length))
        (base : K → List Bool) (scratchEmpty : base scratch = []) (state : State σ) :
        (MachineComposition.advance (TM2.step (program tokens field scratch output exit)))^[
          templateSteps tokens (fun j => base (field j))]
          (some ⟨some (startAt tokens.length 0), state, base⟩) =
          some ⟨exit, reset state,
            outputTapes base output (templateOutput tokens (fun j => base (field j)))⟩ :=
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Label, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.State, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.program, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateSteps, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.startAt, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.reset, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.outputTapes, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateOutput

34. theorem OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateSteps_le line 282
35. def OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.phaseInTime line 295