Proofs

This module collects the maintained proof API: tensor facts, selected autograd correctness theorems, runtime-approximation theorems, model proofs, and verification soundness results.

These are the proof modules included in the supported library, separate from tests, examples, and executable workflows.

Proof landmarks:

• real-analysis and numerics helper theorems: NN.Proofs.Analysis,
• analytic autograd correctness fragments: NN.Proofs.Autograd.FDeriv.*,
• tape/DAG reverse-mode correctness fragments: NN.Proofs.Autograd.Tape.*,
• backend selection and lossless contract grouping: NN.Proofs.Backend.*,
• model-level invariants: NN.Proofs.Models,
• probability-kernel facts: NN.Proofs.Probability,
• runtime-approximation bounds: NN.Proofs.RuntimeApprox.*,
• verification envelopes: NN.Proofs.Verification.

Backend proofs establish properties of the production Lean planner and its declared contracts. Successful plans respect the requested operations, registry, availability, and policy. Coalescing preserves node order, multiplicity, and complete capsules, so group acceptance applies to every original node. The numerical certificate consumer retains its selected capsule's reduction-policy guard. These proofs do not establish correctness of native kernels, numerical algorithms, or the FFI.

References:

• PyTorch autograd background: https://pytorch.org/docs/stable/autograd.html
• The theorem bundles re-exported here document the math/model references they rely on locally.