cost_probability_relation
plain-language theorem explainer
The cost-probability relation equates the Born probability of outcome i to exp of negative outcome cost for any finite-dimensional quantum state with non-zero amplitude at that index. Researchers deriving the measurement postulate from ledger commitment in Recognition Science would cite this to obtain the Born rule from J-costs. The term proof unfolds the two definitions, cancels a negation, confirms positivity of the squared norm, and applies the exp-log identity.
Claim. Let $n$ be a natural number and let $ψ$ be a normalized quantum state in dimension $n$ with amplitudes $ψ_i$. For each basis index $i$ where $ψ_i ≠ 0$, the measurement probability of outcome $i$ equals $e^{-C(i)}$, where $C(i)$ is the outcome cost of that branch.
background
QuantumState is the structure carrying a map from Fin n to Amplitude together with the normalization condition that the sum of squared norms equals one. The module derives the measurement postulate from ledger commitment: superposition is an uncommitted ledger entry, measurement forces commitment to one branch, and outcome probabilities follow from J-cost via the recognition weight |amplitude|². Upstream results include the QuantumLedger.QuantumState definition (configurations and complex amplitudes with normalization) and the PrimitiveDistinction.from theorem that extracts structural conditions from seven axioms.
proof idea
The term proof introduces the quantifiers, unfolds measurementProbability and outcomeCost, rewrites with the positive branch and negation cancellation, builds the positivity fact via norm_pos_iff and sq_pos_of_pos, and finishes with the symmetry of Real.exp_log.
why it matters
This result supplies the explicit link P(i) = exp(-Cost(i)) required by the module's derivation of the measurement postulate from ledger commitment. It thereby shows the Born rule emerges from recognition weights rather than being added by hand, consistent with the J-cost and RCL landmarks of the framework. The declaration closes one step in the QF-001 program that replaces the ad-hoc collapse postulate with ledger balancing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.