The controller preserves valid reports, chronological paths, and terminal correctness certificates.

def V7.Stage8Main.VisitTransition {d : ℕ} (G : ℝ) (current next : ControllerVisit) (report : TrialReport d) : Prop

The allowed change of estimates after a radius or scale failure.

Equations

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

theorem V7.Stage8Main.controllerPath_append {d : ℕ} (G Ma Da : ℝ) {visits : List ControllerVisit} {reports : List (TrialReport d)} (hpath : ControllerPath G Ma Da visits reports) (newVisit : ControllerVisit) (newReport : TrialReport d) (hlast : ∀ (current : ControllerVisit) (report : TrialReport d), VisitAt visits (visits.length - 1) current → ReportAt reports (reports.length - 1) report → VisitTransition G current newVisit report) : ControllerPath G Ma Da (visits ++ [newVisit]) (reports ++ [newReport])

def V7.Stage8Main.ValidReport {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) (visit : ControllerVisit) (report : TrialReport d) : Prop

A report has complete guards, valid trial certificates, and the required local cost bound.

Equations

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

theorem V7.Stage8Main.validReport_of_spec {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (inst : PositiveInstance data.input.p d data.input.x0) (spec : LocalRunSpec data state inst) : ValidReport data inst { M := RuntimeControllerState.M data state, D := RuntimeControllerState.D data state } spec.report

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

The validity and path conditions maintained before the next controller trial.

• valid : List.Forall₂ (ValidReport data inst) state.visits state.reports
• pathWithNext (report : TrialReport d) : ControllerPath data.G data.Ma (data.G / data.Ma) (state.visits ++ [{ M := RuntimeControllerState.M data state, D := RuntimeControllerState.D data state }]) (state.reports ++ [report])

theorem V7.Stage8Main.initial_readyInvariant {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) : ReadyInvariant data inst initialRuntimeControllerState

theorem V7.Stage8Main.readyInvariant_nextScale {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) (state : RuntimeControllerState d) (spec : LocalRunSpec data state inst) (failed : ObservableGuardCheck d) (hout : spec.report.outcome = TrialOutcome.scale failed) (hinv : ReadyInvariant data inst state) : ReadyInvariant data inst (nextScale data state spec.report)

theorem V7.Stage8Main.readyInvariant_nextRadius {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) (state : RuntimeControllerState d) (spec : LocalRunSpec data state inst) (terminal : Observation d) (hout : spec.report.outcome = TrialOutcome.radius terminal) (hinv : ReadyInvariant data inst state) : ReadyInvariant data inst (nextRadius data state spec.report)

structure V7.Stage8Main.FinishInvariant {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) (finish : RuntimeFinish d) : Prop

The path, report validity, and terminal certificate of a successful controller execution.

• path : ControllerPath data.G data.Ma (data.G / data.Ma) finish.visits finish.reports
• valid : List.Forall₂ (ValidReport data inst) finish.visits finish.reports
• terminal : ∃ (report : TrialReport d) (terminal : Observation d), report ∈ finish.reports ∧ report.outcome = TrialOutcome.success terminal ∧ terminal.point = finish.returned ∧ terminal ∈ report.trace ∧ lpNorm (conjugateExponent data.input.p) (inst.oracle.gradient terminal.point) ≤ data.input.eps

theorem V7.Stage8Main.runController_invariant {d : ℕ} (data : RuntimeData 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)) {fuel : ℕ} {state : RuntimeControllerState d} {finish : RuntimeFinish d} : ReadyInvariant data inst state → runController data inst hcached hlarge fuel state = RuntimeControllerRunResult.success finish → FinishInvariant data inst finish