Selection and certification of the local trial for each runtime exponent regime.

noncomputable def V7.Stage8Main.runtimeCoefficient {d : ℕ} (data : RuntimeData d) : ℝ

The local query-cost coefficient for the runtime's exponent regime.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage8Main.RuntimeControllerState.D_ge_base {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : D data state ≥ data.G / M data state

structure V7.Stage8Main.LocalRunSpec {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (inst : PositiveInstance data.input.p d data.input.x0) : Type

A local report together with its execution, correctness, guard, and query-cost certificates.

• report : TrialReport d

  The report produced by the certified local run.

• executes : (runtimeTrial data state).Executes (RuntimeControllerState.M data state) (RuntimeControllerState.D data state) data.cached inst.oracle self.report
• certificate : TrialCertificate data.input.eps data.input.p (RuntimeControllerState.M data state) (RuntimeControllerState.D data state) inst.L inst.R data.cached inst.oracle self.report
• complete : GuardLedgerComplete data.input.p self.report self.report.checkedGuards
• trace_nonempty : self.report.trace ≠ []
• calls_bound : ↑self.report.calls ≤ runtimeCoefficient data * (RuntimeControllerState.M data state * RuntimeControllerState.D data state / data.input.eps) ^ localCostExponent data.input.p

theorem V7.Stage8Main.runtimeTrial_spec {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (inst : PositiveInstance data.input.p d data.input.x0) (hcached : data.cached.observation = O3.PairOracle.observe inst.oracle data.input.x0) (hlarge : data.input.eps < lpNorm (conjugateExponent data.input.p) (inst.oracle.gradient data.input.x0)) : Nonempty (LocalRunSpec data state inst)