stochastic-latent-bounds

API map

module	role
`sbounds.systems`	Analytic N-link arm under gravity‑compensated PD with velocity‑block process noise; exact Ito push‑forward of the physical SDE (the ground truth used for scoring, never for certification).
`sbounds.transport`	Invertible affine‑coupling transport `T` with `T(x*)=0`; sound interval enclosures of `T`, `T⁻¹` and the interval Jacobian `J T`.
`sbounds.models`	`LyapunovNet` (positive‑definite by construction) and `LatentDynamics` with `F(0)=0` enforced structurally; Lyapunov metric for the ρ block; spectral‑norm projection.
`sbounds.nets`	Interval arithmetic, IBP and interval forward‑mode AD (ternary jets) with outward rounding.
`sbounds.bounds`	Sound bounds on `L W + α W`: tight interval Ito trace `½ tr(BBᴹ Hess W)` and the C‑S baseline; full‑space and factorised certification modes.
`sbounds.region`	Region definitions, bound factories, and BnB entry points with the `β+tol` threshold.
`sbounds.bnb`	Worst‑first branch‑and‑bound with explicit node/time budgets; certified fraction is a one‑sided lower bound.
`sbounds.generator`	Exact (autograd) latent generator and the noise floor `β = L W(0)`; evaluation only.
`sbounds.train`	Data generation (Euler‑Maruyama), joint transport+drift training, certificate training on exact‑generator violations.
`sbounds.cegis`	Counterexample search that separates genuine violations from bound looseness; verifier‑in‑the‑loop retraining against model or exact‑plant oracle.
`sbounds.shadow`	Dual‑buffer shadow networks with a certified acceptance gate; counts unsafe swaps against the exact plant generator.

The certificate, precisely

dy = F(y) dt + B(y) dW, B = J T(x) Σ(x), y = T(x) W(y) = V(η) + κ ρᴹ Q ρ, Q: AᵣᵣᴹQ + Q Aᵣᵣ = −I L W(y) = ∇W·F(y) + ½ tr( B Bᴹ Hess W ) claim: supᵢᴸ (L W + α W) ≤ β + tol, β = L W(0) => E[W(t)] ≤ e⁻⁷t W₀ + ((β+tol)/α)(1 − e⁻⁷t)

The interval trace is sound because every elementwise product of intervals contains the true product and sums of intervals contain the true sum; it is tight because both properties become equalities on degenerate (point) boxes, so the bound converges to the exact generator under refinement. The Cauchy‑Schwarz form ½||B||ᵣ²||Hess W||ᵣ is also sound but its slack is bounded away from zero near the origin, which is why it certifies nothing there.

The drift terms use centered (mean‑value) forms: the residual is evaluated exactly at the box center and the deviation is bounded by a Jacobian enclosure whose entries are exact zeros (the factorised residual’s η‑rows do not read ρ) or Lipschitz balls (spectral‑norm products, capped during training). The remainder is quadratic in box radius, so subdivision converges; raw interval bound propagation is linear and certifies nothing at region scale.