OAI/Computability/MaxCut/Machines/MachineUnaryMultiply.lean

GitHub source file

72 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.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label line 18
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList line 22
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_getElem?_ctorIdx_eq line 25
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_nodup line 29
  5. instance OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.(instance at line 31) line 31
  6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet line 35
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.State line 36
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.transition line 38
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.payload line 39
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.emitterLabel line 41
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.statement line 48

    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.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.State

  12. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.program line 65
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.machine line 68
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes line 79
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_output line 82
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other line 86
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.bodySteps line 90
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.steps line 91
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.output_encodeWord_inline_MachineUnaryMultiply line 93
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.prepend_payload_inline_MachineUnaryMultiply line 103
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.loopBase line 108

    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.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.bodyTrace_inline_MachineUnaryMultiply line 111
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.totalSteps_eq_inline_MachineUnaryMultiply line 169
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyTrace line 175

    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.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.State

  25. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime line 251

    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.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Label, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.State

  26. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.timePolynomial line 267
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.steps_le_timePolynomial line 270
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyFrame line 282

    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.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other

  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.programTrace line 288

    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.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.program, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.steps

  30. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.programInPolynomialTime line 301

    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.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryMultiply.program

  31. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.Alphabet line 328
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.finish line 330
  33. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.loop line 335

    Source documentation

    A fixed finite statement; arithmetic is performed by the physical unary tapes.

    def loop (source destination : K) (loopLabel : Λ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

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

  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.loopPushBound line 345
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes line 350

    Source documentation

    A caller's tape frame with the two unary prefixes and their unread suffixes.

    def unaryTapes (source destination : K) (base : K → List Bool) (a b : Nat)
    (sourceSuffix destinationSuffix : List Bool) : K → List Bool :=
…
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_source line 355
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_destination line 361
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_other line 367
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.update_source_inline_MachineUnaryAddAt line 374
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.update_destination_inline_MachineUnaryAddAt line 387
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_true line 397
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_false line 407

    Source documentation

    The zero branch restores the delimiter, clears the register, and exits.

    theorem stepAux_false (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ) (base : K → List Bool)
    (input output : List Bool) (ambient : σ) (register : Option Bool) :
    TM2.stepAux (loop source destination loopLabel exit) (ambient, register)
      (tapesAt source destination base (false :: input) output) =
      ⟨exit, (ambient, none), tapesAt source destination base (false :: input) output⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.loop

  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_succ line 415
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_zero line 426
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.step_succ line 438
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.step_zero line 452
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.addTrace line 467

    Source documentation

    Exactly a positive-bit transitions followed by the delimiter transition.

    theorem addTrace (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.addFromTapes line 492

    Source documentation

    The same actual execution from a caller's supplied tape configuration.

    theorem addFromTapes (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  49. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.addInTime line 513

    Source documentation

    A composable time witness whose stored transition count is exactly a + 1.

    def addInTime (source destination : K) (distinct : source ≠ destination)
    (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAddAt.addInTime_steps line 531
  51. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.Label line 555
  52. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.Alphabet line 560
  53. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.State line 561
  54. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots line 567

    Source documentation

    Multiplication uses radix, accumulator, output, counter, and scratch, skipping the independently preserved digit stack.

    def multiplySlots (slots : Fin 6 ↪ K) : Fin 5 ↪ K :=
…
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_zero line 570
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_one line 571
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_two line 572
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_three line 573
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_four line 574
  60. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.statement line 578
  61. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.program line 590
  62. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.machine line 593
  63. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.resultTapes line 604
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.resultTapes_output line 607
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.resultTapes_other line 611
  66. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.steps line 615
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.radixStepTrace line 619

    Source documentation

    A concrete Horner execution. Caller hypotheses identify the finite code, not an assumed execution or arithmetic oracle.

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

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.State

  68. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.radixStepInTime line 703
  69. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.timePolynomial line 721
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.steps_le_timePolynomial line 724
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.programTrace line 735
  72. def OAI.MaxCutGames.Foundations.Complexity.MachineRadixStep.programInPolynomialTime line 747