OAI/Computability/UniqueGames/Machines/MachineUnaryMultiply.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

An actual five-stack unary multiplication subroutine. Both isolated input fields are preserved. The product field prefixes the previous output stack; the counter and scratch return empty and all other stacks are framed.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label line 19
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label.enumList line 23
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_getElem?_ctorIdx_eq line 26
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_nodup line 30
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.(instance at line 32) line 32
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Alphabet line 38
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.State line 39
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.transition line 41
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.payload line 42
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.emitterLabel line 44
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.statement line 51

    Source documentation

    Slots 0 and 1 contain the operands, 2 the output, 3 the counter, and 4 the reusable empty scratch. The code is independent of operand values.

    def statement (slots : Fin 5 ↪ K) (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.State

  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.program line 68
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.machine line 71
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.resultTapes line 82
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.resultTapes_output line 85
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other line 89
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.bodySteps line 93
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.steps line 94
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.output_encodeWord line 96
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.prepend_payload line 106
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.loopBase line 111

    Source documentation

    The accumulator is indexed by the remaining number of outer iterations.

    def loopBase (slots : Fin 5 ↪ K) (base : K → List Bool) (a b r : ℕ) : K → List Bool :=
…
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.bodyTrace line 114
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.totalSteps_eq line 172
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.multiplyTrace line 178

    Source documentation

    Exact execution in any ambient program containing the nine declared statements. The body traces are derived from the actual copy transducer.

    theorem multiplyTrace (slots : Fin 5 ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.State

  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime line 254

    Source documentation

    A time witness with the exact transition count, including restoration of the operand delimiter and removal of the counter delimiter.

    def multiplyInTime (slots : Fin 5 ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.State

  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.timePolynomial line 270
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.steps_le_timePolynomial line 273
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.multiplyFrame line 285

    Source documentation

    Both input stacks, both restored work stacks, and every unrelated stack are preserved because only the output stack differs at the actual endpoint.

    theorem multiplyFrame (slots : Fin 5 ↪ K) (base : K → List Bool) (a b : ℕ)
    (k : K) (hk : k ≠ slots 2) :
    resultTapes slots base (a * b) k = base k := resultTapes_other slots base _ k hk

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.resultTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other

  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.programTrace line 291

    Source documentation

    The fixed finite program realizes the trace without any caller-code or abstract-computability hypothesis.

    theorem programTrace (slots : Fin 5 ↪ K) (base : K → List Bool) (a b : ℕ)
    (operandA : base (slots 0) = encodeWord a)
    (operandB : base (slots 1) = encodeWord b)
    (counterEmpty : base (slots 3) = []) (scratchEmpty : base (slots 4) = [])
    (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program (σ := σ) slots)))^[steps a b]
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.steps

  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.programInPolynomialTime line 304

    Source documentation

    The fixed program's genuine execution fits a quadratic polynomial in the combined lengths of its two encoded operand fields.

    def programInPolynomialTime (slots : Fin 5 ↪ K) (base : K → List Bool) (a b : ℕ)
    (operandA : base (slots 0) = encodeWord a)
    (operandB : base (slots 1) = encodeWord b)
    (counterEmpty : base (slots 3) = []) (scratchEmpty : base (slots 4) = [])
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program (σ := σ) slots))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryMultiply.program