norm_ofReal_sq
plain-language theorem explainer
For any real r, the squared complex modulus of its embedding into ℂ equals r². Born-rule forcing cites this when two-branch amplitudes are real cos/sin values placed on DFT-8 modes. The proof rewrites via the normSq–‖·‖² identity and Complex.normSq_ofReal, then closes by ring.
Claim. For every real number $r$, $\| r \|_{\mathbb{C}}^{2} = r^{2}$, where $r$ is viewed as an element of $\mathbb{C}$ via the standard real embedding.
background
The module forces the Born rule on 8-mode signals: the unique probability measure on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and consistent with the two-branch exp(−C) calibration is μ(S) = Σ_{k∈S} ‖ψ_k‖² (equivalently the Parseval image under DFT-8).
Two-branch signals embed a rotation angle θ by placing real amplitudes cos θ and sin θ on modes 0 and 1 of a Signal8. Sector measures then reduce to squared moduli of those real entries, so one needs ‖ofReal r‖² = r².
Upstream, normSq_eq_norm_sq equates Complex.normSq z with ‖z‖² for any z ∈ ℂ (via the definition of the complex norm and nonnegativity of normSq). Mathlib supplies Complex.normSq_ofReal: normSq(ofReal r) = r².
proof idea
Term-style tactic proof in three steps. Rewrite the goal with the converse of normSq_eq_norm_sq so the left-hand side becomes Complex.normSq(ofReal r). Apply Complex.normSq_ofReal to obtain r². Finish with ring (trivial algebraic identity on reals). No case splits or induction.
why it matters
Local glue for the two-branch calibration inside Born-rule forcing. Downstream, sector_matches_cos_branch and sector_matches_sin_branch use it to identify sector measure on modes 0 and 1 with complementAmplitudeSquared and initialAmplitudeSquared (cos²θ and sin²θ). twoBranchSignal_normalized uses the same identity to prove the embedded signal has total mass 1 (cos²θ + sin²θ = 1).
That normalisation and branch matching close the Born-rule gap against TwoOutcomeBornCert (P_cos_eq, P_sin_eq), tying the unique sector measure to the two-outcome exp(−C) rule. Framework landmarks: depends on complex structure and DFT-8 from T7 (eight-tick octave) and the measurement mechanism F-009; sits under the foundation chain that already forces J-cost uniqueness (T5) and D = 3 (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.