Stage 9: finite-data OGM-G terminal-gradient certificate

This module connects the source-exact execution and its observable guards to the native finite algebraic certificate. In particular, the certificate is proved from the actual recursion; it is not an input field or hypothesis.

noncomputable def O3.stage9ActualPsi {d : ℕ} (cfg : OGMGExecutionConfig d) (fstar : ℝ) (i : ℕ) : ℝ

The scalar OGM-G potential instantiated with an actual oracle execution.

Equations

• O3.stage9ActualPsi cfg fstar i = O3.Stage9Certificate.ogmgPsi cfg.M fstar (O3.ogmgFunctionValue cfg) (O3.ogmgGradientSq cfg) i

noncomputable def O3.stage9ActualI {d : ℕ} (cfg : OGMGExecutionConfig d) (fstar : ℝ) (i j : ℕ) : ℝ

The two-point interpolation certificate instantiated with an actual oracle execution.

Equations

• O3.stage9ActualI cfg fstar i j = O3.Stage9Certificate.ogmgI (O3.stage9ActualPsi cfg fstar) (O3.ogmgPairTerm cfg) i j

theorem O3.pairing_symm {d : ℕ} (x y : Vec d) : pairing x y = pairing y x

theorem O3.stage9ActualI_eq_interpolationMargin {d : ℕ} (cfg : OGMGExecutionConfig d) (fstar : ℝ) (hM : cfg.M ≠ 0) (i j : ℕ) : stage9ActualI cfg fstar i j = ogmgFunctionValue cfg i - ogmgFunctionValue cfg j - pairing (ogmgGradient cfg j) ((ogmgState cfg i).current - (ogmgState cfg j).current) - lpNorm 2 (ogmgGradient cfg i - ogmgGradient cfg j) ^ 2 / (2 * cfg.M)

The algebraic I_ij is exactly the observable interpolation margin.

theorem O3.stage9InterpolationCheck_iff_actualI_nonneg {d : ℕ} (cfg : OGMGExecutionConfig d) (fstar : ℝ) (hM : cfg.M ≠ 0) (i j : Fin (cfg.horizon + 1)) : (ogmgInterpolationCheck cfg i j).Holds ↔ 0 ≤ stage9ActualI cfg fstar ↑i ↑j

theorem O3.stage9ActualPsi_terminal_nonneg {d : ℕ} (cfg : OGMGExecutionConfig d) (fstar : ℝ) (hM : 0 < cfg.M) (hterminal : (ogmgTerminalDescentCheck cfg).Holds) (hlower : fstar ≤ (ogmgTerminalObservation cfg).value) : 0 ≤ stage9ActualPsi cfg fstar cfg.horizon

The terminal descent query and the proof-side lower bound imply psi_n ≥ 0 with the exact 1/(2M) coefficient.

theorem O3.stage9Actual_certificate_identity {d : ℕ} (n : ℕ) (hn : 1 ≤ n) (oracle : PairOracle d) (M : ℝ) (U : Vec d) (fstar : ℝ) (hM : M ≠ 0) : have cfg := stage9ExecutionConfig n oracle M U; ogmgFunctionValue cfg 0 - fstar - stage9Theta n 0 ^ 2 / (2 * M) * ogmgGradientSq cfg n = Stage9Certificate.ogmgCertificateRhs n (stage9Kappa n) (stage9ActualPsi cfg fstar) (ogmgPairTerm cfg)

The exact source identity instantiated by the actual oracle data and the actual recursive OGM-G execution.

theorem O3.stage9Actual_certificate_audit_n1 {d : ℕ} (oracle : PairOracle d) (M : ℝ) (U : Vec d) (fstar : ℝ) (hM : M ≠ 0) : have cfg := stage9ExecutionConfig 1 oracle M U; ogmgFunctionValue cfg 0 - fstar - stage9Theta 1 0 ^ 2 / (2 * M) * ogmgGradientSq cfg 1 = Stage9Certificate.ogmgCertificateRhs 1 (stage9Kappa 1) (stage9ActualPsi cfg fstar) (ogmgPairTerm cfg)

Exact actual-execution audit at horizon n=1.

theorem O3.stage9Actual_certificate_audit_n2 {d : ℕ} (oracle : PairOracle d) (M : ℝ) (U : Vec d) (fstar : ℝ) (hM : M ≠ 0) : have cfg := stage9ExecutionConfig 2 oracle M U; ogmgFunctionValue cfg 0 - fstar - stage9Theta 2 0 ^ 2 / (2 * M) * ogmgGradientSq cfg 2 = Stage9Certificate.ogmgCertificateRhs 2 (stage9Kappa 2) (stage9ActualPsi cfg fstar) (ogmgPairTerm cfg)

Exact actual-execution audit at horizon n=2.

theorem O3.stage9Actual_certificate_audit_n3 {d : ℕ} (oracle : PairOracle d) (M : ℝ) (U : Vec d) (fstar : ℝ) (hM : M ≠ 0) : have cfg := stage9ExecutionConfig 3 oracle M U; ogmgFunctionValue cfg 0 - fstar - stage9Theta 3 0 ^ 2 / (2 * M) * ogmgGradientSq cfg 3 = Stage9Certificate.ogmgCertificateRhs 3 (stage9Kappa 3) (stage9ActualPsi cfg fstar) (ogmgPairTerm cfg)

Exact actual-execution audit at horizon n=3.

def O3.FiniteDataOGMGStatement : Prop

Exact source-level proposition carrier. The oracle and all method data precede the proof-only lower bound; no certificate is supplied by the caller.

Equations

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

theorem O3.finiteDataOGMG : FiniteDataOGMGStatement

Native finite-data OGM-G terminal-gradient certificate.