Stage 3: the native gradient-ray anchor

This module closes the remaining proof-side bridges for the frozen anchor: acceptance at the first dyadic scale dominating L, the actual infimum distance to the minimizer set, and the displayed base-two ceiling count.

noncomputable def O3.AdmissibleInstance.anchorConfig {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : AnchorConfig d

The anchor loop configuration contains only data already observed at x₀; neither L nor a minimizer nor the solution radius is an input.

Equations

• P.anchorConfig = { q := O3.conjugateExponent p, x₀ := P.x0, f₀ := P.f P.x0, g₀ := P.grad P.x0, G := O3.lpNorm (O3.conjugateExponent p) (P.grad P.x0), M₀ := P.M0 }

theorem O3.anchorScaleCap_le_logCeil {M₀ L : ℝ} (hM₀ : 0 < M₀) (hL : 0 < L) : anchorScaleCap M₀ L hM₀ ≤ ⌈Real.logb 2 (L / M₀)⌉₊

The first dyadic scale dominating L occurs no later than the exact source base-two ceiling.

theorem O3.anchor_cap_test_passes {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) (hGpos : 0 < lpNorm (conjugateExponent p) (P.grad P.x0)) {epoch : ℕ} (hscale : P.L ≤ anchorScale P.M0 epoch) : have cfg := P.anchorConfig; have D := anchorRadius cfg.G cfg.M₀ epoch; have y := anchorProbePoint cfg.q cfg.x₀ cfg.g₀ cfg.G cfg.M₀ epoch; P.oracle.value y ≤ cfg.f₀ - cfg.G * D / 2

At every dyadic scale dominating the true smoothness constant, the observable anchor test passes. This is derived from the exact L/2 descent lemma and the native norming identities, rather than supplied as a certificate.

theorem O3.anchor_radius_le_two_minimizerDistance {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) (hGpos : 0 < lpNorm (conjugateExponent p) (P.grad P.x0)) {D : ℝ} {y : Vec d} (haccept : AnchorTest P.f P.x0 (lpNorm (conjugateExponent p) (P.grad P.x0)) D y) : D ≤ 2 * P.radius

An accepted test controls the radius by the actual infimum distance to the nonempty minimizer set. No closest minimizer is selected or assumed.

theorem O3.runAnchor_some_add_fuel {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) {fuel start : ℕ} {history : OracleTrace d} {result : AnchorResult d} (hrun : runAnchor oracle cfg fuel start history = some result) (extra : ℕ) : runAnchor oracle cfg (fuel + extra) start history = some result

Once the deterministic loop has returned, additional unused fuel cannot change its first accepted result.

def O3.AnchorStatement : Prop

Transparent source-level carrier for the frozen gradient-ray anchor. The only quantified algorithmic object is the admissible instance; L, the minimizer set, and its distance are used only in the correctness conclusion.

Equations

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

theorem O3.anchor : AnchorStatement

Native closure of TeX Lemma lem:anchor.