OAI/Computability/UniqueGames/Machines/MachineRegularDummyRow.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Actual inherited-row emission for a dummy vertex

The fixed program preserves the physical unary vertex index on tape zero, computes its inherited reverse index on tape one, invokes the actual one-port dummy-row emitter, and drains the computed index and fixed true relation. Tape four accumulates output. Tapes one, two, three, and five are empty at both boundaries. The degree is fixed program data, not an input-dependent control parameter.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Tape line 23
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Alphabet line 24
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.State line 25
  4. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Label line 27
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.reverseIndex line 33
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.emittedBits line 35
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.instruction line 39

    Source documentation

    The row subprogram is a static label placement of the checked emitter.

    def instruction {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt Alphabet Λ (State σ)
  | .affine .seed => MachineUnaryAffineAt.seed 1 q (labels (.affine .scan))
  | .affine .scan => MachineUnaryAffineAt.scan 0 3 1 (q + 1)
      (labels (.affine .scan)) (labels (.affine .restore))
  | .affine .restore => Reduction.MachineTransfer.loopAt 3 0 id false
      (labels (.affine .restore)) (some (labels (.row (MachineDummyRows.start 1))))
  | .row stage => MachineCloudPadding.Placement.statement (id : Tape → Tape)
      (fun l => labels (.row l)) (some (labels .reverse))
      (MachineDummyRows.program 1 stage)
  | .reverse => MachineDrain.drain 1 (labels .reverse) (some (labels .relation))
  | .relation => MachineDrain.drain 2 (labels .relation) exit

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.seed, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scan, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drain

  8. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Input line 52
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.memory line 59
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.memory_input line 62
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.join_trace line 65
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.affine_frame line 69
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.cleanup_frame line 77
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.rowTraceAt line 87

    Source documentation

    The existing one-port emitter executes under the caller's actual labels.

    theorem rowTraceAt {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (x e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[MachineDummyRows.steps x e output 1 + 1]
      (some ⟨some (labels (.row (MachineDummyRows.start 1))), (ambient, register),
        MachineDummyRows.initialTapes x e output⟩) =
      some ⟨some (labels .reverse), (ambient, none),
        MachineDummyRows.fieldTapes x (e + 1) (output ++ MachineDummyRows.rowBits x e)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowBits

  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.cleanupTraceAt line 110

    Source documentation

    Both cleanup loops pop their entire physical fields.

    theorem cleanupTraceAt {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (x e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[
        ((encodeWord e).length + 1) + (MachineDummyRows.trueBits.length + 1)]
      (some ⟨some (labels .reverse), (ambient, register),
        MachineDummyRows.fieldTapes x e output⟩) =
      some ⟨exit, (ambient, none),
        Function.update (Function.update (MachineDummyRows.fieldTapes x e output) 1 []) 2 []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.fieldTapes

  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.steps line 136

    Source documentation

    Sum of the actual arithmetic, row-emission, and cleanup transition counts.

    def steps (q x : Nat) (output : List Bool) : Nat :=
…
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.timeBound line 142

    Source documentation

    For each fixed degree, the exact cost is linear in index and prior output.

    def timeBound (q x outputLength : Nat) : Nat :=
…
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.steps_eq line 145
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.traceAt line 152

    Source documentation

    Exact physical execution; only the accumulated output changes at the boundary.

    theorem traceAt {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (x : Nat) (base : Tape → List Bool) (input : Input x base)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps q x (base 4)]
      (some ⟨some (labels (.affine .seed)), (ambient, register), base⟩) =
      some ⟨exit, (ambient, none), Function.update base 4 (base 4 ++ emittedBits q x)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.Input, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.emittedBits

  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.machine line 180

    Source documentation

    A canonical finite machine over six Boolean stacks.

    def machine (q : Nat) : FinTM2 where
…
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularDummyRow.machineInTime line 191