OAI/Computability/UniqueGames/Machines/MachineExpanderRowCleanup.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape_zero line 11
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape_one line 12
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape_two line 13
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape_three line 14
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape_four line 15
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape_five line 16
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes line 20
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupSteps line 33
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupSteps_eq_sum line 42
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes_dirty line 46
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes_other line 53

    Source documentation

    Every tape outside the six named work roles keeps its exact contents.

    theorem cleanupTapes_other (ports : Tape → K) (base : K → List Bool) (k : K)
        (outside : ∀ i : Fin 6, k ≠ ports (dirtyTape i)) :
        cleanupTapes ports base k = base k := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes

12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes_table line 70
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes_inputVertex line 75
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes_output line 80
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.join_trace line 85
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupOneTraceAt line 92

    Source documentation

    One cleanup phase follows the actual drain instruction at its placed label.

    theorem cleanupOneTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
        (ports : Tape → K) (labels : Label d → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
        (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
        (i : Fin 6) (base : K → List Bool) (state : State ρ d) :
        (advance (TM2.step target))^[((base (ports (dirtyTape i))).length + 1)]
          (some ⟨some (labels (.cleanup i)), state, base⟩) =
          some ⟨some (if hi : i.val + 1 < 6 then labels (.cleanup ⟨i.val + 1, hi⟩)
              else labels .done),
            (state.1, none), Function.update base (ports (dirtyTape i)) []⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.dirtyTape

17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTraceAt line 111

    Source documentation

    All six phases execute in the common program, with exactly the sum of the six initial word lengths plus one empty-branch transition per tape.

    theorem cleanupTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
        (ports : Tape → K) (distinct : Function.Injective ports)
        (labels : Label d → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
        (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
        (base : K → List Bool) (state : State ρ d) :
        (advance (TM2.step target))^[cleanupSteps ports base]
          (some ⟨some (labels (.cleanup 0)), state, base⟩) =
          some ⟨some (labels .done), (state.1, none), cleanupTapes ports base⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes

18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.doneStepAt line 137

    Source documentation

    The done label transfers control without inspecting or modifying any tape.

    theorem doneStepAt (positive : 0 < d) (H : Table (cloudSize d) d)
        (ports : Tape → K) (labels : Label d → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
        (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
        (base : K → List Bool) (state : State ρ d) :
        TM2.step target ⟨some (labels .done), state, base⟩ = some ⟨exit, state, base⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement

19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupExitTraceAt line 148

    Source documentation

    Cleanup followed by the actual done-to-caller transition.

    theorem cleanupExitTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
        (ports : Tape → K) (distinct : Function.Injective ports)
        (labels : Label d → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
        (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
        (base : K → List Bool) (state : State ρ d) :
        (advance (TM2.step target))^[cleanupSteps ports base + 1]
          (some ⟨some (labels (.cleanup 0)), state, base⟩) =
          some ⟨exit, (state.1, none), cleanupTapes ports base⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupTapes

20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.initializedTapes line 165
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.initializeStepAt line 175

    Source documentation

    Initialization physically pushes four delimiters and resets the bit register.

    theorem initializeStepAt (positive : 0 < d) (H : Table (cloudSize d) d)
        (ports : Tape → K) (distinct : Function.Injective ports)
        (labels : Label d → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
        (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
        (base : K → List Bool) (state : State ρ d) :
        TM2.step target ⟨some (labels .initialize), state, base⟩ =
          some ⟨some (labels (.firstEmit (PCP.AlphabetTable.Emitter.labelAt 3 _ 0 .entry))),
            (state.1, none), initializedTapes ports base⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.initializedTapes

22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes line 188
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.clearQueryStepAt line 195

    Source documentation

    The query-clear phase removes one symbol from each of its two tapes and preserves the complete finite state and every other tape.

    theorem clearQueryStepAt (positive : 0 < d) (H : Table (cloudSize d) d)
        (ports : Tape → K) (distinct : Function.Injective ports)
        (labels : Label d → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
        (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
        (base : K → List Bool) (state : State ρ d) :
        TM2.step target ⟨some (labels .clearQuery), state, base⟩ =
          some ⟨some (labels (.secondEmit (PCP.AlphabetTable.Emitter.labelAt 3 _ 0 .entry))),
            state, clearedQueryTapes ports base⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes