ledger_implies_probability
plain-language theorem explainer
Ledger conservation implies probability conservation once the ledger is identified with quantum amplitudes. Researchers deriving unitarity from information preservation in Recognition Science would cite this step. The proof is a one-line term assertion that the implication holds by direct identification of total ledger content with the sum of squared amplitudes.
Claim. If the total content of the ledger is conserved, then the sum of squared amplitudes $||ψ||^2$ is conserved.
background
The module QFT-009 derives unitarity from ledger conservation in Recognition Science. The ledger encodes quantum amplitudes such that total ledger content maps directly to probability sums. Conservation of the ledger therefore forces conservation of probabilities, yielding the unitary condition $U^†U = I$ as a consequence of information preservation. Upstream results include LedgerFactorization.of, which structures the ledger as a conserved quantity on the positive reals under multiplication, and QuantumLedger.probability, which supplies the identification between ledger entries and amplitude squares.
proof idea
The proof is a one-line term wrapper that applies the trivial tactic. It asserts the implication directly from the ledger-amplitude identification stated in the module doc-comment, without invoking further lemmas or reductions.
why it matters
This declaration supplies the direct link from ledger conservation to probability conservation, which feeds the unitarity derivation in the same module. It realizes the paper proposition that information conservation is the origin of unitarity. Within the Recognition framework it connects ledger conservation to the reversibility properties already established in the eight-tick structure and the PrimitiveDistinction axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.