normSq_eq_norm_sq
plain-language theorem explainer
For any complex number z, Mathlib's squared-modulus functional equals the square of the complex absolute value. Born-rule and Parseval arguments in the DFT-8 sector calculus cite this bridge constantly when switching between Complex.normSq and ‖·‖² notation. The proof is a three-rewrite wrapper: unfold the modulus, expand the square, and cancel the outer square-root via nonnegativity of the squared modulus.
Claim. For every $z \in \mathbb{C}$, the squared-modulus $\mathrm{N}(z) := (\mathrm{Re}\, z)^2 + (\mathrm{Im}\, z)^2$ equals $|z|^2$.
background
The ambient module forces the Born rule on eight-mode signals: the unique probability measure on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and calibrated to the two-branch exp(−C) rule is μ(S) = Σ_{k∈S} ‖ψ_k‖². By Parseval the same total appears in the DFT-8 frequency basis.
Mathlib writes the squared modulus of a complex number as Complex.normSq and the modulus itself as ‖z‖ := √(Complex.normSq z). Sector measures, inner products, and density matrices in this development mix the two spellings, so a one-line identification is needed before any algebraic simplification.
Upstream, several modules define their own squared-norm objects (finite amplitude vectors, Hilbert displays, planar carriers, metric quadratic forms). Those are separate carriers; the present lemma is purely about the complex scalar field that underlies Signal8 amplitudes.
proof idea
One-line rewrite wrapper. Unfold ‖z‖ via Complex.norm_def to √(Complex.normSq z), expand the outer square, then apply Real.mul_self_sqrt to the nonnegativity fact Complex.normSq_nonneg z, which cancels the square-root and yields Complex.normSq z on the right-hand side.
why it matters
Locally it unlocks the Parseval corollary dft_sector_total_eq (total sector measure is DFT-8 invariant) and the real-embedding identity norm_ofReal_sq used to normalise the two-branch cos/sin calibration. Downstream it is also invoked for phase-invariant pure-state densities, the no-cloning inner-product-self identity, and the two-qubit reduced-density determinant identity det(ρ₁) = ‖det A‖².
In the Recognition chain this sits under Born-rule forcing, which closes the measurement gap and depends on T5 (J-uniqueness), T7 (eight-tick octave), and T8 (D = 3). Without the normSq/‖·‖² bridge, sectorMeasure cannot be rewritten into the inner8 self-product that Parseval preserves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.