born_rule_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of Born-rule probabilities for finite-dimensional quantum states in the Recognition ledger model. A physicist deriving the measurement postulate from cost axioms would cite it to confirm that extracted probabilities form a valid measure. The proof is a one-line term reduction that unfolds the squared-norm definition and invokes algebraic non-negativity of squares.
Claim. Let $n$ be a natural number, let $ψ$ be a normalized quantum state in dimension $n$ with amplitudes $ψ_i$ for each basis index $i$, and let $P_i$ denote the measurement probability of outcome $i$. Then $P_i = |ψ_i|^2$ satisfies $P_i ≥ 0$.
background
In this module a quantum state is a structure carrying a finite list of complex amplitudes together with the normalization condition that the sum of their squared moduli equals one; this representation appears consistently across QuantumLedger, NoCloning, and Unitary modules. The measurement probability for a given outcome is defined directly as the squared modulus of the corresponding amplitude. The surrounding theoretical setting treats superposition as an uncommitted ledger entry whose commitment upon measurement yields probabilities proportional to recognition cost, with the Normalization axiom from CostAxioms supplying the zero-cost reference point at unity.
proof idea
The term proof first unfolds the definition of measurementProbability to expose the squared norm of the amplitude, then applies the lemma sq_nonneg to obtain the required inequality.
why it matters
The result supplies the non-negativity half of the Born rule inside the ledger-commitment account of wavefunction collapse. It directly supports the module's derivation of the measurement postulate from Recognition Science cost structure, where probabilities arise as relative recognition weights. The companion normalization statement (probabilities summing to one) is flagged immediately after this theorem in the source, indicating the pair together yields a probability measure. The underlying cost axioms link to the Recognition Composition Law and the phi-ladder used elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.