OAI/Computability/MaxCut/Machines/MachineHorner.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Fixed-width Horner traversal by actual radix steps. Two accumulators alternate: a radix step writes into the empty alternate, then the previous accumulator is consumed. The base, digit fields, and arbitrary external tapes are preserved.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineHorner.Layout line 18
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineHorner.Alphabet line 19
  3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineHorner.State line 20
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.parity line 22
  5. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.accumulator line 26
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.accumulator_ne line 28
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixLayout line 31
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots line 43
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots_base line 46
  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots_acc line 48
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots_digit line 50
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots_out line 52
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots_counter line 54
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radixSlots_scratch line 56
  15. inductive OAI.MaxCutGames.Foundations.Complexity.MachineHorner.Label line 59
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.entryLabel line 66
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.drainLoop line 70

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

  18. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.statement line 79
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.program line 93
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.machine line 96
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.value line 107
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.stepCost line 111
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.prefixSteps line 114
  24. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.stageTapes line 118
  25. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.resultTapes line 121
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.drainTrace line 124
  27. structure OAI.MaxCutGames.Foundations.Complexity.MachineHorner.Clean line 148
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.Clean.acc line 155
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.digitTrace line 163

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

  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.prefixTrace line 235

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

  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.finishTrace line 258

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

  32. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.steps line 329
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.hornerTrace line 334

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

  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.value_eq_foldl line 365
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.value_add_one_le line 378

    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.MaxCutGames.Foundations.Complexity.MachineHorner.value

  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.value_le line 397
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.perDigitBound line 405
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.stepCost_le line 409
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.prefixSteps_le line 418
  40. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.timePolynomial line 437
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.timePolynomial_eval line 444
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.steps_le_timePolynomial line 450
  43. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.hornerInTime line 460
  44. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.hornerInPolynomialTime line 476
  45. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.operandLength line 497

    Source documentation

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

    def operandLength (radix : Nat) (digits : Nat → Nat) (width : Nat) : Nat :=
…
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.radix_le_operandLength line 501
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.digit_le_operandLength line 508
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.resultTapes_output line 519
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineHorner.resultTapes_other line 523
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime line 529

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

  51. abbrev OAI.MaxCutGames.Explicit.MachineProductField.Layout line 563

    Source documentation

    Gather's table/query/scan/scratch and coordinate tapes; then radix, two Horner accumulators, counter, scratch, isolated field output, global output.

    abbrev Layout (width : Nat) := MachineProductGather.Tape width ⊕ Fin 7

    Mentions: OAI.MaxCutGames.Explicit.MachineProductGather.Tape

  52. def OAI.MaxCutGames.Explicit.MachineProductField.gatherSlots line 565
  53. def OAI.MaxCutGames.Explicit.MachineProductField.hornerRole line 568
  54. theorem OAI.MaxCutGames.Explicit.MachineProductField.hornerRole_injective line 577
  55. def OAI.MaxCutGames.Explicit.MachineProductField.hornerSlots line 589
  56. def OAI.MaxCutGames.Explicit.MachineProductField.clearTapes line 592
  57. abbrev OAI.MaxCutGames.Explicit.MachineProductField.Label line 596
  58. def OAI.MaxCutGames.Explicit.MachineProductField.entry line 600
  59. def OAI.MaxCutGames.Explicit.MachineProductField.instruction line 603
  60. structure OAI.MaxCutGames.Explicit.MachineProductField.Ready line 618

    Source documentation

    Conditions on real input/work stacks; arbitrary output suffixes remain permitted. The two query/scan tapes are empty at a row boundary.

    structure Ready (slots : Layout width ↪ K) (base : K → List Bool) : Prop where
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductField.Layout

  61. def OAI.MaxCutGames.Explicit.MachineProductField.gathered line 629
  62. def OAI.MaxCutGames.Explicit.MachineProductField.evaluated line 634
  63. def OAI.MaxCutGames.Explicit.MachineProductField.emitted line 639
  64. def OAI.MaxCutGames.Explicit.MachineProductField.finalTapes line 645
  65. def OAI.MaxCutGames.Explicit.MachineProductField.steps line 650
  66. theorem OAI.MaxCutGames.Explicit.MachineProductField.gathered_extra line 659
  67. theorem OAI.MaxCutGames.Explicit.MachineProductField.fieldTrace line 671

    Source documentation

    Actual execution of the complete gather/Horner/emit/cleanup phase. The field equality connects only mathematical tape contents; all transition work is proved from the concrete instructions.

    theorem fieldTrace (slots : Layout width ↪ K) (values : List Nat) (coefficient : Nat)
    (indices offsets fields : Fin width → Nat)
    (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
    (labels : Label slots → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ l, program (labels l) = instruction slots coefficient offsets labels exit l)
    (base : K → List Bool) (suffixes : Fin width → List Bool) (ready : Ready slots base)
    (tableWord : base (slots (.inl (.inl 0))) = encodeWords values)
    (sourceWords : ∀ i, base (slots (.inl (.inr (.inl i)))) =
      encodeWord (indices i) ++ suffixes i)
    (radix : Nat) (digits : Nat → Nat)
    (radixWord : base (slots (.inr 0)) = encodeWord radix)
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductField.Layout, OAI.MaxCutGames.Explicit.MachineProductField.Label, OAI.MaxCutGames.Explicit.MachineProductField.instruction, OAI.MaxCutGames.Explicit.MachineProductField.Ready