Finite scale and radius caps give a decreasing rank and controller termination.

noncomputable def V7.Stage8Main.controllerLocalSpec {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)) : LocalRunSpec data state inst

A certified local trial execution selected for the current controller state.

Equations

• V7.Stage8Main.controllerLocalSpec data state inst hcached hlarge = Classical.choice ⋯

noncomputable def V7.Stage8Main.controllerReport {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)) (state : RuntimeControllerState d) : TrialReport d

The report of the selected certified local trial execution.

Equations

• V7.Stage8Main.controllerReport data inst hcached hlarge state = (V7.Stage8Main.controllerLocalSpec data state inst hcached hlarge).report

structure V7.Stage8Main.RuntimeFinish (d : ℕ) : Type

The returned point and chronological visits and reports of a successful controller run.

• returned : Point d

  The point returned by the successful final trial.

• visits : List ControllerVisit

  The chronological sequence of visited smoothness and radius estimates.

• reports : List (TrialReport d)

  The chronological sequence of local trial reports.

inductive V7.Stage8Main.RuntimeControllerRunResult (d : ℕ) : Type

A controller run either exhausts its fuel or returns a successful execution record.

• exhausted {d : ℕ} (state : RuntimeControllerState d) : RuntimeControllerRunResult d
• success {d : ℕ} (finish : RuntimeFinish d) : RuntimeControllerRunResult d

noncomputable def V7.Stage8Main.controllerStep {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (report : TrialReport d) : RuntimeControllerRunResult d

The controller transition determined by a local trial's success, radius, or scale outcome.

Equations

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

noncomputable def V7.Stage8Main.runController {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)) : ℕ → RuntimeControllerState d → RuntimeControllerRunResult d

The finite-fuel controller execution driven by certified local trial reports.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage8Main.runController data inst hcached hlarge 0 x✝ = V7.Stage8Main.RuntimeControllerRunResult.exhausted x✝

noncomputable def V7.Stage8Main.controllerConfig {d : ℕ} (data : RuntimeData d) : O3.ControllerConfig

The underlying controller configuration, including the initialization and anchor call count.

Equations

• V7.Stage8Main.controllerConfig data = { initialScale := data.Ma, gradientSizeAtStart := data.G, eps := data.input.eps, prefixCalls := 1 + data.anchorTrace.length }

@[simp]

theorem V7.Stage8Main.scale_eq_config {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : RuntimeControllerState.M data state = (controllerConfig data).scaleAt state.scaleEpoch

@[simp]

theorem V7.Stage8Main.radius_eq_config {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : RuntimeControllerState.D data state = (controllerConfig data).radiusAt state.scaleEpoch state.radiusLevel

noncomputable def V7.Stage8Main.runtimeCaps {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) : O3.ControllerCaps (controllerConfig data) inst.L inst.R

Finite scale and radius caps selected from the instance's smoothness and minimizer distance.

Equations

• V7.Stage8Main.runtimeCaps data inst = Classical.choice ⋯

def V7.Stage8Main.runtimeRank {d : ℕ} {data : RuntimeData d} {L R : ℝ} (caps : O3.ControllerCaps (controllerConfig data) L R) (state : RuntimeControllerState d) : ℕ

The lexicographic termination rank induced by the finite scale and radius caps.

Equations

• V7.Stage8Main.runtimeRank caps state = (caps.scaleCap - state.scaleEpoch) * (caps.radiusCap + 1) + (caps.radiusCap - state.radiusLevel)

theorem V7.Stage8Main.controller_terminates {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 : ℕ) (finish : RuntimeFinish d), runController data inst hcached hlarge fuel initialRuntimeControllerState = RuntimeControllerRunResult.success finish