6. Verification and Certificates🔗

This chapter explains the verification and theorem layers of TorchLean. The word verification is used broadly here. Sometimes it means a bound propagation certificate for one graph and one input region. Sometimes it means a compiler theorem, an autograd correctness theorem, a finite precision approximation theorem, a learning theory predicate, or a scientific ML certificate.

The common pattern is that every claim has an object and a support. The object may be a graph, a parameter payload, a tensor program, a dataset, a trajectory, a residual, or an external JSON certificate. The support may be a Lean theorem, a small checker, a replayed artifact, a runtime diagnostic, or an explicitly named external producer.

This section has three kinds of pages. The first group explains verifier artifacts: IBP/CROWN bounds, certificates, two-stage workflows, ODE tubes, PINN residuals, and α,β-CROWN leaves. The second group explains proof infrastructure: compiler correctness, autograd soundness, runtime approximation, and reusable gradient/probability lemmas. The third group explains mathematical ML theory: differential privacy, stability, optimization, self-supervised objectives, universal approximation, Hopfield energy, and state-space causality.

The goal is to make those levels readable. A run is evidence about execution. A certificate is a finite artifact with a stated checker. A real-valued theorem needs a numerical bridge before it becomes a Float32 claim. When the right bridges are present, TorchLean can turn concrete artifacts into precise mathematical statements.