born_rule_from_ledger
plain-language theorem explainer
Names the structural Born-rule content as the universal nonnegativity of complex squared norms: every amplitude ψ satisfies 0 ≤ |ψ|². Quantum and ledger-structure arguments cite this Prop as the interface hypothesis. It is a bare definition equating the name to that quantified inequality, with no proof obligation here.
Claim. The proposition asserting that for every complex amplitude $\psi\in\mathbb{C}$, the squared modulus is nonnegative: $0\le|\psi|^2$.
background
In the Born-rule structure module, probability weights are identified with squared norms of complex amplitudes. The Mathlib quantity Complex.normSq is the standard $|\psi|^2 = \psi\overline{\psi}$, which is nonnegative for all $\psi\in\mathbb{C}$.
Upstream, several RS carriers expose analogous squared-norm maps: finite amplitude vectors sum component squares; the finite Hilbert display reuses that complex squared norm as a Born weight; planar and metric carriers use Euclidean or quadratic-form squared norms. Those definitions fix the language of Born weights; the present declaration isolates the single structural demand that such weights stay nonnegative.
Locally this is only a named proposition, not a derivation of the full Born rule from the ledger. Downstream theorems treat it as the hypothesis package for pointwise nonnegativity.
proof idea
Definitional, not a proof. The body is the Prop ∀ ψ : ℂ, 0 ≤ Complex.normSq ψ. No tactics or lemmas fire at this site; discharge happens later when born_rule_structure introduces an arbitrary amplitude and applies born_rule_consistent.
why it matters
Gives the module a single named interface for the nonnegativity half of Born structure. born_rule_structure proves the proposition by reducing to the standard complex-norm fact. born_rule_nonnegative_at and born_rule_implies_nonnegative then unpack it at a fixed amplitude, so later ledger or measurement arguments can cite one hypothesis rather than re-proving $|\psi|^2\ge 0` each time.
In Recognition Science this is scaffolding for reading measurement weights off ledger amplitudes, not yet the full forcing of Born probabilities from the Recognition Composition Law or the eight-tick octave. It sits in the quantum layer that must eventually connect squared norms on the phi-ladder to observed frequencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.