Stage 12A: causal initial-query and anchor prefix

This module is executable plumbing only. The machine is indexed by the dimension and receives the exponent at runtime through MethodInput. Its transition function contains no oracle or admissible instance; objective data enters only through the continuation of Action.query.

noncomputable def O3.anchorPrefixConfig {d : ℕ} (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) : AnchorConfig d

Runtime-only anchor configuration reconstructed after the counted query at x0. This definition has no proof-side problem parameters.

Equations

• O3.anchorPrefixConfig input f0 g0 G = { q := O3.conjugateExponent input.p, x₀ := input.x0, f₀ := f0, g₀ := g0, G := G, M₀ := input.M0 }

inductive O3.AnchorPrefixState (d : ℕ) : Type

Causal prefix states. earlyDone and accepted are explicit handoff states; Stage 12A terminates there, while a later controller may reuse the unchanged preceding transitions and replace only their terminal actions.

• needX0 {d : ℕ} (input : MethodInput d) : AnchorPrefixState d
• anchoring {d : ℕ} (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) (epoch : ℕ) : AnchorPrefixState d
• earlyDone {d : ℕ} (input : MethodInput d) : AnchorPrefixState d
• accepted {d : ℕ} (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) (epoch : ℕ) : AnchorPrefixState d

noncomputable def O3.anchorPrefixAction {d : ℕ} : AnchorPrefixState d → Action d (AnchorPrefixState d)

One observation-driven prefix transition. The only objective values used below are fields of observations delivered by query continuations.

Equations

• One or more equations did not get rendered due to their size.
• O3.anchorPrefixAction (O3.AnchorPrefixState.earlyDone input) = O3.Action.done input.x0

noncomputable def O3.anchorPrefixMethod (d : ℕ) : FirstOrderMethod d

The one dimension-indexed concrete first-order method for the causal prefix. The real exponent is read only from runtime input.

Equations

• O3.anchorPrefixMethod d = { State := O3.AnchorPrefixState d, initial := O3.AnchorPrefixState.needX0, action := O3.anchorPrefixAction }

theorem O3.anchorPrefixMethod_first_action {d : ℕ} (input : MethodInput d) : ∃ (next : Observation d → AnchorPrefixState d), (anchorPrefixMethod d).action ((anchorPrefixMethod d).initial input) = Action.query input.x0 next

The first executable action is definitionally the counted query at x0.

theorem O3.anchorPrefixMethod_early_run {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (hsmall : lpNorm (conjugateExponent input.p) (oracle.gradient input.x0) ≤ input.eps) : (anchorPrefixMethod d).run oracle input 2 = some { returned := input.x0, queries := [oracle.observe input.x0] }

The one-query early-success execution, before any anchor probe.

theorem O3.anchorPrefixMethod_early_exact {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (hsmall : lpNorm (conjugateExponent input.p) (oracle.gradient input.x0) ≤ input.eps) : ∃ (result : RunResult d), (anchorPrefixMethod d).run oracle input 2 = some result ∧ result.returned = input.x0 ∧ result.queries = [oracle.observe input.x0] ∧ result.callCount = 1 ∧ TraceExact oracle result.queries ∧ result.returnedWasQueried

theorem O3.anchorPrefixMethod_admissible_early {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) (hsmall : lpNorm (conjugateExponent p) (P.grad P.x0) ≤ P.eps) : ∃ (result : RunResult d), (anchorPrefixMethod d).run P.oracle P.methodInput 2 = some result ∧ result.returned = P.x0 ∧ result.queries = [P.oracle.observe P.x0] ∧ result.callCount = 1 ∧ TraceExact P.oracle result.queries ∧ result.returnedWasQueried

The public one-query early branch specialized to any admissible instance; the method itself remains the same dimension-indexed object.

theorem O3.anchorPrefixMethod_runFuel_anchoring_succ {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) (fuel epoch : ℕ) (history : OracleTrace d) : have cfg := anchorPrefixConfig input f0 g0 G; have D := anchorRadius cfg.G cfg.M₀ epoch; have y := anchorProbePoint cfg.q cfg.x₀ cfg.g₀ cfg.G cfg.M₀ epoch; (anchorPrefixMethod d).runFuel oracle (fuel + 1) (AnchorPrefixState.anchoring input f0 g0 G epoch) history = (anchorPrefixMethod d).runFuel oracle fuel (if oracle.value y ≤ cfg.f₀ - cfg.G * D / 2 then AnchorPrefixState.accepted input f0 g0 G epoch else AnchorPrefixState.anchoring input f0 g0 G (epoch + 1)) (history ++ [oracle.observe y])

One executable anchoring query, exposed without unfolding the subsequent recursive machine step.

theorem O3.anchorPrefixMethod_runFuel_accepted_succ {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) (fuel epoch : ℕ) (history : OracleTrace d) : (anchorPrefixMethod d).runFuel oracle (fuel + 1) (AnchorPrefixState.accepted input f0 g0 G epoch) history = some { returned := anchorProbePoint (anchorPrefixConfig input f0 g0 G).q (anchorPrefixConfig input f0 g0 G).x₀ (anchorPrefixConfig input f0 g0 G).g₀ (anchorPrefixConfig input f0 g0 G).G (anchorPrefixConfig input f0 g0 G).M₀ epoch, queries := history }

An accepted handoff consumes exactly the final done action and makes no additional query.

theorem O3.anchorPrefixMethod_anchorSuffix_of_runAnchor {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) {fuel epoch : ℕ} {history pre : OracleTrace d} {ar : AnchorResult d} : runAnchor oracle (anchorPrefixConfig input f0 g0 G) fuel epoch history = some ar → (anchorPrefixMethod d).runFuel oracle (fuel + 1) (AnchorPrefixState.anchoring input f0 g0 G epoch) (pre ++ history) = some { returned := ar.acceptedPoint, queries := pre ++ ar.observations }

Proof-level anchor success produces the identical causal suffix execution. The extra unit of method fuel is the final done action.

theorem O3.anchorPrefixMethod_runAnchor_of_anchorSuffix {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) {fuel epoch : ℕ} {history pre : OracleTrace d} {result : RunResult d} : (anchorPrefixMethod d).runFuel oracle (fuel + 1) (AnchorPrefixState.anchoring input f0 g0 G epoch) (pre ++ history) = some result → ∃ (ar : AnchorResult d), runAnchor oracle (anchorPrefixConfig input f0 g0 G) fuel epoch history = some ar ∧ result = { returned := ar.acceptedPoint, queries := pre ++ ar.observations }

Every causal suffix success reconstructs the identical proof-level anchor result.

theorem O3.anchorPrefixMethod_anchorSuffix_iff {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (f0 : ℝ) (g0 : Vec d) (G : ℝ) {fuel epoch : ℕ} {history pre : OracleTrace d} {result : RunResult d} : (anchorPrefixMethod d).runFuel oracle (fuel + 1) (AnchorPrefixState.anchoring input f0 g0 G epoch) (pre ++ history) = some result ↔ ∃ (ar : AnchorResult d), runAnchor oracle (anchorPrefixConfig input f0 g0 G) fuel epoch history = some ar ∧ result = { returned := ar.acceptedPoint, queries := pre ++ ar.observations }

Exact bidirectional suffix equivalence.

theorem O3.anchorPrefixMethod_anchor_run_of_runAnchor {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (hlarge : input.eps < lpNorm (conjugateExponent input.p) (oracle.gradient input.x0)) {anchorFuel : ℕ} {ar : AnchorResult d} (hrun : runAnchor oracle (anchorPrefixConfig input (oracle.value input.x0) (oracle.gradient input.x0) (lpNorm (conjugateExponent input.p) (oracle.gradient input.x0))) anchorFuel 0 [] = some ar) : (anchorPrefixMethod d).run oracle input (anchorFuel + 2) = some { returned := ar.acceptedPoint, queries := [oracle.observe input.x0] ++ ar.observations }

Full nontrivial prefix equivalence in the proof-level-to-causal direction.

theorem O3.anchorPrefixMethod_runAnchor_of_anchor_run {d : ℕ} (oracle : PairOracle d) (input : MethodInput d) (hlarge : input.eps < lpNorm (conjugateExponent input.p) (oracle.gradient input.x0)) (anchorFuel : ℕ) (result : RunResult d) (hrun : (anchorPrefixMethod d).run oracle input (anchorFuel + 2) = some result) : ∃ (ar : AnchorResult d), runAnchor oracle (anchorPrefixConfig input (oracle.value input.x0) (oracle.gradient input.x0) (lpNorm (conjugateExponent input.p) (oracle.gradient input.x0))) anchorFuel 0 [] = some ar ∧ result.returned = ar.acceptedPoint ∧ result.queries = [oracle.observe input.x0] ++ ar.observations

Converse reconstruction: every accepted causal run of the corresponding fuel has one proof-level runAnchor result with identical accepted data and trace.

theorem O3.runAnchor_acceptedPoint_queried {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) {fuel epoch : ℕ} {history : OracleTrace d} {ar : AnchorResult d} : runAnchor oracle cfg fuel epoch history = some ar → WasQueried ar.observations ar.acceptedPoint

The accepted probe is the last observation of every successful proof-level anchor execution.

theorem O3.anchorPrefixMethod_admissible_anchor {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) (hlarge : P.eps < lpNorm (conjugateExponent p) (P.grad P.x0)) : have N := ⌈Real.logb 2 (P.L / P.M0)⌉₊; ∃ (ar : AnchorResult d) (result : RunResult d), runAnchor P.oracle P.anchorConfig (1 + N) 0 [] = some ar ∧ (anchorPrefixMethod d).run P.oracle P.methodInput (1 + N + 2) = some result ∧ result.returned = ar.acceptedPoint ∧ result.queries = [P.oracle.observe P.x0] ++ ar.observations ∧ result.callCount = 1 + List.length ar.observations ∧ TraceExact P.oracle result.queries ∧ result.returnedWasQueried ∧ ar.acceptedScale < 2 * P.L ∧ ar.acceptedRadius ≤ 2 * P.radius ∧ List.length ar.observations ≤ 1 + N

Stage-3 termination transported to the concrete causal prefix.