born_rule_implies_nonnegative
plain-language theorem explainer
Under the structural Born-rule hypothesis (probability weights are nonnegative for every complex amplitude), the squared modulus of any amplitude is nonnegative. Quantum and measurement theorists in the Recognition ledger setting would cite this when discharging nonnegativity side conditions. The proof is a one-line term application of the pointwise nonnegativity lemma.
Claim. If the structural Born-rule hypothesis holds (for every complex amplitude $\psi$, $0 \le |\psi|^2$), then for any fixed $\psi \in \mathbb{C}$ one has $0 \le |\psi|^2$.
background
The module records structural Born-rule content: probability weights extracted from amplitudes must be nonnegative. The hypothesis born_rule_from_ledger is exactly the universal statement $\forall \psi:\mathbb{C},, 0\le |\psi|^2$, i.e. the squared complex modulus is a nonnegative real weight.
In the broader Recognition stack the same squared-norm idea appears as finite amplitude-vector norms, finite Hilbert-display norms, planar carrier norms, and metric quadratic forms. Here the carrier is simply $\mathbb{C}$ with Mathlib's Complex.normSq. The sibling pointwise lemma already specializes the universal hypothesis to a single amplitude; this declaration packages that specialization under the "implies nonnegative" name used by the module narrative.
proof idea
One-line term proof: apply the sibling lemma that, given the structural Born-rule hypothesis and any amplitude $\psi$, returns $0\le|\psi|^2$ by instantiating the universal quantifier. No algebraic rewriting or case analysis is required.
why it matters
Born-rule structure is the minimal ledger-side demand that measurement weights be nonnegative before any normalization or phase cancellation is imposed. This theorem is the named bridge from that global hypothesis to a concrete nonnegativity obligation at a single amplitude, matching the module's stated content ("probability weights are nonnegative").
It sits next to phase-cancellation and structure-packaging siblings in the same file. No downstream consumers are wired yet (used_by is empty), so its present role is local API: give later Born-rule or measurement lemmas a short name for the nonnegativity side condition without reopening the universal Prop. It does not itself derive the Born rule from the forcing chain (T0–T8) or from the Recognition Composition Law; it only propagates the structural nonnegativity assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.