born_rule_phase_independent
plain-language theorem explainer
Global phase drops out of Born weights: the squared modulus of a real amplitude times a pure phase factor equals the square of that amplitude. Anyone deriving P = |ψ|² from Recognition Science phase invariance cites this identity. The proof is a short rewrite chain using multiplicativity of Complex.normSq, unitarity of e^{iθ}, and the real-embedding formula, closed by ring.
Claim. For all real $r$ and $\theta$, $\lvert r \, e^{i\theta}\rvert^2 = r^2$.
background
Module QF-002 derives the Born rule $P = \lvert\psi\rvert^2$ as the unique probability measure on 8-mode DFT sectors that is normalised, phase-invariant, additive on disjoint mode-sets, and consistent with the two-branch $\exp(-C)$ calibration. Phase invariance of $J$-cost is the hinge: probability may depend only on moduli, never on $\arg(\psi_k)$.
Complex squared modulus is the standard Mathlib map $\mathrm{normSq}:\mathbb{C}\to\mathbb{R}$. Sibling normSq_exp_I_eq_one records $\lvert e^{i\theta}\rvert^2 = 1$. Upstream amplitude displays (DeltaAmplitude.normSq, Hilbert-display normSq) package the same squared-modulus idea for finite mode vectors; the eight-tick phase values $k\pi/4$ supply the discrete phases that appear in the DFT-8 sector picture.
The full forcing argument lives in Foundation.BornRuleForcing; this lemma is the elementary complex-analysis step that makes phase cancellation available to the quantum layer.
proof idea
Rewrite chain, not a deep argument. Expand $\mathrm{normSq}$ of a product via Complex.normSq_mul. Replace $\mathrm{normSq}(e^{i\theta})$ by $1$ using the sibling normSq_exp_I_eq_one. Cancel the unit factor with mul_one. Convert $\mathrm{normSq}$ of a real embedding via Complex.normSq_ofReal, then finish the remaining polynomial identity with ring.
why it matters
Phase independence is step 2 of the RS Born-rule mechanism in the module doc: once $J$-cost is phase-invariant, probabilities depend only on moduli. Downstream, born_rule_phase_cancels in BornRuleStructure is a one-line re-export of this theorem, packaging the same identity for the structural layer (nonnegativity and global-phase freeness of Born weights).
Together with born_rule_from_jcost, normalization_from_jcost, and gleason_from_rs, it supports the claim that $P=\lvert\psi\rvert^2$ is forced rather than postulated, calibrated by the two-branch $\exp(-C)$ model and lifted by Parseval to the DFT-8 frequency basis. It does not itself invoke the eight-tick octave or $D=3$, but it is the complex-arithmetic fact those sector arguments rely on whenever a global phase multiplies an amplitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.