Exact data, floating rendering, and formal coverage
On this page · Permalink · Source line 244
Three kinds of evidence support different parts of the guide. Exact Python data. The source verifier uses integers, rational fractions, and cyclotomic quotient-ring arithmetic. The release visualization script adds an independent rational-matrix implementation for all six shell products and completeness, component energy bookkeeping, the unsigned Fourier table, and the phase-family quarter-turn cases. The assertion counts and hashes are recorded in the accompanying verification results.
Floating diagnostics. Fourier matrix checks, lane assembly, phase curves, and figure coordinates use NumPy and Matplotlib. Their residuals are reported against an explicit \(10^{-12}\) tolerance. Passing that tolerance is numerical evidence, not exact arithmetic or an interval certificate.
Inherited Lean coverage. The later five-module source contains exact rational and cyclotomic calculations, normalized finite Fourier statements, and semantic transport into ordinary complex matrices and state vectors. The Lean guide maps the checked declarations and records the inherited certificate. This visual release does not claim a fresh Lean compilation.
The script is checks/make_visuals.py. Its final bounded-run manifest and scientific result are in verification/visual_release_run_v2/. Every scientific figure is supplied as PDF, SVG, and PNG. No image-generation model was used.