OAI/Computability/UniqueGames/Machines/PoweringMachineFinish.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Physical output headers followed by complete work-tape cleanup

The finite program first copies the dart-count word onto the existing row output, then copies the vertex-count word, and finally drains every tape except the output. Both unary header values are read from physical tapes; they do not parameterize the program. Header sources and their unread suffixes are restored by the two copies before cleanup. The final configuration contains the full encoded header and rows on the output tape and empty words on every other tape.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Alphabet line 25
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Label line 27
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.copyInstruction line 31
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.instruction line 39

    Source documentation

    The labels contain two fixed affine copies and one fixed list of drains.

    def instruction (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (labels : Label enumeration output → Λ) :
    Label enumeration output → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Alphabet

  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.program line 52

    Source documentation

    Actual finite control, independent of both runtime header values.

    def program (enumeration : Fin N ≃ K) (headerV headerD output scratch : K) :
    Label enumeration output →
      TM2.Stmt (Alphabet (K := K)) (Label enumeration output) (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Alphabet

  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.afterD line 57
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.afterHeaders line 60
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.afterHeaders_output line 63
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.afterHeaders_other line 67
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.copySteps line 71
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.copySteps_eq line 73
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps line 78

    Source documentation

    Exact cleanup cost is computed on the actual post-copy tape contents.

    def steps (enumeration : Fin N ≃ K) (output : K) (base : K → List Bool) (n m : Nat) : Nat :=
…
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.budget line 82
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.trace_trans line 86
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.traceAt line 92

    Source documentation

    Exact execution inside any ambient program containing these instructions. The only data premises describe physical header words and an empty scratch tape.

    theorem traceAt (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (hvs : headerV ≠ scratch) (hvo : headerV ≠ output)
    (hds : headerD ≠ scratch) (hdo : headerD ≠ output) (hso : scratch ≠ output)
    (labels : Label enumeration output → Λ)
    (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.Alphabet

  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.trace line 142

    Source documentation

    The standalone program satisfies the trace with no code or execution premise.

    theorem trace (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (hvs : headerV ≠ scratch) (hvo : headerV ≠ output)
    (hds : headerD ≠ scratch) (hdo : headerD ≠ output) (hso : scratch ≠ output)
    (base : K → List Bool) (n m : Nat) (suffixV suffixD : List Bool)
    (wordV : base headerV = encodeWord n ++ suffixV)
    (wordD : base headerD = encodeWord m ++ suffixD)
    (scratchEmpty : base scratch = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program enumeration headerV headerD output scratch)))^[
      steps enumeration output base n m]
      (some ⟨some (.inl .seed), (ambient, register), base⟩) =
      some ⟨none, (ambient, none),
        MachineDrainMany.haltTapes output (encodeWords [n, m] ++ base output)⟩ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.program, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.haltTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps_le_budget line 158
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.afterHeaders_length_le line 164
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps_le_uniform line 178

    Source documentation

    A uniform pre-cleanup stack bound gives a linear finishing budget.

    theorem steps_le_uniform (enumeration : Fin N ≃ K) (output : K)
    (base : K → List Bool) (n m bound : Nat)
    (bounded : ∀ k, (base k).length ≤ bound) :
    steps enumeration output base n m ≤ 2 * (n + m) + 6 + N * (bound + n + m + 3) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps

  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.execution line 193

    Source documentation

    A bounded execution witness, obtained from the physical trace above.

    def execution (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (hvs : headerV ≠ scratch) (hvo : headerV ≠ output)
    (hds : headerD ≠ scratch) (hdo : headerD ≠ output) (hso : scratch ≠ output)
    (base : K → List Bool) (n m : Nat) (suffixV suffixD : List Bool)
    (wordV : base headerV = encodeWord n ++ suffixV)
    (wordD : base headerD = encodeWord m ++ suffixD)
    (scratchEmpty : base scratch = []) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program enumeration headerV headerD output scratch))
      ⟨some (.inl .seed), (ambient, register), base⟩
      (some ⟨none, (ambient, none),
        MachineDrainMany.haltTapes output (encodeWords [n, m] ++ base output)⟩)
      (budget enumeration output base n m) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.haltTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.budget