The successful runtime produces a causal exact query trace and valid output.
theorem
V7.Stage8Main.run_traceExact
{d : ℕ}
(method : O3.FirstOrderMethod d)
(oracle : PairOracle d)
{fuel : ℕ}
{state : method.State}
{history : List (Observation d)}
(hhistory : TraceExact oracle history)
{result : O3.RunResult d}
(hrun : method.runFuel oracle fuel state history = some result)
:
TraceExact oracle result.queries
theorem
V7.Stage8Main.method_run_traceExact
{d : ℕ}
(method : O3.FirstOrderMethod d)
(oracle : PairOracle d)
(input : O3.MethodInput d)
{fuel : ℕ}
{result : O3.RunResult d}
(hrun : method.run oracle input fuel = some result)
:
TraceExact oracle result.queries
theorem
V7.Stage8Main.currentExecution
{d : ℕ}
(input : MethodInput d)
(hp : 1 < input.p)
(heps : 0 < input.eps)
(hM0 : 0 < input.M0)
(inst : PositiveInstance input.p d input.x0)
(hsec : SecantInitialization input inst.oracle)
(hM0L : input.M0 ≤ inst.L)
(rateCoefficient : ℝ)
(hrate : 1 ≤ rateCoefficient)
(hanchorCoefficient : 1 + O3.anchorLogConstant ≤ rateCoefficient)
(hlocal :
∀ (data : RuntimeData d),
data.input = input → runtimeCoefficient data * selectedAmort data.input.p ⋯ ≤ rateCoefficient)
:
∃ (run : PairRunResult d),
Executes (currentMethod d) input inst.oracle run ∧ TraceExact inst.oracle run.trace ∧ run.trace ≠ [] ∧ Option.map O3.Observation.point run.trace.head? = some input.x0 ∧ run.returnedWasQueried ∧ lpNorm (conjugateExponent input.p) (inst.oracle.gradient run.returned) ≤ input.eps ∧ ↑run.postInitializationCallCount ≤ rateCoefficient * conditionBar inst input.eps ^ localCostExponent input.p + rateCoefficient * Real.log (Real.exp 1 + inst.L / input.M0)