All-index ambient time bounds for the actual decision compiler

theorem MIPRE.Introspection.DecisionCompiler.positive_time_bound {c : ℕ} (hc : 1 ≤ c) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), ∀ (S D : Cost.Prog) (lam n : ℕ), 1 ≤ lam → 1 ≤ n → (decider c U S D lam).TimeBoundAt n (ansBound C lam n) C

theorem MIPRE.Introspection.DecisionCompiler.time_bound {c : ℕ} (hc : 1 ≤ c) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), ∀ (S D : Cost.Prog) (lam n : ℕ), (decider c U S D lam).TimeBoundAt n (ansBound C lam n) C

The zero cases and positive branch share one fixed degree and the exact all-index exponential coefficient required by the pipeline.