Formal Verification
Proven, not just tested.
A wavelet library is only as trustworthy as its reconstruction identity. FerroWave's mathematics is verified in layers — each doing what it can actually prove, with an explicit map of where each layer's reach ends. The transform identities are machine-checked in the Lean theorem prover; the transform-step rounding carries tight bounds in Gappa, re-checked by the Coq kernel. This is the assurance level of avionics and cryptography — applied to a signal-processing crate.
Perfect reconstruction, Parseval / energy preservation, orthonormality, MODWT, and EMD reconstruction — proven over the reals.
Every headline theorem reduces to propext, Classical.choice, and Quot.sound — the audit fails on any sorry or non-standard axiom.
Reconstruction, Parseval, and linearity hold at machine epsilon in the real f64 transform — orthonormal transforms don't accumulate roundoff.
The transform is an exact-coefficient dot product — no approximation error, only rounding. Haar ≤1 ulp, db2 ≤1.6 ulps, all tight.
The Layers
Verified in layers, each doing what it can prove
There is no single "verified" checkbox. Different claims need different machinery — and the honest version says so explicitly.
| Layer | What it establishes | On what | Strength |
|---|---|---|---|
| Proven (ℝ) | The wavelet mathematics is correct | An idealized ℝ model (Lean) | Lean-kernel-checked · minimal axioms · no sorry |
| Proven (structural) | Index / length / boundary logic is correct | The real shipping Rust (Aeneas) | Lean-kernel-checked |
| Measured (f64) | The proved laws hold in the shipping code | The real code, on a signal × wavelet grid | Validated to ~1e-16 |
| Bounded (f64) | The transform step rounds correctly | The real code (Gappa) | Rigorous · tight (~1 ulp) · Coq-checked |
What Each Layer Proves
From the reals down to the float
Proven over ℝ — the wavelet mathematics
formal/lean-math/ — 125 theorems in Lean + mathlib: perfect reconstruction IDWT(DWT(x)) = x one-level, whole-signal, and multilevel at any depth; Parseval / energy preservation at every level; the transform as a verified linear orthogonal map; the general orthonormal 2-tap bank (reconstruction and Parseval hold iff s² + t² = 1); filter orthonormality and vanishing moments; the MODWT; a Parseval frame (covering EWT); EMD reconstruction; the Mexican-hat ψ = −g″. The jump-prior laws sit on top: the cross-check relative gap is a bounded symmetric dissimilarity on [0, 1], zero iff the legs agree; the clamped QV − BV leg is part of a non-negative realized variance; the diffusion correction is a pure deflation; and relative intensity uncertainty is exactly 1/√N and antitone in N — the fabricated-confidence law, over ℝ.
Proven on the real Rust — structural index laws
The integer index / length / boundary law_* targets in ferro-wave/src/formal_model.rs are proved on the Aeneas-generated translation of the actual Rust— for example, "a periodic boundary index always lands back inside [0, n)." Index plumbing only; Aeneas has no floating-point model.
Measured in f64 — the proved laws, in the shipping code
ferro-wave/tests/formal_conformance.rs — over signals (random, sine, chirp, ramp, step, impulse) × orthonormal wavelets (Haar, db2, db4, db6), every proved law is checked in the real f64 transform and holds at machine epsilon: reconstruction (1-level / multilevel / MODWT) ~2e-16, Parseval 8e-16, linearity 2e-16, filter orthonormality ~1e-16.
Bounded in f64 — the transform step
Unlike a transcendental approximation, the wavelet transform is an exact-coefficient dot product — so it has no approximation error, only rounding, and the bounds are tight. formal/gappa/: the Haar DWT step ≤1 ulp, the db2 step ≤1.6 ulps, the CWT complex multiply ≤1 ulp. The Gappa proofs export to gappa -Bcoq for the Coq kernel to re-check.
The Honest Boundary
What we prove — and what we still trust
A tool that tells you the limits of its own guarantees is one you can trust with the parts it does guarantee. We publish the boundary in full.
Proven
The wavelet mathematics over ℝ, and the structural index logic on the real Rust. Lean-kernel-checked.
Measured
The proved laws hold in f64 at machine epsilon — the orthonormal transforms are well-conditioned, so roundoff does not accumulate.
Bounded
The transform-step rounding, tight to ~1 ulp, with a foundational Coq-kernel export of the Gappa proofs.
Still trusted
rustfft's FFT internals (external; classical O(log N · ε) bound), libm exp / sin / cos, and the iterative data-driven decompositions (EMD, CEEMDAN, EWT, VMD, SSWT). SIMD/FMA reassociation is out of scope.
Reproduce It
Re-check it yourself
The proofs aren't a marketing artifact — they are re-runnable. Every layer has a command.
# trusted-base audit — only the three standard axioms sh formal/lean-math/check-axioms.sh # DWT/CWT transform-step rounding bounds (Gappa) sh formal/gappa/run.sh # the proved laws, measured in f64 cargo test -p ferro-wave --test formal_conformance -- --nocapture # FFT accumulation + the CWT scale-band finding cargo test -p ferro-wave --test cwt_fft_accumulation -- --nocapture