OAI/Computability/UniqueGames/Machines/MachineRadixStepLemmas.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

One actual Horner step on unary field stacks. Multiplication and addition are executions of the same finite program. All three operands are preserved; only the output stack receives a new field and both work stacks return empty.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.Label line 18
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.Alphabet line 23
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.State line 24
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots line 30

    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 :=
…
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots_zero line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots_one line 34
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots_two line 35
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots_three line 36
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.multiplySlots_four line 37
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.statement line 41
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.program line 53
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.machine line 56
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.resultTapes line 67
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.resultTapes_output line 70
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.resultTapes_other line 74
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.steps line 78
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.radixStepTrace line 82

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

  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.radixStepInTime line 166
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.timePolynomial line 184
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.steps_le_timePolynomial line 187
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.programTrace line 198
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRadixStep.programInPolynomialTime line 210
  23. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Layout line 246
  24. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet line 247
  25. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State line 248
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.parity line 250
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.accumulator line 254
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.accumulator_ne line 256
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixLayout line 259
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots line 271
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots_base line 274
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots_acc line 276
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots_digit line 278
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots_out line 280
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots_counter line 282
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radixSlots_scratch line 284
  37. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Label line 287
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.entryLabel line 294
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.drainLoop line 298

    Source documentation

    Consume an isolated unary field, including its delimiter.

    def drainLoop (tape : K) (loopLabel : Λ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (State σ) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State

  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.statement line 307
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.program line 321
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.machine line 324
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.value line 335
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.stepCost line 339
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.prefixSteps line 342
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.stageTapes line 346
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.resultTapes line 349
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.drainTrace line 352
  49. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Clean line 376
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Clean.acc line 383
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.digitTrace line 391

    Source documentation

    One genuine radix execution followed by a unary drain of its old input accumulator. The new accumulator is left in the alternate physical tape.

    theorem digitTrace (slots : Layout width ↪ K) (labels : Label width → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Layout, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State

  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.prefixTrace line 463

    Source documentation

    Prefix induction follows the fixed finite sequence of digit labels.

    theorem prefixTrace (slots : Layout width ↪ K) (labels : Label width → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Layout, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State

  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.finishTrace line 486

    Source documentation

    Move the final accumulator to the external output, restoring its order and emptying accumulator/scratch. The old destination is retained as a suffix.

    theorem finishTrace (slots : Layout width ↪ K) (labels : Label width → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Layout, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State

  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.steps line 557
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.hornerTrace line 562

    Source documentation

    Complete actual Horner execution on preserved digit/base fields. Initial work tapes are empty; only the destination changes at the optional continuation.

    theorem hornerTrace (slots : Layout width ↪ K) (labels : Label width → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Layout, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State

  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.value_eq_foldl line 593
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.value_add_one_le line 606

    Source documentation

    A magnitude bound accommodates arbitrary digits, including fixed polynomial coefficients larger than the radix. No bounded-digit assumption is needed for execution correctness.

    theorem value_add_one_le (radix : Nat) (digits : Nat → Nat) (width magnitude : Nat)
    (radixBound : radix ≤ magnitude)
    (digitBound : ∀ i, i < width → digits i ≤ magnitude)
    (n : Nat) (hn : n ≤ width) : value radix digits n + 1 ≤ (magnitude + 1) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.value

  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.value_le line 625
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.perDigitBound line 633
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.stepCost_le line 637
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.prefixSteps_le line 646
  62. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.timePolynomial line 665
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.timePolynomial_eval line 672
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.steps_le_timePolynomial line 678
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.hornerInTime line 688
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.hornerInPolynomialTime line 704
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.operandLength line 725

    Source documentation

    The actual total bit length of the isolated radix and digit fields.

    def operandLength (radix : Nat) (digits : Nat → Nat) (width : Nat) : Nat :=
…
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.radix_le_operandLength line 729
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.digit_le_operandLength line 736
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.resultTapes_output line 747
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.resultTapes_other line 751
  72. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime line 757

    Source documentation

    Actual subroutine time bounded in the concrete lengths of its operand fields. The destination suffix and unrelated tapes are preserved without scans.

    def hornerInEncodedPolynomialTime (slots : Layout width ↪ K) (labels : Label width → Λ)
    (exit : Option Λ) (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Layout, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineHorner.State