born_rule_consistent
plain-language theorem explainer
The declaration asserts that the Born rule for probabilities is consistent with unitarity under ledger conservation in Recognition Science. Researchers deriving quantum mechanics from information preservation axioms would cite it when linking amplitude squares to conserved totals. The proof is a direct term application of the trivial proposition.
Claim. The Born rule gives probabilities via $P(i) = |⟨i|ψ⟩|²$, and unitarity ensures these probabilities sum to 1 under time evolution.
background
The QFT.Unitarity module derives unitarity from ledger conservation, where total ledger content remains constant and information is neither created nor destroyed. This conservation forces probability preservation, yielding the evolution operator condition $U†U = I$. Upstream LedgerFactorization structures the underlying (R₊, ×) calibration of J-cost, while PhiForcingDerived supplies the J-cost structures that enforce the conservation axiom.
proof idea
The proof is a one-line term proof that directly applies the trivial proposition to the consistency claim.
why it matters
This theorem confirms Born rule consistency as the initial step in QFT-009 unitarity derivation from ledger conservation. It supports the paper proposition on information conservation as the origin of unitarity and aligns with the framework's information-preservation axiom that underpins the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.