born_rule_phase_cancels
plain-language theorem explainer
Global phase drops out of Born weights: for real radius and angle, the squared modulus of r·e^{iθ} equals r². Quantum and double-slit arguments cite this when converting complex amplitudes to probabilities. The proof is a one-line term wrapper of the phase-independence lemma in BornRule.
Claim. For all real $r$ and $\theta$, $\lvert r\, e^{i\theta}\rvert^{2}=r^{2}$. Equivalently, a global $U(1)$ phase multiplies a real amplitude without changing its Born weight.
background
The module collects structural Born-rule facts: probability weights extracted from complex amplitudes are nonnegative. The basic weight is the complex squared modulus $\lvert z\rvert^{2}=z\overline{z}$, written Complex.normSq in Lean and aligned with several RS-side squared-norm carriers (finite amplitude vectors, finite Hilbert displays, planar bipartite points, and metric quadratic forms).
Upstream, born_rule_phase_independent already states the same identity and proves it by expanding the product, using $\lvert e^{i\theta}\rvert^{2}=1$, and reducing the real factor. Double-slit amplitudes are pure phase sums $e^{i\varphi_{1}}+e^{i\varphi_{2}}$, so intensity calculations repeatedly need that overall phase factors cancel in $\lvert A\rvert^{2}$.
proof idea
One-line term proof: apply the upstream theorem born_rule_phase_independent at the same real arguments $r$ and $\theta$. No extra rewriting is done here; the algebraic work (norm of a product, unit modulus of $e^{i\theta}$, real squared norm, and ring simplification) lives entirely in that lemma.
why it matters
Phase cancellation is the structural reason Born probabilities depend only on modulus, not on global $U(1)$ gauge. In the Recognition Science quantum layer this licenses reading ledger-derived amplitudes as physical weights once they are reduced to real nonnegative numbers. Sibling results in the same module package nonnegativity of those weights and the ledger-to-Born bridge; double-slit intensity is the concrete consumer of the same identity. No downstream theorem currently depends on this alias, so it functions as a named structural restatement inside BornRuleStructure rather than a new forcing step (T0–T8 are not touched).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.