OAI/Computability/MaxCut/Machines/Runtime.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Stack-length bounds derived from actual machine transitions. A finite program has a maximum number of pushes in any one statement. Iterating its transitions therefore bounds output length by input length plus that constant times elapsed steps. This proves a consequence of a runtime certificate, not its converse.

  1. def OAI.MaxCutGames.Foundations.Complexity.Runtime.statementPushBound line 15
  2. def OAI.MaxCutGames.Foundations.Complexity.Runtime.maxLabelPushes line 25
  3. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.maxLabelPushes_ge line 30
  4. def OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound line 44

    Source documentation

    The finite maximum is a proof-bound constant, not an operation of the machine being analyzed.

    noncomputable def programPushBound (tm : Turing.FinTM2) : Nat :=
…
  5. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.statement_le_programPushBound line 47
  6. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.stepAuxStackLength line 52
  7. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.iterateSizeBound_inline_Runtime line 95
  8. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.executionSizeBound line 108

    Source documentation

    Resource growth along the actual iterated transition witness.

    theorem executionSizeBound {σ : Type} (step : σ → Option σ) (size : σ → Nat) (C : Nat)
    (oneStep : ∀ a b, step a = some b → size b ≤ size a + C)
    {start finish : σ} {budget : Nat}
    (execution : StateTransition.EvalsToInTime step start (some finish) budget) :
    size finish ≤ size start + budget * C := by
…
  9. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.stepStackLength line 131
  10. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.initialStackLength line 144
  11. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.haltedOutputLength line 151
  12. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.outputLength_le line 155
  13. theorem OAI.MaxCutGames.Foundations.Complexity.Runtime.encodedOutputLength line 169

    Source documentation

    Polynomial-time computation implies a polynomial bound on serialized output length. This direction is used for intermediate data in composition.

    theorem encodedOutputLength {α β αΓ βΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
    (certificate : Turing.TM2ComputableInPolyTime ea eb f) (a : α) :
    (eb (f a)).length ≤
      (Polynomial.X + Polynomial.C (programPushBound certificate.tm) * certificate.time).eval
        (ea a).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound

  14. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.Alphabet line 191
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.tapes line 195
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.tapes_inl line 200
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.tapes_inr line 203
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.label line 206
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.configuration line 210
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.statement line 217
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.tapes_update line 234
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 249

    Source documentation

    One finite statement executes identically on the original stacks and state. The entire statement is simulated in exactly one TM2 transition.

    theorem stepAux_simulation (haltTarget : Option (Λ ⊕ Λextra))
    (extraState : τ) (extraTapes : ∀ e, List (Δ e))
    (q : Stmt Γ Λ σ) (state : σ) (source : ∀ k, List (Γ k)) :
    stepAux (statement haltTarget q) (state, extraState) (tapes source extraTapes) =
      configuration haltTarget extraState extraTapes (stepAux q state source) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.statement, OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.tapes, OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.configuration

  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 275
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 283
  25. def OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.program line 291
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.step_running line 297
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.step_simulation line 310
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance line 338
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance_none line 341
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance_some line 344
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance_iterate_none line 347
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 353
  33. def OAI.MaxCutGames.Foundations.Complexity.MachineComposition.liftExecutionInTime line 377
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 391
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineComposition.embeddedExecution line 400

    Source documentation

    The checked disjoint-stack embedding transports a complete successful run with no additional transitions, including its final jump to a bridge label.

    def embeddedExecution {K E Λ Λextra σ τ : Type} {Γ : K → Type} {Δ : E → Type}
    [DecidableEq K] [DecidableEq E]
    (haltTarget : Option (Λ ⊕ Λextra)) (extraState : τ)
    (extraTapes : ∀ e, List (Δ e))
    (source : Λ → Turing.TM2.Stmt Γ Λ σ)
    (extra : Λextra → Turing.TM2.Stmt (MachineEmbedding.Alphabet Γ Δ)
      (Λ ⊕ Λextra) (σ × τ))
    {start finish : Turing.TM2.Cfg Γ Λ σ} {budget : Nat}
    (execution : StateTransition.EvalsToInTime (Turing.TM2.step source)
      start (some finish) budget) :
    StateTransition.EvalsToInTime (Turing.TM2.step (MachineEmbedding.program haltTarget source extra))
      (MachineEmbedding.configuration haltTarget extraState extraTapes start)
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.program, OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.configuration

  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 418
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineComposition.compositionPolynomial line 428

    Source documentation

    Two reversal transfers each consume intermediateLength + 1 transitions.

    noncomputable def compositionPolynomial (first second intermediate : Polynomial Nat) : Polynomial Nat :=
…
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineComposition.compositionBudget_le line 431
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineComposition.fourPhaseExecution line 442
  40. abbrev OAI.MaxCutGames.Reduction.MachineTransfer.alphabet line 488
  41. def OAI.MaxCutGames.Reduction.MachineTransfer.loop line 494
  42. def OAI.MaxCutGames.Reduction.MachineTransfer.machine line 501
  43. def OAI.MaxCutGames.Reduction.MachineTransfer.tapeStacks line 513
  44. def OAI.MaxCutGames.Reduction.MachineTransfer.running line 518
  45. def OAI.MaxCutGames.Reduction.MachineTransfer.halted line 522
  46. theorem OAI.MaxCutGames.Reduction.MachineTransfer.update_input_inline_MachineTransfer line 526
  47. theorem OAI.MaxCutGames.Reduction.MachineTransfer.update_output_inline_MachineTransfer line 532
  48. theorem OAI.MaxCutGames.Reduction.MachineTransfer.step_empty line 537
  49. theorem OAI.MaxCutGames.Reduction.MachineTransfer.step_cons line 545
  50. def OAI.MaxCutGames.Reduction.MachineTransfer.next line 554
  51. theorem OAI.MaxCutGames.Reduction.MachineTransfer.transfer_steps line 558

    Source documentation

    Exact actual-machine trace, for any accumulator and internal register.

    theorem transfer_steps (f : α → β) (fallback : β) (input : List α) (output : List β)
    (state : Option β) :
    (next f fallback)^[input.length + 1] (some (running f fallback input output state)) =
      some (halted f fallback (input.reverse.map f ++ output)) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransfer.next, OAI.MaxCutGames.Reduction.MachineTransfer.running, OAI.MaxCutGames.Reduction.MachineTransfer.halted

  52. theorem OAI.MaxCutGames.Reduction.MachineTransfer.initList_eq line 575
  53. theorem OAI.MaxCutGames.Reduction.MachineTransfer.haltList_eq line 582
  54. theorem OAI.MaxCutGames.Reduction.MachineTransfer.transfer_init_steps line 589
  55. def OAI.MaxCutGames.Reduction.MachineTransfer.outputsInTime line 595
  56. theorem OAI.MaxCutGames.Reduction.MachineTransfer.outputsInTime_steps line 602
  57. def OAI.MaxCutGames.Reduction.MachineTransfer.computableInPolyTime line 606

    Source documentation

    A genuine finite-machine certificate with identity encodings and bound X+1.

    noncomputable def computableInPolyTime (f : α → β) (fallback : β) :
    TM2ComputableInPolyTime (id : List α → List α) (id : List β → List β)
      (fun input => input.reverse.map f) where
…
  58. def OAI.MaxCutGames.Reduction.MachineTransfer.exitAt line 625
  59. def OAI.MaxCutGames.Reduction.MachineTransfer.loopAt line 630
  60. def OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt line 637
  61. theorem OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt_src line 641
  62. theorem OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt_dst line 646
  63. theorem OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt_other line 651
  64. theorem OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt_self line 656
  65. theorem OAI.MaxCutGames.Reduction.MachineTransfer.update_tapesAt_src_inline_MachineTransfer line 660
  66. theorem OAI.MaxCutGames.Reduction.MachineTransfer.update_tapesAt_dst_inline_MachineTransfer line 674
  67. def OAI.MaxCutGames.Reduction.MachineTransfer.nextAt line 685
  68. theorem OAI.MaxCutGames.Reduction.MachineTransfer.stepAt_empty line 690
  69. theorem OAI.MaxCutGames.Reduction.MachineTransfer.stepAt_cons line 704
  70. theorem OAI.MaxCutGames.Reduction.MachineTransfer.transferAt_steps line 722

    Source documentation

    Placement-aware exact transfer, preserving all ambient state and other tapes. The optional exit label is reached in the same final empty-pop transition.

    theorem transferAt_steps (src dst : K) (distinct : src ≠ dst)
    (f : Γ src → Γ dst) (fallback : Γ dst) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Γ Λ (σ × Option (Γ dst)))
    (atLoop : program loopLabel = loopAt src dst f fallback loopLabel exit)
    (base : (k : K) → List (Γ k)) (input : List (Γ src)) (output : List (Γ dst))
    (ambient : σ) (register : Option (Γ dst)) :
    (nextAt dst program)^[input.length + 1]
      (some ⟨some loopLabel, (ambient, register), tapesAt src dst base input output⟩) =
      some ⟨exit, (ambient, none), tapesAt src dst base [] (input.reverse.map f ++ output)⟩ := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Reduction.MachineTransfer.nextAt, OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt

  71. theorem OAI.MaxCutGames.Reduction.MachineTransfer.transferAt_fromTapes line 747

    Source documentation

    The same trace starting with an arbitrary actual ambient tape family.

    theorem transferAt_fromTapes (src dst : K) (distinct : src ≠ dst)
    (f : Γ src → Γ dst) (fallback : Γ dst) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Γ Λ (σ × Option (Γ dst)))
    (atLoop : program loopLabel = loopAt src dst f fallback loopLabel exit)
    (base : (k : K) → List (Γ k)) (ambient : σ) (register : Option (Γ dst)) :
    (nextAt dst program)^[(base src).length + 1]
      (some ⟨some loopLabel, (ambient, register), base⟩) =
      some ⟨exit, (ambient, none),
        tapesAt src dst base [] ((base src).reverse.map f ++ base dst)⟩ := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Reduction.MachineTransfer.nextAt, OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt

  72. def OAI.MaxCutGames.Reduction.MachineTransfer.transferAtInTime line 762

    Source documentation

    A timed execution witness suitable for composing this bridge with other phases of the same actual transition system.

    def transferAtInTime (src dst : K) (distinct : src ≠ dst)
    (f : Γ src → Γ dst) (fallback : Γ dst) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Γ Λ (σ × Option (Γ dst)))
    (atLoop : program loopLabel = loopAt src dst f fallback loopLabel exit)
    (base : (k : K) → List (Γ k)) (ambient : σ) (register : Option (Γ dst)) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some loopLabel, (ambient, register), base⟩
      (some ⟨exit, (ambient, none),
        tapesAt src dst base [] ((base src).reverse.map f ++ base dst)⟩)
      ((base src).length + 1) where
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt