Euclidean-chain arithmetic and oracle accounting

This module closes scalar recurrences and exact finite-query accounting that are independent of the guarded estimate-sequence and finite-data OGM-G vector identities. It deliberately does not turn either load-bearing identity into a certificate field.

noncomputable def O3.euclideanWeight (A : ℝ) : ℝ

The positive quadratic root used to update the Euclidean acceleration weight.

Equations

• O3.euclideanWeight A = (1 + √(1 + 4 * A)) / 2

theorem O3.euclideanWeight_pos {A : ℝ} (hA : 0 ≤ A) : 0 < euclideanWeight A

theorem O3.euclideanWeight_equation {A : ℝ} (hA : 0 ≤ A) : euclideanWeight A ^ 2 = A + euclideanWeight A

noncomputable def O3.thetaStep (t : ℝ) : ℝ

The standard accelerated theta update with discriminant 1 + 4 t².

Equations

• O3.thetaStep t = (1 + √(1 + 4 * t ^ 2)) / 2

noncomputable def O3.thetaZeroStep (t : ℝ) : ℝ

The modified terminal theta update with discriminant 1 + 8 t².

Equations

• O3.thetaZeroStep t = (1 + √(1 + 8 * t ^ 2)) / 2

theorem O3.thetaStep_pos (t : ℝ) : 0 < thetaStep t

theorem O3.thetaStep_equation (t : ℝ) : thetaStep t ^ 2 - thetaStep t = t ^ 2

theorem O3.thetaZeroStep_equation (t : ℝ) : thetaZeroStep t ^ 2 - thetaZeroStep t = 2 * t ^ 2

theorem O3.thetaStep_ge_add_half {t : ℝ} (ht : 0 ≤ t) : t + 1 / 2 ≤ thetaStep t

noncomputable def O3.ogmgTheta (n : ℕ) : Fin (n + 1) → ℝ

Backward OGM-G coefficients with the special doubled first equation.

Equations

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

noncomputable def O3.ogmgThetaTail : ℕ → ℝ

The ordinary backward tail theta_n=1, iterated away from the endpoint.

Equations

• O3.ogmgThetaTail 0 = 1
• O3.ogmgThetaTail k.succ = O3.thetaStep (O3.ogmgThetaTail k)

theorem O3.ogmgThetaTail_pos (k : ℕ) : 0 < ogmgThetaTail k

theorem O3.ogmgThetaTail_ge (k : ℕ) : 1 + ↑k / 2 ≤ ogmgThetaTail k

noncomputable def O3.ogmgThetaZero (n : ℕ) : ℝ

The special doubled first coefficient of the OGM-G certificate.

Equations

• O3.ogmgThetaZero n = O3.thetaZeroStep (O3.ogmgThetaTail (n - 1))

theorem O3.thetaZeroStep_ge_sqrtTwo_mul {t : ℝ} (_ht : 0 ≤ t) : √2 * t ≤ thetaZeroStep t

theorem O3.ogmgThetaZero_ge {n : ℕ} (hn : 1 ≤ n) : (↑n + 1) / √2 ≤ ogmgThetaZero n

The exact lower bound theta_0 >= (n+1)/sqrt 2.

def O3.euclideanTrialCallBudget (m n : ℕ) : ℕ

Exact number of pair calls in the source's Euclidean trial: Phase A makes at most two calls per iteration, Phase B reuses U, makes n further iterate queries, and makes one terminal descent query.

Equations

• O3.euclideanTrialCallBudget m n = 2 * m + n + 1

theorem O3.euclideanTrialCallBudget_diagonal (n : ℕ) : euclideanTrialCallBudget n n = 3 * n + 1

noncomputable def O3.euclideanHorizon (kappa : ℝ) : ℕ

The source horizon ceil (2 sqrt (M D / eps)).

Equations

• O3.euclideanHorizon kappa = ⌈2 * √kappa⌉₊

theorem O3.euclideanHorizon_real_le {kappa : ℝ} : ↑(euclideanHorizon kappa) ≤ 2 * √kappa + 1

theorem O3.euclideanTrialCallBudget_horizon {kappa : ℝ} (hkappa : 1 ≤ kappa) : ↑(euclideanTrialCallBudget (euclideanHorizon kappa) (euclideanHorizon kappa)) ≤ 10 * √kappa

Universal concrete call constant for the diagonal Euclidean horizon.

def O3.euclideanPhaseTrace {d m : ℕ} (oracle : PairOracle d) (y accelerated : Fin m → Vec d) : OracleTrace d

The two Phase-A oracle calls at each iteration, in chronological order.

Equations

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

theorem O3.euclideanPhaseTrace_exact {d m : ℕ} (oracle : PairOracle d) (y accelerated : Fin m → Vec d) : TraceExact oracle (euclideanPhaseTrace oracle y accelerated)

@[simp]

theorem O3.euclideanPhaseTrace_length {d m : ℕ} (oracle : PairOracle d) (y accelerated : Fin m → Vec d) : List.length (euclideanPhaseTrace oracle y accelerated) = 2 * m

def O3.finiteDataOGMGTrace {d n : ℕ} (oracle : PairOracle d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : OracleTrace d

Phase B reuses U; this trace therefore contains only the n newly queried iterates u_1,...,u_n and the additional terminal query at v_n.

Equations

• O3.finiteDataOGMGTrace oracle newIterates terminalDescent = List.map (fun (i : Fin n) => oracle.observe (newIterates i)) (List.finRange n) ++ [oracle.observe terminalDescent]

theorem O3.finiteDataOGMGTrace_exact {d n : ℕ} (oracle : PairOracle d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : TraceExact oracle (finiteDataOGMGTrace oracle newIterates terminalDescent)

@[simp]

theorem O3.finiteDataOGMGTrace_length {d n : ℕ} (oracle : PairOracle d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : List.length (finiteDataOGMGTrace oracle newIterates terminalDescent) = n + 1

def O3.euclideanTrialTrace {d m n : ℕ} (oracle : PairOracle d) (y accelerated : Fin m → Vec d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : OracleTrace d

Full Euclidean local-trial trace with no double-counting of the reused U.

Equations

• O3.euclideanTrialTrace oracle y accelerated newIterates terminalDescent = O3.euclideanPhaseTrace oracle y accelerated ++ O3.finiteDataOGMGTrace oracle newIterates terminalDescent

theorem O3.euclideanTrialTrace_exact {d m n : ℕ} (oracle : PairOracle d) (y accelerated : Fin m → Vec d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : TraceExact oracle (euclideanTrialTrace oracle y accelerated newIterates terminalDescent)

@[simp]

theorem O3.euclideanTrialTrace_length {d m n : ℕ} (oracle : PairOracle d) (y accelerated : Fin m → Vec d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : List.length (euclideanTrialTrace oracle y accelerated newIterates terminalDescent) = euclideanTrialCallBudget m n

theorem O3.finiteDataOGMGTrace_final_iterate_queried {d n : ℕ} (hn : 1 ≤ n) (oracle : PairOracle d) (newIterates : Fin n → Vec d) (terminalDescent : Vec d) : WasQueried (finiteDataOGMGTrace oracle newIterates terminalDescent) (newIterates ⟨n - 1, ⋯⟩)

noncomputable def O3.EuclideanGapScalarStatement : Prop

Scalar denominator step used at the end of the guarded Euclidean-gap proof.

Equations

• O3.EuclideanGapScalarStatement = ∀ (M D fGap A : ℝ) (m : ℕ), 0 < M → 0 ≤ D → 1 ≤ m → A ≥ (↑m + 1) ^ 2 / 4 → fGap ≤ M * D ^ 2 / (2 * A) → fGap ≤ 2 * M * D ^ 2 / (↑m + 1) ^ 2

theorem O3.euclideanGap_scalar : EuclideanGapScalarStatement