Documentation

MIPRE.Foundations.Introspection.ClockCost

Uniform runtime bounds for the growing introspection clock #

For each fixed positive exponent, clock construction runs in polynomial time in its unary output budget, uniformly in the parameter and index. The existing polynomial-exponent absorption lemma then gives another introspection budget.

source
noncomputable def MIPRE.Introspection.ClockArithmetic.unaryCostPoly :
Polynomial ℕ
Equations
Instances For
    source
    theorem MIPRE.Introspection.ClockArithmetic.esize_le_value {n M : ℕ} (h : n ≤ M) :
    Cost.esize n ≤ 4 * M + 1
    source
    theorem MIPRE.Introspection.ClockArithmetic.unaryCost_le {n M : ℕ} (h : n ≤ M) :
    unaryCost n ≤ Polynomial.eval M unaryCostPoly
    source
    noncomputable def MIPRE.Introspection.ClockArithmetic.mulCostPoly :
    Polynomial ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.ClockArithmetic.mulCost_le {a b M : ℕ} (ha : a ≤ M) (hb : b ≤ M) :
      mulCost a b ≤ Polynomial.eval M mulCostPoly
      source
      noncomputable def MIPRE.Introspection.ClockArithmetic.clockCostPoly (k : ℕ) :
      Polynomial ℕ
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.ClockArithmetic.clock_arguments_le {k lam n : ℕ} (hk : 1 ≤ k) (hl : 1 ≤ lam) (hn : 1 ≤ n) :
        lam ≤ ansBound k lam n ∧ n ≤ ansBound k lam n ∧ lam * n + 1 ≤ ansBound k lam n ∧ (lam * n + 1) ^ k ≤ ansBound k lam n
        source
        theorem MIPRE.Introspection.ClockArithmetic.growingClock_cost_le {k lam n : ℕ} (hk : 1 ≤ k) (hl : 1 ≤ lam) (hn : 1 ≤ n) :
        uniformCost k lam n + Cost.esize lam + Cost.esize n + 3 ≤ Polynomial.eval (ansBound k lam n) (clockCostPoly k)

        One polynomial controls all parameter/index instances of the actual clock.

        source
        theorem MIPRE.Introspection.growingClock_polynomial_time {k : ℕ} (hk : 1 ≤ k) :
        ∃ (Q : Polynomial ℕ), ∀ (lam n : ℕ), 1 ≤ lam → 1 ≤ n → Cost.HaltsWithin (growingClock k lam).prog (Cost.encode n) (Polynomial.eval (ansBound k lam n) Q)
        source
        theorem MIPRE.Introspection.growingClock_ansBound_time {k : ℕ} (hk : 1 ≤ k) :
        ∃ (C : ℕ), ∀ (lam n : ℕ), 1 ≤ lam → 1 ≤ n → Cost.HaltsWithin (growingClock k lam).prog (Cost.encode n) (ansBound C lam n)

        Generating the unary clock itself fits a uniformly enlarged introspection budget.