Frozen outer curvature/radius controller

The executable object is a fuel-bounded deterministic controller. Scale failures double the curvature and reset the radius level; radius failures double the tested radius; success is terminal. Running states contain only finite observations, guard reports, and exact counters. Termination is proved from the local-trial obligations and finite numerical search caps; it is not a field of the controller state or of a certificate.

structure O3.ControllerConfig : Type

Inputs known to the outer controller after the anchor phase.

• initialScale : ℝ

  The scale estimate at the controller's initial epoch.

• gradientSizeAtStart : ℝ

  The initial gradient size used to convert scale levels into radii.

• eps : ℝ

  The requested upper bound on the terminal gradient norm.

• prefixCalls : ℕ

  Counted prefix calls (initial query and anchor probes).

def O3.ControllerConfig.scaleAt (cfg : ControllerConfig) (s : ℕ) : ℝ

The scale estimate after the specified number of dyadic doublings.

Equations

• cfg.scaleAt s = 2 ^ s * cfg.initialScale

noncomputable def O3.ControllerConfig.radiusAt (cfg : ControllerConfig) (s j : ℕ) : ℝ

The radius at a given scale epoch and radius-doubling level.

Equations

• cfg.radiusAt s j = 2 ^ j * cfg.gradientSizeAtStart / cfg.scaleAt s

structure O3.ControllerState (d : ℕ) : Type

A running state. Every report in history is a rejected trial.

• scaleEpoch : ℕ

  The current number of scale doublings.

• radiusLevel : ℕ

  The current number of radius doublings within the scale epoch.

• totalCalls : ℕ

  The total number of counted calls, including initialization.

• rejectedCalls : ℕ

  The calls spent on trials already rejected by the controller.

• history : List (TrialReport d)

  The reports of all trials rejected before the current state.

def O3.initialControllerState {d : ℕ} (cfg : ControllerConfig) : ControllerState d

Initialize both search levels at zero and retain the counted initialization cost.

Equations

• O3.initialControllerState cfg = { scaleEpoch := 0, radiusLevel := 0, totalCalls := cfg.prefixCalls, rejectedCalls := 0, history := [] }

def O3.ControllerState.scale {d : ℕ} (cfg : ControllerConfig) (state : ControllerState d) : ℝ

The scale estimate selected by the current controller state.

Equations

• O3.ControllerState.scale cfg state = cfg.scaleAt state.scaleEpoch

noncomputable def O3.ControllerState.radius {d : ℕ} (cfg : ControllerConfig) (state : ControllerState d) : ℝ

The radius selected by the current controller state.

Equations

• O3.ControllerState.radius cfg state = cfg.radiusAt state.scaleEpoch state.radiusLevel

@[reducible, inline]

abbrev O3.TrialRoutine (d : ℕ) : Type

A deterministic local guarded trial routine.

Equations

• O3.TrialRoutine d = (ℝ → ℝ → O3.TrialReport d)

structure O3.ControllerFinish (d : ℕ) : Type

Terminal controller data; it contains no correctness proposition.

• point : Vec d

  The point returned by the successful terminal trial.

• totalCalls : ℕ

  The total counted calls when the controller terminates.

• rejectedCalls : ℕ

  The portion of the total cost spent on rejected trials.

• terminalCalls : ℕ

  The calls used by the successful terminal trial.

• history : List (TrialReport d)

  The trial reports retained in the completed controller execution.

inductive O3.ControllerStep (d : ℕ) : Type

One controller transition either produces another running state or a completed result.

• next {d : ℕ} (state : ControllerState d) : ControllerStep d
• done {d : ℕ} (finish : ControllerFinish d) : ControllerStep d

def O3.controllerStep {d : ℕ} (_cfg : ControllerConfig) (state : ControllerState d) (report : TrialReport d) : ControllerStep d

One exact outer-controller transition.

Equations

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

noncomputable def O3.currentTrial {d : ℕ} (routine : TrialRoutine d) (cfg : ControllerConfig) (state : ControllerState d) : TrialReport d

Run the local trial routine at the current scale and radius.

Equations

• O3.currentTrial routine cfg state = routine (O3.ControllerState.scale cfg state) (O3.ControllerState.radius cfg state)

inductive O3.ControllerRunResult (d : ℕ) : Type

A bounded controller execution either exhausts its fuel or returns a successful result.

• exhausted {d : ℕ} (state : ControllerState d) : ControllerRunResult d
• success {d : ℕ} (finish : ControllerFinish d) : ControllerRunResult d

noncomputable def O3.runController {d : ℕ} (routine : TrialRoutine d) (cfg : ControllerConfig) : ℕ → ControllerState d → ControllerRunResult d

Explicit deterministic fuel-bounded execution; no termination is assumed.

Equations

• One or more equations did not get rendered due to their size.
• O3.runController routine cfg 0 x✝ = O3.ControllerRunResult.exhausted x✝

def O3.ControllerState.Accounting {d : ℕ} (cfg : ControllerConfig) (state : ControllerState d) : Prop

Exact invariant separating prefix, rejected, and terminal calls.

Equations

• O3.ControllerState.Accounting cfg state = (state.totalCalls = cfg.prefixCalls + state.rejectedCalls)

def O3.ControllerFinish.Accounting {d : ℕ} (cfg : ControllerConfig) (finish : ControllerFinish d) : Prop

The total cost splits into initialization, rejected trials, and the terminal trial.

Equations

• O3.ControllerFinish.Accounting cfg finish = (finish.totalCalls = cfg.prefixCalls + finish.rejectedCalls + finish.terminalCalls)

def O3.trialReportsCallCount {d : ℕ} (reports : List (TrialReport d)) : ℕ

Sum of calls recorded by a chronological list of local-trial reports.

Equations

• O3.trialReportsCallCount reports = (List.map O3.TrialReport.calls reports).sum

def O3.ControllerState.HistoryAccounting {d : ℕ} (cfg : ControllerConfig) (state : ControllerState d) : Prop

Running-state counters agree with the complete rejected-report history.

Equations

• O3.ControllerState.HistoryAccounting cfg state = (state.totalCalls = cfg.prefixCalls + O3.trialReportsCallCount state.history ∧ state.rejectedCalls = O3.trialReportsCallCount state.history)

def O3.ControllerFinish.HistoryAccounting {d : ℕ} (cfg : ControllerConfig) (finish : ControllerFinish d) : Prop

Terminal counters agree both with history and with rejected/terminal splitting.

Equations

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

theorem O3.initialControllerState_accounting {d : ℕ} (cfg : ControllerConfig) : ControllerState.Accounting cfg (initialControllerState cfg)

theorem O3.initialControllerState_historyAccounting {d : ℕ} (cfg : ControllerConfig) : ControllerState.HistoryAccounting cfg (initialControllerState cfg)

theorem O3.controllerStep_accounting {d : ℕ} {cfg : ControllerConfig} {state : ControllerState d} (hstate : ControllerState.Accounting cfg state) (report : TrialReport d) : match controllerStep cfg state report with | ControllerStep.next state' => ControllerState.Accounting cfg state' | ControllerStep.done finish => ControllerFinish.Accounting cfg finish

theorem O3.runController_accounting {d : ℕ} (routine : TrialRoutine d) (cfg : ControllerConfig) {fuel : ℕ} {state : ControllerState d} (hstate : ControllerState.Accounting cfg state) : match runController routine cfg fuel state with | ControllerRunResult.exhausted state' => ControllerState.Accounting cfg state' | ControllerRunResult.success finish => ControllerFinish.Accounting cfg finish

theorem O3.controllerStep_historyAccounting {d : ℕ} {cfg : ControllerConfig} {state : ControllerState d} (hstate : ControllerState.HistoryAccounting cfg state) (report : TrialReport d) : match controllerStep cfg state report with | ControllerStep.next state' => ControllerState.HistoryAccounting cfg state' | ControllerStep.done finish => ControllerFinish.HistoryAccounting cfg finish

theorem O3.runController_historyAccounting {d : ℕ} (routine : TrialRoutine d) (cfg : ControllerConfig) {fuel : ℕ} {state : ControllerState d} (hstate : ControllerState.HistoryAccounting cfg state) : match runController routine cfg fuel state with | ControllerRunResult.exhausted state' => ControllerState.HistoryAccounting cfg state' | ControllerRunResult.success finish => ControllerFinish.HistoryAccounting cfg finish

noncomputable def O3.ControllerNext {d : ℕ} (routine : TrialRoutine d) (cfg : ControllerConfig) (state' state : ControllerState d) : Prop

Relation consisting of one nonterminal deterministic controller step.

Equations

• O3.ControllerNext routine cfg state' state = (O3.controllerStep cfg state (O3.currentTrial routine cfg state) = O3.ControllerStep.next state')

structure O3.ControllerCaps (cfg : ControllerConfig) (L R : ℝ) : Type

Finite numerical caps for the two geometric searches.

• scaleCap : ℕ

  A scale epoch beyond which the guessed scale dominates the true smoothness scale.

• radiusCap : ℕ

  A radius level sufficient to dominate the minimizer distance within the relevant epochs.

• scaleDominates (s : ℕ) : self.scaleCap ≤ s → L ≤ cfg.scaleAt s
• radiusDominates (s j : ℕ) : s ≤ self.scaleCap → self.radiusCap ≤ j → R ≤ cfg.radiusAt s j

theorem O3.exists_controllerCaps (cfg : ControllerConfig) (L R : ℝ) (hM : 0 < cfg.initialScale) (hG : 0 < cfg.gradientSizeAtStart) (hR : 0 ≤ R) : Nonempty (ControllerCaps cfg L R)

The two finite search caps follow from positivity; they are not supplied to the method.

def O3.controllerRank {d : ℕ} {cfg : ControllerConfig} {L R : ℝ} (caps : ControllerCaps cfg L R) (state : ControllerState d) : ℕ

Lexicographic search rank inside the finite cap rectangle.

Equations

• O3.controllerRank caps state = (caps.scaleCap - state.scaleEpoch) * (caps.radiusCap + 1) + (caps.radiusCap - state.radiusLevel)

theorem O3.controllerNext_rank_lt {d : ℕ} (oracle : PairOracle d) (gradientSize : Vec d → ℝ) (routine : TrialRoutine d) (cfg : ControllerConfig) (L R : ℝ) (caps : ControllerCaps cfg L R) {state state' : ControllerState d} (hs : state.scaleEpoch ≤ caps.scaleCap) (hj : state.radiusLevel ≤ caps.radiusCap) (hvalid : TrialValid oracle gradientSize cfg.eps L R (ControllerState.scale cfg state) (ControllerState.radius cfg state) (currentTrial routine cfg state)) (hnext : ControllerNext routine cfg state' state) : controllerRank caps state' < controllerRank caps state

theorem O3.controllerNext_wellFounded {d : ℕ} (oracle : PairOracle d) (gradientSize : Vec d → ℝ) (routine : TrialRoutine d) (cfg : ControllerConfig) (L R : ℝ) (caps : ControllerCaps cfg L R) (hvalid : ∀ (state : ControllerState d), state.scaleEpoch ≤ caps.scaleCap → state.radiusLevel ≤ caps.radiusCap → TrialValid oracle gradientSize cfg.eps L R (ControllerState.scale cfg state) (ControllerState.radius cfg state) (currentTrial routine cfg state)) : WellFounded fun (state' state : ControllerState d) => state.scaleEpoch ≤ caps.scaleCap ∧ state.radiusLevel ≤ caps.radiusCap ∧ ControllerNext routine cfg state' state

theorem O3.controllerStep_done_queried {d : ℕ} {oracle : PairOracle d} {gradientSize : Vec d → ℝ} {L R : ℝ} {cfg : ControllerConfig} {state : ControllerState d} {report : TrialReport d} {finish : ControllerFinish d} (hvalid : TrialValid oracle gradientSize cfg.eps L R (ControllerState.scale cfg state) (ControllerState.radius cfg state) report) (hdone : controllerStep cfg state report = ControllerStep.done finish) : WasQueried report.observations finish.point ∧ gradientSize (oracle.gradient finish.point) ≤ cfg.eps

A successful finish points to an actually queried terminal observation.

theorem O3.guardedControllerWithCaps {d : ℕ} (oracle : PairOracle d) (gradientSize : Vec d → ℝ) (routine : TrialRoutine d) (cfg : ControllerConfig) (L R : ℝ) (caps : ControllerCaps cfg L R) (hvalid : ∀ (state : ControllerState d), state.scaleEpoch ≤ caps.scaleCap → state.radiusLevel ≤ caps.radiusCap → TrialValid oracle gradientSize cfg.eps L R (ControllerState.scale cfg state) (ControllerState.radius cfg state) (currentTrial routine cfg state)) : ∃ (fuel : ℕ) (finish : ControllerFinish d), runController routine cfg fuel (initialControllerState cfg) = ControllerRunResult.success finish ∧ ControllerFinish.Accounting cfg finish ∧ ControllerFinish.HistoryAccounting cfg finish ∧ ∃ terminalReport ∈ finish.history, WasQueried terminalReport.observations finish.point ∧ gradientSize (oracle.gradient finish.point) ≤ cfg.eps

Native formal counterpart of the frozen guarded-controller lemma at the algorithm-semantics layer. It proves termination from the two finite geometric search caps, returns only a queried successful point, and proves the exact prefix/rejected/terminal call decomposition. Regime modules discharge TrialValid and the numerical cap hypotheses.

theorem O3.guardedControllerCore {d : ℕ} (oracle : PairOracle d) (gradientSize : Vec d → ℝ) (routine : TrialRoutine d) (cfg : ControllerConfig) (L R : ℝ) (hM : 0 < cfg.initialScale) (hG : 0 < cfg.gradientSizeAtStart) (hR : 0 ≤ R) (hvalid : ∀ (state : ControllerState d), TrialValid oracle gradientSize cfg.eps L R (ControllerState.scale cfg state) (ControllerState.radius cfg state) (currentTrial routine cfg state)) : ∃ (fuel : ℕ) (finish : ControllerFinish d), runController routine cfg fuel (initialControllerState cfg) = ControllerRunResult.success finish ∧ ControllerFinish.Accounting cfg finish ∧ ControllerFinish.HistoryAccounting cfg finish ∧ ∃ terminalReport ∈ finish.history, WasQueried terminalReport.observations finish.point ∧ gradientSize (oracle.gradient finish.point) ≤ cfg.eps

The guarded controller with its finite geometric caps derived internally from the positive scales. Thus neither termination nor a successful trace is a public input.