born_rule_consistent
plain-language theorem explainer
Squared modulus of any complex amplitude is nonnegative, the elementary consistency condition for Born weights P = |ψ|². Cited by the ledger-to-Born packaging and by the QFT unitarity stub that records the same fact. Proof is a one-line appeal to Mathlib's Complex.normSq_nonneg.
Claim. For every complex amplitude $\psi \in \mathbb{C}$, the squared modulus satisfies $|\psi|^2 \ge 0$.
background
Module QF-002 derives the Born rule $P = |\psi|^2$ as the unique probability measure on 8-mode sectors that is normalised, phase-invariant, additive on disjoint mode-sets, and compatible with the two-branch $\exp(-C)$ Gibbs model. The forcing chain lives in Foundation.BornRuleForcing; this file records the elementary consistency facts used along that path.
In Recognition Science the cost functional $J$ is phase-invariant, so probabilities can depend only on moduli. The squared-modulus map is the candidate weight. Upstream, finite-amplitude and Hilbert-display squared norms are defined as sums of squares (DeltaAmplitude.normSq, HilbertDisplayCompletion.normSq) and proved nonnegative by summing sq_nonneg. The present statement is the scalar complex case of the same nonnegativity.
The 8-tick phase space (Phase := Fin 8) and DFT-8 sector decomposition supply the ambient mode structure, but are not needed for this inequality alone.
proof idea
Term-mode one-liner: apply Mathlib's Complex.normSq_nonneg to the given amplitude. No local lemmas, no unfolding, no tactics. The same nonnegativity pattern appears upstream for finite amplitude vectors as a Finset sum of squares.
why it matters
Closes the first consistency gate in the Born-from-J-cost package: weights that could become probabilities must be nonnegative. Downstream, born_rule_structure packages the ledger claim by introducing an arbitrary amplitude and discharging it with exactly this theorem. The QFT.Unitarity sibling of the same name currently records only True, so this Quantum.BornRule version is the nontrivial nonnegativity fact the structure theorem actually consumes.
In the broader RS story this is a prerequisite, not the forcing step. Uniqueness of $r \mapsto r^2$, phase independence, disjoint-sector additivity, and the two-branch exp(-C) calibration are sibling results (and the full derivation in BornRuleForcing). The eight-tick octave (T7) and DFT-8 sector picture set the mode count, but nonnegativity itself is basis-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.