Stage 9: quadratic pairing certificate

This module proves the pairing balance required by the finite-data certificate from the actual auxiliary recurrence. The balance is a theorem, not a field of the final statement.

noncomputable def O3.stage9PairTerm {d : ℕ} (g v : ℕ → Vec d) (i j : ℕ) : ℝ

The gradient at index j paired with the difference of the two indexed points.

Equations

• O3.stage9PairTerm g v i j = O3.pairing (g j) (v i - v j)

theorem O3.stage9_pairingAggregate_eq_edgeSum {d : ℕ} (n : ℕ) (kappa delta : ℕ → ℝ) (g v : ℕ → Vec d) (hdelta : ∀ (i : ℕ), delta i = Stage9Certificate.ogmgDelta kappa i) (hweighted : ∀ k ≤ n, stage9WeightedGradient delta g k = kappa k • stage9P (stage9Theta n) g k) : Stage9Certificate.ogmgPairingAggregate n kappa (stage9PairTerm g v) = ∑ k ∈ Finset.range n, kappa (k + 1) * pairing (stage9P (stage9Theta n) g (k + 1) - g (k + 1)) (v (k + 1) - v k)

The two pairing sums combine into one edge sum after discrete summation by parts and the exact weighted-gradient identity.

theorem O3.stage9_pairing_balance {d : ℕ} (n : ℕ) (hn : 1 ≤ n) (M : ℝ) (hM : M ≠ 0) (g v : ℕ → Vec d) (hvelocity : ∀ (k : ℕ), 1 ≤ k → k ≤ n → M • (v k - v (k - 1)) = -stage9Theta n k • (stage9P (stage9Theta n) g k + stage9P (stage9Theta n) g (k + 1))) : Stage9Certificate.ogmgPairingAggregate n (stage9Kappa n) (stage9PairTerm g v) = (stage9Theta n 0 ^ 2 * lpNorm 2 (g n) ^ 2 - lpNorm 2 (g 0) ^ 2) / (2 * M)

Native proof of the exact quadratic balance in the source certificate.