Evidence categories and present status

We distinguish:

Analytical proof.

A theorem established by an explicit argument under stated hypotheses.

Source alignment.

A documented comparison with an identified implementation, including source locations and conventions.

Numerical regression.

Reproducible floating-point comparisons with predeclared tolerances.

Validated numerical certificate.

Outward-rounded enclosures and a finite error budget for a specified calculation.

Document construction.

Successful compilation, resolved references, and inspection of the PDF.

The theorem and proof environments below belong to the first category. A proved error-bound theorem is an interface for a numerical certificate; it is not evidence that its hypotheses have been numerically enclosed for a particular run.

The supplied verification plan reports that an originating simulator export was supplied as documentary material and describes its conventions. These reported correspondences are recorded in Appendix app:alignment. This revision does not include an archived, line-numbered copy of that export or a completed source-inspection record. Source alignment therefore remains to be independently established; it is not replaced by the assertion that code was unavailable, nor by an unsupported assertion that inspection passed.

No execution archive, compiler log, independent symbolic-check output, validated numerical certificate, or machine-checked proof accompanies this revision. The execution-dependent release gates in Appendix app:verification remain unverified.