The 1 < p < 2 branch: exact numerical recurrences and call ledger

This module contains the parts of the frozen below-two chain that do not rely on the still-open real-exponent squared-ell_p strong-convexity bridge. It uses the exact real exponent range, the source weights, and a chronological pair-oracle trace with two calls per accelerated iteration and one extraction call.

The public declarations O3.belowEstimate and O3.belowTrial are intentionally not asserted while O3.belowGeometry is unavailable: their TeX proofs use that result load-bearingly. No conditional replacement taking the desired strong-convexity conclusion as an extra hypothesis is introduced.

def O3.BelowTwoRegime (p : ℝ) : Prop

The genuine-real regime from TeX Section 4.

Equations

• O3.BelowTwoRegime p = (1 < p ∧ p < 2)

def O3.belowSigma (p : ℝ) : ℝ

The source parameter sigma = p - 1.

Equations

• O3.belowSigma p = p - 1

theorem O3.belowSigma_pos {p : ℝ} (hp : BelowTwoRegime p) : 0 < belowSigma p

theorem O3.belowSigma_lt_one {p : ℝ} (hp : BelowTwoRegime p) : belowSigma p < 1

noncomputable def O3.belowLambda (eps D : ℝ) : ℝ

The exact regularization parameter lambda = eps / (4 D).

Equations

• O3.belowLambda eps D = eps / (4 * D)

noncomputable def O3.belowRho (sigma eps : ℝ) : ℝ

The exact residual target rho = sigma eps / 32.

Equations

• O3.belowRho sigma eps = sigma * eps / 32

noncomputable def O3.belowQ (kappa sigma : ℝ) : ℝ

The exact source amplification factor Q = 4096 kappa^2 / sigma^4.

Equations

• O3.belowQ kappa sigma = 4096 * kappa ^ 2 / sigma ^ 4

theorem O3.belowLambda_pos {eps D : ℝ} (heps : 0 < eps) (hD : 0 < D) : 0 < belowLambda eps D

theorem O3.belowRho_pos {sigma eps : ℝ} (hsigma : 0 < sigma) (heps : 0 < eps) : 0 < belowRho sigma eps

theorem O3.one_lt_belowQ {kappa sigma : ℝ} (hkappa : 1 < kappa) (hsigma : 0 < sigma) (hsigma1 : sigma < 1) : 1 < belowQ kappa sigma

noncomputable def O3.belowTau (M lambda sigma : ℝ) : ℝ

The source contraction parameter, with no discretization of p.

Equations

• O3.belowTau M lambda sigma = 2 / (1 + √(1 + 4 * M / (lambda * sigma)))

theorem O3.belowTau_pos {M lambda sigma : ℝ} (hM : 0 < M) (hlambda : 0 < lambda) (hsigma : 0 < sigma) : 0 < belowTau M lambda sigma

theorem O3.belowTau_lt_one {M lambda sigma : ℝ} (hM : 0 < M) (hlambda : 0 < lambda) (hsigma : 0 < sigma) : belowTau M lambda sigma < 1

theorem O3.belowTau_equation {M lambda sigma : ℝ} (hM : 0 < M) (hlambda : 0 < lambda) (hsigma : 0 < sigma) : M * belowTau M lambda sigma ^ 2 = lambda * sigma * (1 - belowTau M lambda sigma)

The exact source identity M * tau^2 = lambda * sigma * (1 - tau).

noncomputable def O3.belowWeight (M tau : ℝ) : ℕ → ℝ

The accepted estimate-sequence weight A_N. This recursive definition is exactly A_0 = 0, A_1 = 1/M, and A_(k+1) = A_k/(1-tau) for k >= 1.

Equations

• O3.belowWeight M tau 0 = 0
• O3.belowWeight M tau n.succ = if n = 0 then 1 / M else O3.belowWeight M tau n / (1 - tau)

@[simp]

theorem O3.belowWeight_zero (M tau : ℝ) : belowWeight M tau 0 = 0

@[simp]

theorem O3.belowWeight_one (M tau : ℝ) : belowWeight M tau 1 = 1 / M

theorem O3.belowWeight_succ {M tau : ℝ} {k : ℕ} (hk : 1 ≤ k) : belowWeight M tau (k + 1) = belowWeight M tau k / (1 - tau)

theorem O3.belowWeight_pos {M tau : ℝ} (hM : 0 < M) (htau : tau < 1) {N : ℕ} : 1 ≤ N → 0 < belowWeight M tau N

theorem O3.belowWeight_eq {M tau : ℝ} (htau : tau ≠ 1) {N : ℕ} : 1 ≤ N → belowWeight M tau N = 1 / M / (1 - tau) ^ (N - 1)

Closed form A_N = M⁻¹ (1-tau)^(-(N-1)), written as division.

structure O3.BelowPhaseState (d : ℕ) : Type

One below-two accelerated iteration adds exactly its two pair responses.

• iteration : ℕ

  The number of primal iterations recorded in this phase.

• accelerated : Vec d

  The current accelerated primal point.

• estimateMinimizer : Vec d

  The current minimizer of the phase's estimate function.

• weight : ℝ

  The cumulative acceleration weight at the current iteration.

• queries : List (Observation d)

  The chronological oracle responses accumulated by this phase.

def O3.BelowPhaseState.callCount {d : ℕ} (state : BelowPhaseState d) : ℕ

The number of oracle responses recorded by the phase.

Equations

• state.callCount = state.queries.length

def O3.BelowPhaseState.recordIteration {d : ℕ} (state : BelowPhaseState d) (accelerated estimateMinimizer : Vec d) (weight : ℝ) (atY atAccelerated : Observation d) : BelowPhaseState d

Advance the phase state and append the two observations from one primal iteration.

Equations

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

theorem O3.BelowPhaseState.recordIteration_callCount {d : ℕ} (state : BelowPhaseState d) (accelerated estimateMinimizer : Vec d) (weight : ℝ) (atY atAccelerated : Observation d) : (state.recordIteration accelerated estimateMinimizer weight atY atAccelerated).callCount = state.callCount + 2

def O3.belowPhaseTrace {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) : List (Observation d)

Chronological exact trace of N two-query phase iterations.

Equations

• O3.belowPhaseTrace oracle y accelerated = List.flatMap (fun (i : Fin N) => [oracle.observe (y i), oracle.observe (accelerated i)]) (List.finRange N)

def O3.ObservationTraceExact {d : ℕ} (oracle : PairOracle d) (trace : List (Observation d)) : Prop

Every entry is the exact oracle response at its recorded query point.

Equations

• O3.ObservationTraceExact oracle trace = ∀ observation ∈ trace, observation = oracle.observe observation.point

theorem O3.belowPhaseTrace_exact {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) : ObservationTraceExact oracle (belowPhaseTrace oracle y accelerated)

@[simp]

theorem O3.belowPhaseTrace_length {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) : (belowPhaseTrace oracle y accelerated).length = 2 * N

def O3.belowTrialTrace {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) (extraction : Vec d) : List (Observation d)

The phase trace followed by the counted residual-extraction query.

Equations

• O3.belowTrialTrace oracle y accelerated extraction = O3.belowPhaseTrace oracle y accelerated ++ [oracle.observe extraction]

theorem O3.belowTrialTrace_callCount {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) (extraction : Vec d) : (belowTrialTrace oracle y accelerated extraction).length = 2 * N + 1

Exact local oracle accounting from TeX lines 751--752.

theorem O3.belowTrialTrace_exact {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) (extraction : Vec d) : ObservationTraceExact oracle (belowTrialTrace oracle y accelerated extraction)

theorem O3.belowTrialTrace_extraction_queried {d N : ℕ} (oracle : PairOracle d) (y accelerated : Fin N → Vec d) (extraction : Vec d) : extraction ∈ List.map Observation.point (belowTrialTrace oracle y accelerated extraction)

theorem O3.belowFinalScalarBudget {sigma eps D : ℝ} (hsigma : 0 < sigma) (hsigma1 : sigma < 1) (heps : 0 < eps) (hD : 0 < D) : belowLambda eps D * D + belowRho sigma eps + belowRho sigma eps / sigma < eps

The final scalar budget in TeX lines 729--737. It is kept independent of the unavailable vector strong-convexity step: once the three displayed scalar terms have been derived, their sum is strictly below eps.