Stage 9: exact finite-data OGM-G algebraic certificate

This file isolates the algebraic heart of the finite-data OGM-G argument. The main result below is horizon-generic: it expands the two certificate sums, proves that every function-value coefficient telescopes to psi 0, and reduces the remaining equality to the exact signed inner-product balance.

The final section contains a literal source-recurrence audit at n = 1, explicit coefficient-theorem specializations at n = 2, 3, and separate endpoint audits at all three horizons. They are theorem statements rather than floating-point examples: all coefficients remain symbolic and the special equation theta_0^2-theta_0=2 theta_1^2 is used exactly. The actual vector recurrence supplies the pairing-balance premise in Stage9Pairing.

noncomputable def O3.Stage9Certificate.ogmgPsi (M fstar : ℝ) (fval gradSq : ℕ → ℝ) (i : ℕ) : ℝ

The source quantity psi_i = f_i - f^* - ||g_i||^2/(2M). The squared gradient is an explicit scalar input so that the coefficient algebra is independent of a particular vector representation.

Equations

• O3.Stage9Certificate.ogmgPsi M fstar fval gradSq i = fval i - fstar - gradSq i / (2 * M)

def O3.Stage9Certificate.ogmgI (psi : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) (i j : ℕ) : ℝ

The source interpolation remainder I_ij = psi_i - psi_j - <g_j,v_i-v_j>.

Equations

• O3.Stage9Certificate.ogmgI psi pairTerm i j = psi i - psi j - pairTerm i j

def O3.Stage9Certificate.ogmgDelta (kappa : ℕ → ℝ) (i : ℕ) : ℝ

delta_i = kappa_(i+1) - kappa_i.

Equations

• O3.Stage9Certificate.ogmgDelta kappa i = kappa (i + 1) - kappa i

def O3.Stage9Certificate.ogmgCertificateRhs (n : ℕ) (kappa psi : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) : ℝ

The literal right side of the frozen OGM-G certificate.

Equations

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

def O3.Stage9Certificate.ogmgPairingAggregate (n : ℕ) (kappa : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) : ℝ

The unsigned collection of pairing terms subtracted by the certificate.

Equations

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

theorem O3.Stage9Certificate.ogmg_value_coefficients_telescope (n : ℕ) (kappa psi : ℕ → ℝ) (hkappa0 : kappa 0 = 1) : ∑ i ∈ Finset.range n, kappa (i + 1) * (psi i - psi (i + 1)) + ∑ i ∈ Finset.range n, ogmgDelta kappa i * (psi n - psi i) + psi n = psi 0

Exact telescoping of the function-value coefficients. No monotonicity or theta equation is needed: only the source normalization kappa_0 = 1.

theorem O3.Stage9Certificate.ogmgCertificateRhs_eq (n : ℕ) (kappa psi : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) (hkappa0 : kappa 0 = 1) : ogmgCertificateRhs n kappa psi pairTerm = psi 0 - ogmgPairingAggregate n kappa pairTerm

Fully expanded arbitrary-horizon certificate: the value coefficients collapse exactly, leaving only the two signed pairing sums.

theorem O3.Stage9Certificate.ogmgCertificate_identity_of_pairing_balance (n : ℕ) (M theta0 fstar : ℝ) (fval gradSq kappa : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) (hM : M ≠ 0) (hkappa0 : kappa 0 = 1) (hpair : ogmgPairingAggregate n kappa pairTerm = (theta0 ^ 2 * gradSq n - gradSq 0) / (2 * M)) : fval 0 - fstar - theta0 ^ 2 / (2 * M) * gradSq n = ogmgCertificateRhs n kappa (ogmgPsi M fstar fval gradSq) pairTerm

The exact source identity follows once the OGM-G recurrence supplies its quadratic pairing balance. This lemma is the interface between the actual iterate proof and the coefficient certificate; the balance is not stored in the final finite-data statement.

theorem O3.Stage9Certificate.weighted_terminal_displacement (n : ℕ) (w v : ℕ → ℝ) : ∑ i ∈ Finset.range n, w i * (v n - v i) = ∑ k ∈ Finset.range n, (∑ i ∈ Finset.range (k + 1), w i) * (v (k + 1) - v k)

Discrete change-of-order identity behind the second pairing sum.

noncomputable def O3.Stage9Certificate.scalarOgmgNext (theta thetaNext u v vPrev : ℝ) : ℝ

The source scalar OGM-G recurrence, used only for the independent small-horizon coefficient audits below.

Equations

• O3.Stage9Certificate.scalarOgmgNext theta thetaNext u v vPrev = v + (theta - 1) * (2 * thetaNext - 1) / (theta * (2 * theta - 1)) * (v - vPrev) + (2 * thetaNext - 1) / (2 * theta - 1) * (v - u)

def O3.Stage9Certificate.auditTwo (x0 x1 : ℝ) : ℕ → ℝ

A scalar sequence supported at indices zero and one for the one-step certificate audit.

Equations

• O3.Stage9Certificate.auditTwo x0 x1 0 = x0
• O3.Stage9Certificate.auditTwo x0 x1 1 = x1
• O3.Stage9Certificate.auditTwo x0 x1 x✝ = 0

theorem O3.Stage9Certificate.ogmg_certificate_audit_n1 (M U fstar f0 f1 g0 g1 : ℝ) (hM : M ≠ 0) : have theta := stage9Theta 1; have kappa := stage9Kappa 1; have v0 := U - g0 / M; have u1 := scalarOgmgNext (theta 0) (theta 1) U v0 U; have v1 := u1 - g1 / M; have fval := auditTwo f0 f1; have grad := auditTwo g0 g1; have vel := auditTwo v0 v1; have gradSq := fun (i : ℕ) => grad i ^ 2; have pairTerm := fun (i j : ℕ) => grad j * (vel i - vel j); f0 - fstar - theta 0 ^ 2 / (2 * M) * g1 ^ 2 = ogmgCertificateRhs 1 kappa (ogmgPsi M fstar fval gradSq) pairTerm

Independent exact audit at the smallest legal horizon. This unfolds the literal source recurrence with v_{-1}=U, the terminal v_1, and the special theta equation; no convergence theorem is used.

noncomputable def O3.Stage9Certificate.auditP (n : ℕ) (g : ℕ → ℝ) : ℕ → ℝ

The p-sequence used in the TeX verification, specialized to the exact source theta array.

Equations

• O3.Stage9Certificate.auditP n g 0 = 0
• O3.Stage9Certificate.auditP n g k.succ = (1 - 1 / O3.stage9Theta n k) * O3.Stage9Certificate.auditP n g k + 1 / O3.stage9Theta n k * g k

theorem O3.Stage9Certificate.auditP_terminal {n : ℕ} (hn : 1 ≤ n) (g : ℕ → ℝ) : auditP n g (n + 1) = g n

The endpoint p_(n+1)=g_n is derived from theta_n=1; it is not an extra certificate input.

theorem O3.Stage9Certificate.ogmg_endpoint_audit_n1 (g : ℕ → ℝ) : stage9Theta 1 1 = 1 ∧ stage9Theta 1 0 ^ 2 - stage9Theta 1 0 = 2 * stage9Theta 1 1 ^ 2 ∧ auditP 1 g 2 = g 1

Exact source endpoint audit at n=1.

theorem O3.Stage9Certificate.ogmg_endpoint_audit_n2 (g : ℕ → ℝ) : stage9Theta 2 2 = 1 ∧ stage9Theta 2 0 ^ 2 - stage9Theta 2 0 = 2 * stage9Theta 2 1 ^ 2 ∧ stage9Theta 2 1 ^ 2 - stage9Theta 2 1 = stage9Theta 2 2 ^ 2 ∧ auditP 2 g 3 = g 2

Exact source endpoint and ordinary-coefficient audit at n=2.

theorem O3.Stage9Certificate.ogmg_endpoint_audit_n3 (g : ℕ → ℝ) : stage9Theta 3 3 = 1 ∧ stage9Theta 3 0 ^ 2 - stage9Theta 3 0 = 2 * stage9Theta 3 1 ^ 2 ∧ stage9Theta 3 1 ^ 2 - stage9Theta 3 1 = stage9Theta 3 2 ^ 2 ∧ stage9Theta 3 2 ^ 2 - stage9Theta 3 2 = stage9Theta 3 3 ^ 2 ∧ auditP 3 g 4 = g 3

Exact source endpoint and both ordinary-coefficient audits at n=3.

theorem O3.Stage9Certificate.ogmg_certificate_coefficients_audit_n2 (M fstar : ℝ) (fval gradSq : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) (hM : M ≠ 0) (hpair : ogmgPairingAggregate 2 (stage9Kappa 2) pairTerm = (stage9Theta 2 0 ^ 2 * gradSq 2 - gradSq 0) / (2 * M)) : fval 0 - fstar - stage9Theta 2 0 ^ 2 / (2 * M) * gradSq 2 = ogmgCertificateRhs 2 (stage9Kappa 2) (ogmgPsi M fstar fval gradSq) pairTerm

Explicit horizon-2 specialization of the native arbitrary-horizon coefficient theorem. The execution audit supplies the exact pairing balance after expanding the two literal source recurrence steps.

theorem O3.Stage9Certificate.ogmg_certificate_coefficients_audit_n3 (M fstar : ℝ) (fval gradSq : ℕ → ℝ) (pairTerm : ℕ → ℕ → ℝ) (hM : M ≠ 0) (hpair : ogmgPairingAggregate 3 (stage9Kappa 3) pairTerm = (stage9Theta 3 0 ^ 2 * gradSq 3 - gradSq 0) / (2 * M)) : fval 0 - fstar - stage9Theta 3 0 ^ 2 / (2 * M) * gradSq 3 = ogmgCertificateRhs 3 (stage9Kappa 3) (ogmgPsi M fstar fval gradSq) pairTerm

Explicit horizon-3 specialization of the native arbitrary-horizon coefficient theorem.