OAI/Computability/MaxCut/Machines/Machine.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Actual complete-stack cleanup, with an arbitrary continuation. Each symbol costs one transition and the empty-stack branch costs one final transition.

  1. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceMachine.Alphabet line 14
  2. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldLoop line 17

    Source documentation

    Read one unary field, stopping at its zero delimiter.

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

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceMachine.Alphabet

  3. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStart line 26

    Source documentation

    Seed the destination delimiter before scanning the unary payload.

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

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceMachine.Alphabet

  4. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldTapes line 30
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldTapes_source line 34
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldTapes_destination line 39
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldTapes_self line 44
  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldTapes_other line 48
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.update_field_source_inline_SourceMachine line 54
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.update_field_destination_inline_SourceMachine line 65
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStep_delimiter line 71
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStep_true line 85
  13. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldLoopTrace line 100

    Source documentation

    Exactly one transition per unary bit, including its terminating delimiter.

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

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceMachine.Alphabet

  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStartStep line 132
  15. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldInTime line 146
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.afterField line 177

    Source documentation

    Stack state after one completed field, retaining an arbitrary old destination.

    def afterField (source destination : K) (base : K → List Bool)
    (n : Nat) (suffix : List Bool) : K → List Bool :=
…
  17. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldNext line 181
  18. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourTapes line 188
  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourTapes_source line 195
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourTapes_other line 201
  21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourField_time_eq_length line 207
  22. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourFieldsInTime line 214

    Source documentation

    Four fields are separated by actual finite-stack transitions. The stated bound is exactly their serialized length plus four delimiter-seeding steps.

    def fourFieldsInTime (source : K) (destination : Fin 4 → K)
    (hsep : ∀ j, source ≠ destination j)
    (start loopLabel : Fin 4 → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceMachine.Alphabet

  23. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldDestination line 258
  24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourTapes_concrete line 260
  25. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.groupingProgram line 272
  26. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.groupingMachine line 281

    Source documentation

    One concrete finite machine: five Boolean stacks, eight labels, and three internal states. Four destination stacks hold the four separated fields.

    def groupingMachine : FinTM2 where
…
  27. def OAI.MaxCutGames.Foundations.Hastad.SourceMachine.groupingMachineInTime line 294

    Source documentation

    The concrete machine's verified trace includes arbitrary unread input and arbitrary prior destination contents. No assumed algorithm remains here.

    def groupingMachineInTime (base : Fin 5 → List Bool) (a b c d : Nat) (suffix : List Bool)
    (hinput : base 0 = encodeWords [a, b, c, d] ++ suffix) (register : Option Bool) :
    StateTransition.EvalsToInTime groupingMachine.step
      ⟨some (0, false), ((), register), base⟩
      (some ⟨none, ((), none), fourTapes (0 : Fin 5) fieldDestination base a b c d suffix⟩)
      (a + b + c + d + 8) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fourTapes, OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldDestination

  28. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDrain.Alphabet line 320
  29. def OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drain line 322
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drainTrace line 329
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drainInTime line 350
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.Label line 379
  33. instance OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.labelFintype line 383
  34. instance OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.labelDecidableEq line 391
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.entry line 402
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.instruction line 409
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.resultOf line 420
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.steps line 424
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.trace line 432

    Source documentation

    This generic composition lemma retains the local execution obligations. Concrete callers discharge them with the rotor, comparison and row programs.

    theorem trace (program : Λ → TM2.Stmt Γ Λ σ)
    (invariant : Data → Prop) (state : Data → σ) (tapes : Data → ∀ k, List (Γ k))
    (commands : List Command)
    (localInvariant : ∀ command ∈ commands, ∀ data, invariant data →
      invariant (result command data))
    (localTrace : ∀ command ∈ commands, ∀ (labels : LocalLabel command → Λ) (exit : Option Λ),
      (∀ l, program (labels l) = localInstruction command labels exit l) →
      ∀ data, invariant data →
      (advance (TM2.step program))^[cost command data]
        (some ⟨some (labels (main command)), state data, tapes data⟩) =
      some ⟨exit, state (result command data), tapes (result command data)⟩)
    (labels : Label LocalLabel commands → Λ) (exit : Option Λ)
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFiniteSequence.Label

  40. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Alphabet line 487
  41. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Tapes line 488
  42. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.LocalLabel line 489
  43. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Label line 490
  44. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Data line 491
  45. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.entry line 493
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.localInstruction line 496
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.instruction line 500
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.result line 505
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.cost line 508
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalTapes line 510
  51. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalRegister line 514
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalRegister_none line 519
  53. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.steps line 522
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.sequence_result line 527
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.sequence_steps line 537
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalTapes_apply line 545

    Source documentation

    Selected tapes are empty; every other tape word is preserved.

    theorem finalTapes_apply (chosen : List K) (base : Tapes K) (k : K) :
    finalTapes chosen base k = if k ∈ chosen then [] else base k := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Tapes, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalTapes

  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalTapes_mem line 556
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalTapes_not_mem line 559
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.lengthSum line 562
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.lengthSum_mono line 566
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.steps_le line 576

    Source documentation

    This upper bound remains valid when the cleanup list repeats tapes.

    theorem steps_le (chosen : List K) (base : Tapes K) :
    steps chosen base ≤ lengthSum chosen base + chosen.length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Tapes, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.steps, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.lengthSum

  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.steps_le_uniform line 592
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.trace line 608

    Source documentation

    Exact execution of all concrete drains in the supplied ambient program.

    theorem trace (chosen : List K) (labels : Label chosen → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Label, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Alphabet

  64. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.execution line 629
  65. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.workTapes line 642

    Source documentation

    An executable complete cleanup list from an explicit finite enumeration.

    def workTapes {N : Nat} (enumeration : Fin N ≃ K) (output : K) : List K :=
…
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.mem_workTapes line 645
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.workTapes_length_le line 652
  68. def OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.haltTapes line 658

    Source documentation

    The tape component of the actual halted configuration: only output remains.

    def haltTapes (output : K) (word : List Bool) : Tapes K :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Tapes

  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.finalTapes_workTapes line 661
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.cleanupTrace line 673

    Source documentation

    With a clean register, complete work-tape cleanup reaches the standard halted shape, preserving the output word and the ambient state exactly.

    theorem cleanupTrace {N : Nat} (enumeration : Fin N ≃ K) (output : K)
    (labels : Label (workTapes enumeration output) → Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Label, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.workTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.Alphabet

  71. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Label line 693
  72. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Tapes line 694
  73. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.entry line 696
  74. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.statement line 701

    Source documentation

    All instructions act on physical stacks. The final load only resets the finite internal register; no input-dependent integer is stored in it.

    def statement (clearKeys : List K) (accumulator output : K) (canonical : σ)
    (labels : Label clearKeys → Λ) (exit : Option Λ) :
    Label clearKeys → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool)
  | .inl label => MachineDrainMany.instruction clearKeys (fun l => labels (.inl l))
      (some (labels (.inr false))) label
  | .inr false => Reduction.MachineTransfer.loopAt accumulator output id false
      (labels (.inr false)) (some (labels (.inr true)))
  | .inr true => .load (fun _ => (canonical, none)) (Reduction.MachineTransfer.exitAt output exit)

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Label, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Reduction.MachineTransfer.exitAt

  75. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.canonicalTapes line 710
  76. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishCost line 713
  77. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.cleared_frame line 716
  78. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.reversed_tapes line 720
  79. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishInTime line 739

    Source documentation

    Exact execution, including the real drain loops, reversal, and reset. The only program hypotheses identify the caller's actual placed statements.

    def finishInTime (clearKeys : List K) (accumulator output : K)
    (distinct : accumulator ≠ output)
    (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
    (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
    (canonical : σ) (labels : Label clearKeys → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (atLabels : ∀ label,
      program (labels label) = statement clearKeys accumulator output canonical labels exit label)
    (base : Tapes K) (outputEmpty : base output = []) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨entry clearKeys labels, (ambient, register), base⟩
      (some ⟨exit, (canonical, none), canonicalTapes output (base accumulator).reverse⟩)
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Label, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.statement, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Tapes, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.entry, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.canonicalTapes

  80. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishCost_le_list line 799
  81. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.totalLength line 809
  82. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.totalLength_erase line 811
  83. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.drain_conservation line 827

    Source documentation

    Each physical pop removes one stored symbol; repeated clear keys add only the extra empty-tape loop test after their first occurrence.

    theorem drain_conservation (clearKeys : List K) (base : Tapes K) :
    MachineDrainMany.steps clearKeys base +
      totalLength (MachineDrainMany.finalTapes clearKeys base) =
        totalLength base + clearKeys.length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Tapes, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.totalLength

  84. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.cleared_totalLength line 839
  85. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishCost_eq_totalLength line 858

    Source documentation

    Exact finalization cost from the complete initial stack contents.

    theorem finishCost_eq_totalLength (clearKeys : List K) (accumulator output : K)
    (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
    (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
    (base : Tapes K) (outputEmpty : base output = []) :
    finishCost clearKeys accumulator base = totalLength base + clearKeys.length + 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.Tapes, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishCost, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.totalLength