Stage 8: one current V7 runtime-p machine

This is a new V7 dispatcher. It uses the current V7 local trials and only the primitive O3.FirstOrderMethod execution interface from the historical namespace.

@[instance_reducible]

noncomputable def V7.Stage8Main.runtimePropDecidable (q : Prop) : Decidable q

Classical proposition decisions used locally by the runtime construction.

Equations

• V7.Stage8Main.runtimePropDecidable q = Classical.propDecidable q

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

The validated primitive input, cached gradient, and accepted anchor-search data.

• input : MethodInput d

  The primitive numerical input of the method.

• hp : 1 < self.input.p
• heps : 0 < self.input.eps
• hM0 : 0 < self.input.M0
• cached : CachedPair d

  The initial observation reused by subsequent local trials.

• G : ℝ

  The dual norm of the cached initial gradient.

• G_eq : self.G = lpNorm (conjugateExponent self.input.p) self.cached.observation.gradient
• hG : 0 < self.G
• anchorEpoch : ℕ

  The accepted dyadic epoch of the anchor search.

• anchorTrace : List (Observation d)

  The observations made during the anchor search.

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

The accepted anchor smoothness estimate.

Equations

• data.Ma = 2 ^ data.anchorEpoch * data.input.M0

theorem V7.Stage8Main.RuntimeData.Ma_pos {d : ℕ} (data : RuntimeData d) : 0 < data.Ma

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

The geometric search indices and chronological history of the runtime controller.

• scaleEpoch : ℕ

  The number of smoothness doublings after the accepted anchor estimate.

• radiusLevel : ℕ

  The radius-doubling index at the current smoothness scale.

• visits : List ControllerVisit

  The completed controller visits.

• reports : List (TrialReport d)

  The local trial reports associated with the completed visits.

def V7.Stage8Main.initialRuntimeControllerState {d : ℕ} : RuntimeControllerState d

The controller state before its first local trial.

Equations

• V7.Stage8Main.initialRuntimeControllerState = { scaleEpoch := 0, radiusLevel := 0, visits := [], reports := [] }

noncomputable def V7.Stage8Main.RuntimeControllerState.M {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : ℝ

The current dyadic smoothness estimate.

Equations

• V7.Stage8Main.RuntimeControllerState.M data state = 2 ^ state.scaleEpoch * data.Ma

noncomputable def V7.Stage8Main.RuntimeControllerState.D {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : ℝ

The current dyadic radius estimate normalized by the initial gradient size.

Equations

• V7.Stage8Main.RuntimeControllerState.D data state = 2 ^ state.radiusLevel * data.G / V7.Stage8Main.RuntimeControllerState.M data state

theorem V7.Stage8Main.RuntimeControllerState.M_pos {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : 0 < M data state

theorem V7.Stage8Main.RuntimeControllerState.D_pos {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : 0 < D data state

noncomputable def V7.Stage8Main.runtimeTrial {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : LocalTrial d

The certified local trial selected for the current exponent regime and controller estimates.

Equations

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

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

The next controller state after a scale failure, resetting the radius level.

Equations

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

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

The next controller state after a radius failure, retaining the current smoothness scale.

Equations

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

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

The causal method's initialization, anchor-search, local-trial, and terminal states.

• needX0 {d : ℕ} (input : MethodInput d) : CurrentMethodState d
• earlyDone {d : ℕ} (input : MethodInput d) : CurrentMethodState d
• anchoring {d : ℕ} (input : MethodInput d) (hp : 1 < input.p) (heps : 0 < input.eps) (hM0 : 0 < input.M0) (cached : CachedPair d) (G : ℝ) (G_eq : G = lpNorm (conjugateExponent input.p) cached.observation.gradient) (hG : 0 < G) (epoch : ℕ) (observations : List (Observation d)) : CurrentMethodState d
• controllerReady {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : CurrentMethodState d
• localTrial {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (machineState : (runtimeTrial data state).State) (observations : List (Observation d)) : CurrentMethodState d

noncomputable def V7.Stage8Main.startLocalAction {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) : O3.Action d (CurrentMethodState d)

The first action of the current local trial, embedded in the global method state.

Equations

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

noncomputable def V7.Stage8Main.continueLocalAction {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (machineState : (runtimeTrial data state).State) (observations : List (Observation d)) : O3.Action d (CurrentMethodState d)

The next local query or controller transition after a local trial observation.

Equations

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

noncomputable def V7.Stage8Main.currentMethodAction {d : ℕ} : CurrentMethodState d → O3.Action d (CurrentMethodState d)

The observable state transition of the complete parameter-free method.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage8Main.currentMethodAction (V7.Stage8Main.CurrentMethodState.earlyDone input) = O3.Action.done input.x0
• V7.Stage8Main.currentMethodAction (V7.Stage8Main.CurrentMethodState.controllerReady data state) = V7.Stage8Main.startLocalAction data state
• V7.Stage8Main.currentMethodAction (V7.Stage8Main.CurrentMethodState.localTrial data state machineState observations) = V7.Stage8Main.continueLocalAction data state machineState observations

noncomputable def V7.Stage8Main.currentMethod (d : ℕ) : O3.FirstOrderMethod d

The first-order method implementing initialization, anchor search, and the geometric controller.

Equations

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

noncomputable def V7.Stage8Main.currentMethodFamily : RuntimeMethodFamily

One family is fixed before runtime p, dimension-specific input, or oracle.

Equations

• V7.Stage8Main.currentMethodFamily d = V7.Stage8Main.currentMethod d