OAI/Computability/UniqueGames/Machines/PoweringMachineRowBody.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.capacity line 15
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.bufferSize line 16
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.State line 17
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.commands line 19
5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Label line 22
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.planMain line 27

   Source documentation

   A finite main label also exists for an empty command list.

   def planMain {max : Nat} {E : Type}
       (ops : List (PoweringMachinePlan.Command d max)) (fallback : E) :
       PoweringMachinePlan.Label ops ⊕ E :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Command, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Label

7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.plan_entry_eq line 34
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.entry line 41
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.headerPlacement line 45

   Source documentation

   Only the header phase directs shared output role 10 to the external output.

   def headerPlacement {max : Nat} (placement : PoweringMachineTapes.Tape max → K)
       (output : K) (i : PoweringMachineTapes.Tape max) : K :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape

10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_output line 50
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_other line 55
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_injective line 61
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_excludes_data line 77
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.instruction line 89
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.afterPlan line 100
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.rowRelation line 104
17. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.rowWords line 109
18. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.afterEmit line 114
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes line 121
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.planSteps line 129
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.planSteps_eq line 134
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.steps line 147
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Ready line 152
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.plan_other line 157
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.afterEmit_data line 170
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.afterEmit_role line 177
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.afterEmit_ready line 187
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes_data line 209
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes_ready line 222
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes_other line 247
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.rowBlock_eq_rowRelation line 266
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes_output line 283

    Source documentation

    The full serialized row is prepended to the caller's existing output.

    theorem finalTapes_output (graph : PortTables.Table vertices d) (n : Nat)
        (placement : PoweringMachineTapes.Tape (capacity n) → K) (distinct : Function.Injective placement)
        (output : K) (outside : ∀ i, output ≠ placement i) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool) (base : K → List Bool)
        (suffix : List Bool) (ready : Ready graph n placement vertex suffix base) :
        finalTapes graph n placement output vertex ports direction base output =
          encodeWords (rowWords graph n vertex ports direction) ++ base output := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Ready, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.rowWords

33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.rowTrace line 314

    Source documentation

    The complete row producer executes its concrete plan, one row transition, and the concrete two-header writer. No local execution hypothesis is assumed.

    theorem rowTrace (graph : PortTables.Table vertices d) (n : Nat)
        (placement : PoweringMachineTapes.Tape (capacity n) → K) (distinct : Function.Injective placement)
        (output : K) (outside : ∀ i, output ≠ placement i) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool)
        (labels : Label n ports direction → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State d n))
        (atLabels : ∀ l, program (labels l) = instruction n placement output ports direction labels exit l)
        (base : K → List Bool) (suffix : List Bool) (ready : Ready graph n placement vertex suffix base) :
        (advance (TM2.step program))^[steps graph vertex n ports direction]
          (some ⟨some (labels (entry n ports direction)), PoweringMasterState.clean (bufferSize d n), base⟩) =
          some ⟨exit, PoweringMasterState.clean (bufferSize d n),
            finalTapes graph n placement output vertex ports direction base⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.State, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Ready, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes

34. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.budget line 366
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.steps_le line 370
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.rowInTime line 383

    Source documentation

    The row subroutine's genuine execution certificate has the explicit fixed-parameter affine bound in the serialized graph length.

    def rowInTime (graph : PortTables.Table vertices d) (n : Nat)
        (placement : PoweringMachineTapes.Tape (capacity n) → K) (distinct : Function.Injective placement)
        (output : K) (outside : ∀ i, output ≠ placement i) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool)
        (labels : Label n ports direction → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State d n))
        (atLabels : ∀ l, program (labels l) = instruction n placement output ports direction labels exit l)
        (base : K → List Bool) (suffix : List Bool) (ready : Ready graph n placement vertex suffix base) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labels (entry n ports direction)), PoweringMasterState.clean (bufferSize d n), base⟩
          (some ⟨exit, PoweringMasterState.clean (bufferSize d n),
            finalTapes graph n placement output vertex ports direction base⟩)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.State, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.Ready, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.finalTapes