born_rule_structure
plain-language theorem explainer
Every complex amplitude has nonnegative squared modulus, so Born probability weights cannot go negative. Quantum and ledger-consistency arguments cite this as the structural packaging of that fact. The proof is a one-line intro that applies the standard Complex.normSq nonnegativity lemma.
Claim. For every complex amplitude $\psi\in\mathbb{C}$, the squared modulus satisfies $0\le|\psi|^2$.
background
The module isolates structural Born-rule content: probability weights are nonnegative. The Prop being proved is exactly the universal statement that for every $\psi:\mathbb{C}$, $0\le\mathrm{Complex.normSq},\psi$.
Upstream, born_rule_consistent in Quantum.BornRule records the same inequality pointwise: $\mathrm{normSq},\psi\ge 0$, proved by Mathlib's Complex.normSq_nonneg. A parallel stub in QFT.Unitarity only asserts consistency with unitarity as True; the real content used here is the Quantum.BornRule lemma.
Eight-tick phase data (phase, Phase := Fin 8) lives nearby for phase-independence results in the same file, but is not needed for nonnegativity itself.
proof idea
One-line tactic wrapper. Introduce an arbitrary complex $\psi$, then apply born_rule_consistent from Quantum.BornRule, which is definitionally Complex.normSq_nonneg. No further rewriting or case analysis.
why it matters
In Recognition Science the Born rule is not an extra postulate: probability weights must emerge as nonnegative ledger quantities. This theorem closes the structural Prop born_rule_from_ledger that packages that nonnegativity, so later siblings (phase cancellation, pointwise nonnegativity implications) can treat the Born weight as already ledger-safe.
It sits in the Quantum domain next to unitarity and eight-tick phase structure (T7 octave). Downstream use count is currently zero; the declaration is the interface Prop itself rather than a consumer. No open scaffold remains: claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.