OAI/Computability/UniqueGames/Machines/Runtime.lean

GitHub source file

13 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.UniqueGamesTheorem.Foundations.Complexity.Runtime.statementPushBound line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.maxLabelPushes line 26
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.maxLabelPushes_ge line 31
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound line 45

    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.UniqueGamesTheorem.Foundations.Complexity.Runtime.statement_le_programPushBound line 48
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.stepAuxStackLength line 53
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.iterateSizeBound line 96
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.executionSizeBound line 109

    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.UniqueGamesTheorem.Foundations.Complexity.Runtime.stepStackLength line 132
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.initialStackLength line 145
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.haltedOutputLength line 152
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.outputLength_le line 156
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.encodedOutputLength line 170

    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.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound