6.11.1. ODE Enclosures🔗

An ODE enclosure certificate is a finite description of a corridor around a trajectory. The checker does not need to trust an external integrator's narrative. It parses the ODE expression, evaluates interval bounds over each segment, and checks that the claimed tube is closed under the vector field with the required margins.

The executable side is exposed through the ODE checker API. The core pieces are the expression AST, the interval evaluator, the segment certificate, and the final checker result.

The theorem side is the real mathematical statement. In the ODE enclosure API, a corridor theorem says, in plain language:

If the initial state lies in the first set, and each segment satisfies the enclosure condition for

the ODE vector field, then the true solution remains inside the certified corridor for the

covered time interval.

The backend bridge in ODE enclosure backends explains how backend valued trajectories, including FP32 and IEEE32Exec views, can be related back to the real statement through explicit interpretation maps.

Lean has a local enclosure theorem, and the executable checker puts imported ODE or PINN artifacts into the shape that theorem expects. This does not prove every neural ODE or every external integrator correct.

6.11.2. PINN Certificates🔗

PINN verification is more than "run the neural network." The artifact has at least four claims:

1. the imported parameters match the architecture;

2. the PDE expression is the one being checked;

3. the residual is bounded over the domain;

4. boundary or dataset constraints are respected.

TorchLean gives each piece a small object. The PINN architecture API names sequential network records and graph construction. The PDE expression API names the PDE language. The PyTorch parameter store API names imported parameters instead of letting a raw tensor dictionary float around unchecked. The residual affine API contains the bound helpers, including McCormick style pieces and branch and bound support.

The certificate level combines the architecture, imported parameters, PDE expression, and domain boxes, then checks residual bounds and produces an accepted certificate with a theorem-ready residual proposition.

The PINN certificate API, the dataset checker API, and the PINN command API are the user surfaces for that path.

PINNs are a good stress test because the model is only part of the claim. The PDE residual, the domain, the boundary data, and the imported parameters all matter. TorchLean's design makes those pieces explicit in the certificate object.

6.11.3. Piecewise Polynomial and Spline Certificates🔗

The spline path is concentrated in NN.Verification.Splines.PiecewisePolyCert API. It parses piecewise_poly_v0 JSON, checks rational polynomial pieces, evaluates polynomials by Horner's rule, and also has an IEEE32Exec exact conversion path.

This is one of the cleanest examples of the external tool philosophy:

1. another system may generate a piecewise polynomial artifact;

2. the artifact is serialized into a small explicit certificate format;

3. Lean parses and checks that format;

4. any remaining trust boundary is named instead of hidden.

6.11.4. Scientific Artifacts In The Same Trust Story🔗

Scientific ML often lives at the boundary between theorem proving and numerical tooling. TorchLean's verification layer includes ODEs, PINNs, and splines alongside image classifiers and language models. These sections give readers a clear place to start when their question is:

How do I bring a scientific artifact into Lean without treating the external producer as

already verified?

The answer is the same pattern we use elsewhere: small certificate formats, explicit parsers, checked predicates, and theorem statements that say exactly which mathematical claim follows.