born_rule_nonnegative_at
plain-language theorem explainer
Under the ledger-derived Born-rule hypothesis, the squared modulus of any complex amplitude is nonnegative. Quantum and recognition-ledger arguments cite this as the pointwise nonnegativity half of structural Born content. The proof is a one-line term application of that hypothesis to the given amplitude.
Claim. If the Born rule is obtained from the quantum ledger, then for every complex amplitude $\psi\in\mathbb{C}$ one has $0\le|\psi|^2$.
background
The module collects structural Born-rule content: probability weights must be nonnegative. In the ledger picture, a quantum state carries complex amplitudes, and the probability of configuration $i$ is the squared modulus of the corresponding amplitude (as in QuantumLedger.probability).
Upstream, squared-norm primitives appear in several layers: finite amplitude vectors sum component squares; the finite Hilbert display reuses the complex squared norm; bipartite and holographic weights play analogous density roles. The standing hypothesis here is that the Born rule has already been extracted from the ledger, so nonnegativity is available as a structural property rather than a fresh analytic inequality.
Locally this sits next to phase-cancellation and full Born-structure packages: nonnegativity is the elementary half that every probability weight must satisfy before normalization or completeness is discussed.
proof idea
Term-mode one-liner. The hypothesis that the Born rule comes from the ledger is already a pointwise nonnegativity witness on complex amplitudes; apply it directly to $\psi$. No unfolding of Complex.normSq, no Mathlib positivity lemmas, and no case split.
why it matters
Feeds the sibling born_rule_implies_nonnegative, which is the same statement re-exported as the module's closing nonnegativity theorem ("Born-rule structure implies nonnegative probability weight at each amplitude"). Together they pin the structural claim of the module: ledger-derived Born weights are nonnegative at every amplitude.
In the broader Recognition stack this is the elementary positivity gate before Born probabilities can be treated as physical weights on the recognition ledger. It does not itself force the eight-tick octave, $D=3$, or the $\phi$-ladder mass formula; it only secures the sign of the weight that those constructions later normalize. Anyone assembling a full Born-rule package from ledger data needs this pointwise fact before summing or comparing alternatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.