OAI/Computability/MaxCut/Machines/MachineRegisterEmit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.Alphabet line 14
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.finish line 16
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.emitStatement line 22

    Source documentation

    The fixed literal push chain executes in one TM2 transition.

    def emitStatement (destination : K) (offset : Nat) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.Alphabet

  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.emitStep line 26
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.prefix_encodeWord line 37
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.registerEmitTrace line 42

    Source documentation

    Caller-program form of the full exact trace. No execution premise is used.

    theorem registerEmitTrace (source destination scratch : K)
    (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
    (destinationScratch : destination ≠ scratch) (offset : Nat)
    (firstLabel secondLabel emitLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.Alphabet

  7. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.registerEmitInTime line 72

    Source documentation

    Timed witness retaining the exact 2*n+5-transition execution.

    def registerEmitInTime (source destination scratch : K)
    (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
    (destinationScratch : destination ≠ scratch) (offset : Nat)
    (firstLabel secondLabel emitLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.Alphabet

  8. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.program line 96

    Source documentation

    The three labels are transfer, restore-and-copy, and fixed-offset emission.

    def program (source destination scratch : K) (offset : Nat) (exit : Option (Fin 3)) :
    Fin 3 → TM2.Stmt (Alphabet (K := K)) (Fin 3) (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.Alphabet

  9. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.programInTime line 104
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.machine line 120

    Source documentation

    Three Boolean stacks, three labels, and one optional Boolean register.

    def machine (offset : Nat) : FinTM2 where
…
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.machineInTime line 131
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.emitStatement_pushes line 143
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.program_pushes_le line 149
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.machine_pushes_le line 163

    Source documentation

    The fixed offset is included in the finite program's push bound.

    theorem machine_pushes_le (offset : Nat) :
    Runtime.programPushBound (machine offset) ≤ max 2 offset := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound, OAI.MaxCutGames.Foundations.Complexity.MachineRegisterEmit.machine