interference_from_phase
plain-language theorem explainer
For any two complex amplitudes, the squared modulus of their sum equals the sum of squared moduli plus twice the real part of the first times the conjugate of the second. This is the classical interference cross-term identity. Quantum and entanglement-ontology arguments in the RS Born-rule stack cite it to expose relative-phase dependence. The proof is a one-line application of Mathlib's Complex.normSq_add.
Claim. For all $\psi_1,\psi_2\in\mathbb{C}$, $|\psi_1+\psi_2|^2=|\psi_1|^2+|\psi_2|^2+2\operatorname{Re}(\psi_1\overline{\psi_2})$.
background
Module QF-002 derives the Born rule $P=|\psi|^2$ as the unique probability measure on 8-mode DFT sectors that is normalised, phase-invariant, additive on disjoint mode-sets, and calibrated to the two-branch $\exp(-C)$ Gibbs weight. The RS mechanism is: DFT-8 splits a ledger state into eight orthogonal modes; J-cost phase invariance forces probabilities to depend only on moduli; Finset additivity handles disjoint sectors; the two-branch certificate fixes singleton weights to $r\mapsto r^2$; Parseval carries the measure to the frequency basis.
The present identity is the elementary complex-analysis expansion that isolates the interference cross-term $2\operatorname{Re}(\psi_1\overline{\psi_2})$. Upstream infrastructure supplies squared-norm primitives (finite amplitude vectors, Hilbert display completion) and the eight-tick phase grid $k\pi/4$, but the identity itself is pure $\mathbb{C}$-algebra and does not invoke J-cost or the rung ladder.
proof idea
One-line term proof: apply Mathlib's Complex.normSq_add to the two amplitudes. No RS-specific lemmas are used; the declaration simply re-exports the standard expansion under the module's naming so downstream entanglement and Born-rule arguments can cite a local name.
why it matters
The sole recorded consumer is entanglement_ontology_structure, which reduces the entanglement-ontology ledger claim to this cross-term identity by applying it to a pair of amplitudes. In the QF-002 stack the identity is the algebraic hinge between phase-invariant Born weights (moduli only) and genuine two-path interference: when relative phase varies, the cross-term oscillates while the separate $|\psi_i|^2$ stay fixed. That separation is what lets the DFT-8 sector forcing (phase invariance plus two-branch calibration) force $P=|\psi|^2$ without smuggling interference in by hand. It sits beside siblings such as phase-independence of the Born weight and the J-cost derivation of normalisation, and feeds the broader claim that entanglement structure is ledger geometry rather than an extra postulate. Framework landmarks touched indirectly: T7 eight-tick octave (the DFT-8 mode grid) and the Born-rule forcing chain in Foundation.BornRuleForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.