Secant and accepted-anchor certificates

This module proves the parts of the gradient-ray anchor that reduce directly to finite-dimensional ell_p/ell_q Hölder geometry. It deliberately does not postulate termination or an accepted trace as data.

def O3.LipschitzGradient {d : ℕ} (p q L : ℝ) (grad : Point d → Point d) : Prop

The exact ell_p → ell_q Lipschitz-gradient hypothesis.

Equations

• O3.LipschitzGradient p q L grad = ∀ (x y : O3.Point d), O3.lpNorm q (grad x - grad y) ≤ L * O3.lpNorm p (x - y)

noncomputable def O3.secantScale {d : ℕ} (p q : ℝ) (grad : Point d → Point d) (x₀ z₀ : Point d) : ℝ

The supplied nondegenerate secant scale.

Equations

• O3.secantScale p q grad x₀ z₀ = O3.lpNorm q (grad z₀ - grad x₀) / O3.lpNorm p (z₀ - x₀)

theorem O3.secantScale_pos {d : ℕ} {p q : ℝ} {grad : Point d → Point d} {x₀ z₀ : Point d} (hx : z₀ ≠ x₀) (hg : grad z₀ ≠ grad x₀) : 0 < secantScale p q grad x₀ z₀

theorem O3.secantScale_le {d : ℕ} {p q L : ℝ} {grad : Point d → Point d} (hLip : LipschitzGradient p q L grad) {x₀ z₀ : Point d} (hx : z₀ ≠ x₀) : secantScale p q grad x₀ z₀ ≤ L

The secant witness automatically gives the lower scale M₀ ≤ L.

def O3.FirstOrderConvex {d : ℕ} (f : Point d → ℝ) (grad : Point d → Point d) : Prop

A first-order convexity inequality, kept explicit so that no ambient Euclidean norm silently replaces the frozen ell_p geometry.

Equations

• O3.FirstOrderConvex f grad = ∀ (x y : O3.Point d), f x + O3.pairing (grad x) (y - x) ≤ f y

def O3.AnchorTest {d : ℕ} (f : Point d → ℝ) (x₀ : Point d) (G D : ℝ) (y : Point d) : Prop

The observable anchor test at distance D.

Equations

• O3.AnchorTest f x₀ G D y = (f y ≤ f x₀ - G * D / 2)

theorem O3.anchorAccepted_radius {d : ℕ} {p : ℝ} (hp : 1 < p) {f : Point d → ℝ} {grad : Point d → Point d} (hconv : FirstOrderConvex f grad) {x₀ xstar y : Point d} {G D R : ℝ} (hmin : ∀ (x : Point d), f xstar ≤ f x) (hG : G = lpNorm (conjugateExponent p) (grad x₀)) (hGpos : 0 < G) (hR : lpNorm p (xstar - x₀) ≤ R) (haccept : AnchorTest f x₀ G D y) : D ≤ 2 * R

The accepted anchor test and first-order convexity imply the exact radius certificate D ≤ 2R. No optimizer or radius is supplied to the algorithm; they occur only in this correctness proof.

noncomputable def O3.anchorNormingVector {d : ℕ} (q : ℝ) (g : Vec d) : Vec d

The explicit coordinate norming direction used by the frozen anchor.

Equations

• O3.anchorNormingVector q g i = ↑(SignType.sign (g i)) * |g i| ^ (q - 1) / O3.lpNorm q g ^ (q - 1)

noncomputable def O3.anchorScale (M₀ : ℝ) (epoch : ℕ) : ℝ

Dyadic curvature scale 2^epoch M₀.

Equations

• O3.anchorScale M₀ epoch = 2 ^ epoch * M₀

noncomputable def O3.anchorRadius (G M₀ : ℝ) (epoch : ℕ) : ℝ

Exact radius tested at one dyadic scale.

Equations

• O3.anchorRadius G M₀ epoch = G / O3.anchorScale M₀ epoch

noncomputable def O3.anchorProbePoint {d : ℕ} (q : ℝ) (x₀ g₀ : Vec d) (G M₀ : ℝ) (epoch : ℕ) : Vec d

Exact gradient-ray point queried at one dyadic scale.

Equations

• O3.anchorProbePoint q x₀ g₀ G M₀ epoch = x₀ - O3.anchorRadius G M₀ epoch • O3.anchorNormingVector q g₀

structure O3.AnchorConfig (d : ℕ) : Type

Inputs already available after the counted query at x₀.

• q : ℝ

  The exponent used to normalize the anchor search direction.

• x₀ : Vec d

  The initial point from which anchor probes are taken.

• f₀ : ℝ

  The observed objective value at the initial point.

• g₀ : Vec d

  The observed gradient at the initial point.

• G : ℝ

  The initial gradient size used to set probe radii.

• M₀ : ℝ

  The initial scale estimate for the dyadic anchor search.

structure O3.AnchorResult (d : ℕ) : Type

Data returned by the first accepted probe; no correctness claim is a field.

• epoch : ℕ

  The dyadic epoch at which the anchor probe was accepted.

• acceptedScale : ℝ

  The scale estimate associated with the accepted anchor probe.

• acceptedRadius : ℝ

  The radius associated with the accepted anchor probe.

• acceptedPoint : Vec d

  The point returned by the accepted anchor probe.

• observations : OracleTrace d

  All pair-oracle responses collected during the anchor search.

noncomputable def O3.runAnchor {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) : ℕ → ℕ → OracleTrace d → Option (AnchorResult d)

The actual fuel-bounded dyadic anchor loop. Every iteration makes exactly one pair-oracle query, tests its returned value, and either stops or doubles the scale by incrementing epoch.

Equations

• One or more equations did not get rendered due to their size.
• O3.runAnchor oracle cfg 0 x✝¹ x✝ = none

theorem O3.anchorScale_succ (M₀ : ℝ) (epoch : ℕ) : anchorScale M₀ (epoch + 1) = 2 * anchorScale M₀ epoch

theorem O3.anchorScale_mono {M₀ : ℝ} (hM₀ : 0 ≤ M₀) {i j : ℕ} (hij : i ≤ j) : anchorScale M₀ i ≤ anchorScale M₀ j

theorem O3.exists_anchor_scale_ge {M₀ L : ℝ} (hM₀ : 0 < M₀) : ∃ (epoch : ℕ), L ≤ anchorScale M₀ epoch

noncomputable def O3.anchorScaleCap (M₀ L : ℝ) (hM₀ : 0 < M₀) : ℕ

First dyadic scale which dominates L; this is proof-side, not method input.

Equations

• O3.anchorScaleCap M₀ L hM₀ = Nat.find ⋯

theorem O3.anchorScaleCap_dominates {M₀ L : ℝ} (hM₀ : 0 < M₀) : L ≤ anchorScale M₀ (anchorScaleCap M₀ L hM₀)

theorem O3.anchorScaleCap_lt_two_mul {M₀ L : ℝ} (hM₀ : 0 < M₀) (hM₀L : M₀ ≤ L) : anchorScale M₀ (anchorScaleCap M₀ L hM₀) < 2 * L

theorem O3.runAnchor_acceptsBy {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) (start extra : ℕ) (history : OracleTrace d) (hpass : have epoch := start + extra; have D := anchorRadius cfg.G cfg.M₀ epoch; have y := anchorProbePoint cfg.q cfg.x₀ cfg.g₀ cfg.G cfg.M₀ epoch; oracle.value y ≤ cfg.f₀ - cfg.G * D / 2) : ∃ (result : AnchorResult d), runAnchor oracle cfg (extra + 1) start history = some result

If a specified later probe passes, the deterministic loop succeeds no later.

theorem O3.runAnchor_result_valid {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) {fuel start : ℕ} {history : OracleTrace d} {result : AnchorResult d} (hrun : runAnchor oracle cfg fuel start history = some result) : result.acceptedScale = anchorScale cfg.M₀ result.epoch ∧ result.acceptedRadius = anchorRadius cfg.G cfg.M₀ result.epoch ∧ result.acceptedPoint = anchorProbePoint cfg.q cfg.x₀ cfg.g₀ cfg.G cfg.M₀ result.epoch ∧ oracle.value result.acceptedPoint ≤ cfg.f₀ - cfg.G * result.acceptedRadius / 2

Any successful loop result records the accepted test and exact dyadic data.

theorem O3.runAnchor_traceExact {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) {fuel start : ℕ} {history : OracleTrace d} {result : AnchorResult d} (hhistory : TraceExact oracle history) (hrun : runAnchor oracle cfg fuel start history = some result) : TraceExact oracle result.observations

Successful execution records only exact oracle observations.

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

theorem O3.runAnchor_callCount_le {d : ℕ} (oracle : PairOracle d) (cfg : AnchorConfig d) {fuel start : ℕ} {history : OracleTrace d} {result : AnchorResult d} (hrun : runAnchor oracle cfg fuel start history = some result) : List.length result.observations ≤ List.length history + fuel

theorem O3.anchor_of_cap_acceptance {d : ℕ} {p L R : ℝ} (hp : 1 < p) (oracle : PairOracle d) (cfg : AnchorConfig d) (hM₀ : 0 < cfg.M₀) (hM₀L : cfg.M₀ ≤ L) (hbase : cfg.f₀ = oracle.value cfg.x₀) (hconv : FirstOrderConvex oracle.value oracle.gradient) (xstar : Vec d) (hmin : ∀ (x : Vec d), oracle.value xstar ≤ oracle.value x) (hG : cfg.G = lpNorm (conjugateExponent p) (oracle.gradient cfg.x₀)) (hGpos : 0 < cfg.G) (hR : lpNorm p (xstar - cfg.x₀) ≤ R) (hcapPass : have cap := anchorScaleCap cfg.M₀ L hM₀; have D := anchorRadius cfg.G cfg.M₀ cap; have y := anchorProbePoint cfg.q cfg.x₀ cfg.g₀ cfg.G cfg.M₀ cap; oracle.value y ≤ cfg.f₀ - cfg.G * D / 2) : ∃ (result : AnchorResult d), runAnchor oracle cfg (anchorScaleCap cfg.M₀ L hM₀ + 1) 0 [] = some result ∧ result.acceptedScale < 2 * L ∧ result.acceptedRadius ≤ 2 * R ∧ List.length result.observations ≤ anchorScaleCap cfg.M₀ L hM₀ + 1 ∧ TraceExact oracle result.observations

Everything in the anchor conclusion after the analytic descent implication: the concrete loop terminates, uses at most cap+1 probes, returns exact data, and satisfies both scale and radius certificates.