prob
plain-language theorem explainer
The definition supplies the normalized weight exp(-C1) over the sum of both exponential costs for any two-outcome measurement. Researchers recovering the Born rule from recognition costs would cite this normalization step. It is realized by a direct algebraic expression in the supplied costs.
Claim. Let $m$ be a two-outcome measurement with non-negative recognition costs $C_1$ and $C_2$. The probability of outcome 1 is $P_1 = e^{-C_1}/(e^{-C_1}+e^{-C_2})$.
background
The module derives Born's rule $P(I)=|α_I|^2$ from the recognition cost functional $J$ and the amplitude bridge $𝒜=exp(-C/2)·exp(iφ)$. A TwoOutcomeMeasurement is the structure carrying two non-negative real numbers $C_1$ and $C_2$ that stand for the recognition costs of each outcome. The factors $exp(-C_i)$ arise directly as the squared moduli of the amplitudes before normalization.
proof idea
The definition is a direct one-line expression that normalizes the factors $exp(-C_i)$ obtained from the amplitude bridge.
why it matters
This definition supplies the explicit probability map used to recover the Born rule inside the module. It implements the normalization step once costs are identified with the recognition functional $J$. It sits inside the derivation of $P(I)=|α_I|^2$ from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.