prob
plain-language theorem explainer
Defines the probability of the first outcome in a two-outcome measurement as the normalized exponential of its negative recognition cost. Researchers deriving the Born rule from recognition costs would reference this when normalizing weights from the cost functional J. It is implemented as a direct division of exponentials without additional lemmas.
Claim. $P_1 = e^{-C_1} / (e^{-C_1} + e^{-C_2})$ for a two-outcome measurement with nonnegative recognition costs $C_1, C_2$.
background
The module derives Born's rule P(I) = |α_I|² from the recognition cost functional J and the amplitude bridge 𝒜 = exp(-C/2)·exp(iφ). TwoOutcomeMeasurement is a structure with fields C₁, C₂ (recognition costs for each outcome) together with proofs that both are nonnegative. This supplies the explicit probability for outcome 1 via normalized Boltzmann weights.
proof idea
The definition is a direct algebraic expression that normalizes the exponential weights exp(-C₁) and exp(-C₂). No lemmas are applied; it is the explicit formula.
why it matters
This definition provides the explicit form for outcome probabilities in the derivation of the Born rule within the Recognition Science framework. It connects the recognition costs to probabilities via the amplitude bridge, feeding into later results such as born_rule_from_C and born_rule_normalized. It supports the emergence of quantum probabilities from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.