OAI/Computability/MaxCut/Machines/MachineTemplateAddress.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

A fixed canonical-word template followed by actual radix-address execution. The program is determined by the fixed tokens and tape layout. Numeric field values enter only the tape invariants and execution theorem, never the labels.

  1. inductive OAI.MaxCutGames.Reduction.MachineTemplateAddress.Tape line 18
  2. abbrev OAI.MaxCutGames.Reduction.MachineTemplateAddress.State line 25
  3. abbrev OAI.MaxCutGames.Reduction.MachineTemplateAddress.Alphabet line 26
  4. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.hornerLayout line 30
  5. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.hornerSlots line 46
  6. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.chosen line 49
  7. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.mem_chosen line 52
  8. abbrev OAI.MaxCutGames.Reduction.MachineTemplateAddress.Label line 56
  9. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.emitLabel line 60
  10. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.reverseLabel line 62
  11. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.parseLabel line 63
  12. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.hornerLabel line 65
  13. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.cleanupLabel line 67
  14. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.parseDestination line 70
  15. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parseDestination_below line 74
  16. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.instruction line 78

    Source documentation

    Fixed finite instruction assembly, with arbitrary placement and continuation.

    def instruction (tokens : List (MachineFieldTemplate.Token q)) (slots : Tape q width ↪ K)
    (place : Label tokens.length width (chosen slots) → Λ) (exit : Option Λ) :
    Label tokens.length width (chosen slots) → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Tape, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Label, OAI.MaxCutGames.Reduction.MachineTemplateAddress.chosen, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Alphabet, OAI.MaxCutGames.Reduction.MachineTemplateAddress.State

  17. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.program line 101
  18. structure OAI.MaxCutGames.Reduction.MachineTemplateAddress.Clean line 107
  19. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.digits line 117
  20. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.forwardTapes line 119
  21. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.parsedTapes line 122
  22. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.resultTapes line 127
  23. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.afterHorner line 130
  24. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.phaseSteps line 135
  25. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.resultTapes_output line 142
  26. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.resultTapes_other line 146
  27. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.hornerValue_eq_radix line 152

    Source documentation

    The numeric recurrence used by the checked Horner machine is the direct canonical-address radix, in the original template-word order.

    theorem hornerValue_eq_radix (B : Nat) (values : List Nat) :
    MachineHorner.value B (digits values) values.length = CanonicalAddress.radix B values := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTemplateAddress.digits, OAI.MaxCutGames.Reduction.CanonicalAddress.radix

  28. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parsedTapes_other line 162
  29. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parsedTapes_source line 173
  30. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parsedTapes_digit line 182
  31. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parsedTapes_clean line 201
  32. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.cleanup_result line 222
  33. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parse_atStart line 262
  34. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parse_atLoop line 271
  35. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.parse_atDone line 281
  36. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.phaseTrace line 287
  37. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.programTrace line 381

    Source documentation

    The emitted finite program discharges every instruction-placement premise.

    theorem programTrace (tokens : List (MachineFieldTemplate.Token q)) (slots : Tape q width ↪ K)
    (exit : Option (Label tokens.length width (chosen slots)))
    (base : K → List Bool) (B : Nat) (values : List Nat) (hlen : values.length = width)
    (clean : Clean slots base) (baseField : base (slots .radix) = encodeWord B)
    (wordCorrect : MachineFieldTemplate.templateOutput tokens (fun j => base (slots (.field j))) =
      encodeWords values) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program tokens slots exit)))^[phaseSteps tokens slots base B values]
      (some ⟨some (emitLabel (MachineFieldTemplate.startAt tokens.length 0)),
        ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none), resultTapes slots base (CanonicalAddress.radix B values)⟩ :=
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Tape, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Label, OAI.MaxCutGames.Reduction.MachineTemplateAddress.chosen, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Clean, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateOutput, OAI.MaxCutGames.Reduction.MachineTemplateAddress.program, OAI.MaxCutGames.Reduction.MachineTemplateAddress.phaseSteps, OAI.MaxCutGames.Reduction.MachineTemplateAddress.emitLabel, OAI.MaxCutGames.Reduction.MachineFieldTemplate.startAt, OAI.MaxCutGames.Reduction.MachineTemplateAddress.resultTapes, OAI.MaxCutGames.Reduction.CanonicalAddress.radix

  38. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.phaseInTime line 395

    Source documentation

    Timed witness with the exact sum of the five concrete phase counts.

    def phaseInTime (tokens : List (MachineFieldTemplate.Token q)) (slots : Tape q width ↪ K)
    (place : Label tokens.length width (chosen slots) → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Tape, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Label, OAI.MaxCutGames.Reduction.MachineTemplateAddress.chosen, OAI.MaxCutGames.Reduction.MachineTemplateAddress.Alphabet, OAI.MaxCutGames.Reduction.MachineTemplateAddress.State

  39. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.copiedLength_le_inline_MachineTemplateAddress line 414
  40. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.lengthSum_le_inline_MachineTemplateAddress line 432
  41. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.timePolynomial line 446

    Source documentation

    A fixed polynomial in a magnitude bounding input fields, the serialized word list, the radix, and the digits. Width and token count are static.

    noncomputable def timePolynomial (tokenCount width : Nat) : Polynomial Nat :=
…
  42. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.timePolynomial_eval line 452
  43. theorem OAI.MaxCutGames.Reduction.MachineTemplateAddress.phaseSteps_le_timePolynomial line 458
  44. def OAI.MaxCutGames.Reduction.MachineTemplateAddress.phaseInPolynomialTime line 491
  45. abbrev OAI.MaxCutGames.Reduction.MachineAddressEdge.Tape line 525
  46. abbrev OAI.MaxCutGames.Reduction.MachineAddressEdge.State line 526
  47. abbrev OAI.MaxCutGames.Reduction.MachineAddressEdge.Alphabet line 527
  48. def OAI.MaxCutGames.Reduction.MachineAddressEdge.addressSlots line 531
  49. def OAI.MaxCutGames.Reduction.MachineAddressEdge.capacityTape line 535
  50. def OAI.MaxCutGames.Reduction.MachineAddressEdge.outputTape line 536
  51. def OAI.MaxCutGames.Reduction.MachineAddressEdge.workTape line 537
  52. def OAI.MaxCutGames.Reduction.MachineAddressEdge.tempTape line 538
  53. def OAI.MaxCutGames.Reduction.MachineAddressEdge.scratchTape line 539
  54. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.address_ne_output line 542
  55. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.capacity_ne_output line 546
  56. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.work_ne_output line 550
  57. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.temp_ne_work line 554
  58. abbrev OAI.MaxCutGames.Reduction.MachineAddressEdge.Label line 557
  59. def OAI.MaxCutGames.Reduction.MachineAddressEdge.leftLabel line 560
  60. def OAI.MaxCutGames.Reduction.MachineAddressEdge.rightLabel line 562
  61. def OAI.MaxCutGames.Reduction.MachineAddressEdge.plumbing line 564
  62. def OAI.MaxCutGames.Reduction.MachineAddressEdge.instruction line 567
  63. def OAI.MaxCutGames.Reduction.MachineAddressEdge.program line 593
  64. structure OAI.MaxCutGames.Reduction.MachineAddressEdge.Clean line 598
  65. def OAI.MaxCutGames.Reduction.MachineAddressEdge.appended line 602
  66. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.appended_address line 605
  67. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.appended_capacity line 611
  68. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.appended_output line 615
  69. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.appended_other line 620
  70. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.appended_append line 625
  71. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.Clean.appended line 630
  72. def OAI.MaxCutGames.Reduction.MachineAddressEdge.edgeBits line 644
  73. def OAI.MaxCutGames.Reduction.MachineAddressEdge.phaseSteps line 649
  74. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.addressResult_eq line 657
  75. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.transfer_result line 661
  76. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.literalStep line 692
  77. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.phaseTrace line 703

    Source documentation

    Both actual address computations, a preserved-capacity copy, unary addition, cleanup, two reverse transfers, and the fixed permutation instruction.

    theorem phaseTrace (base : K → List Bool) (B C : Nat)
    (leftValues rightValues : List Nat)
    (leftLength : leftValues.length = width) (rightLength : rightValues.length = width)
    (clean : Clean slots base)
    (baseField : base (addressSlots slots .radix) = encodeWord B)
    (capacityField : base (capacityTape slots) = encodeWord C)
    (leftCorrect : MachineFieldTemplate.templateOutput left
      (fun j => base (addressSlots slots (.field j))) = encodeWords leftValues)
    (rightCorrect : MachineFieldTemplate.templateOutput right
      (fun j => base (addressSlots slots (.field j))) = encodeWords rightValues)
    (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step P))^[phaseSteps left right slots base B C leftValues rightValues]
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressEdge.Clean, OAI.MaxCutGames.Reduction.MachineAddressEdge.addressSlots, OAI.MaxCutGames.Reduction.MachineAddressEdge.capacityTape, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateOutput, OAI.MaxCutGames.Reduction.MachineAddressEdge.phaseSteps

  78. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.programTrace line 836
  79. def OAI.MaxCutGames.Reduction.MachineAddressEdge.phaseInTime line 859
  80. def OAI.MaxCutGames.Reduction.MachineAddressEdge.timePolynomial line 890

    Source documentation

    A fixed polynomial in a common magnitude bound for the input fields, serialized words, radix, capacity, and digits.

    noncomputable def timePolynomial (leftCount rightCount width : Nat) : Polynomial Nat :=
…
  81. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.timePolynomial_eval line 896
  82. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.radix_le_magnitude line 904
  83. theorem OAI.MaxCutGames.Reduction.MachineAddressEdge.phaseSteps_le_timePolynomial line 913