Prove fast/spec equivalence for the multilinear Möbius transform #185
Description
Summary
Add a fast/spec equivalence layer for the multilinear Möbius transform by proving that the existing fast inverse transform agrees with the closed-form specification.
For v : Vector R (2 ^ n), expose a theorem identifying the iterative butterfly implementation with the Boolean-lattice Möbius inversion formula already encoded by lagrangeToMonoSpec.
Correctness target
Prove that for every v : Vector R (2 ^ n),
lagrangeToMono n v = lagrangeToMonoSpec v.
Package the proof through a dedicated multilinear equivalence module, keep the fast transform computable, and preserve the existing round-trip relationship with monoToLagrange.
Motivation
Contributes to Phase 2 multilinear correctness: turns the existing fast transform into a proof-backed surface rather than relying only on implementation-level invertibility lemmas.