probabilities_normalized
For any two-outcome measurement given by non-negative recognition costs C1 and C2, the probabilities formed as normalized exponentials of the negative costs sum to one. Workers deriving the Born rule from the recognition cost functional J would cite this to confirm the probabilities constitute a valid distribution before equating them to squared amplitudes. The proof is a short tactic sequence that unfolds the probability definitions, proves the denominator nonzero via positivity of exponentials, and reduces the sum to the identity x/x = 1.
claimLet $m$ be a two-outcome measurement with non-negative recognition costs $C_1, C_2$. Define $p_1 = e^{-C_1}/(e^{-C_1}+e^{-C_2})$ and $p_2 = e^{-C_2}/(e^{-C_1}+e^{-C_2})$. Then $p_1 + p_2 = 1$.
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φ). The central structure is the two-outcome measurement, a record holding a pair of non-negative reals C1 and C2 that represent the recognition costs assigned to each outcome. Probabilities are then constructed as the normalized exponentials of the negative costs, ensuring they lie in [0,1] and sum to unity.
proof idea
Unfold the two probability definitions to expose the ratio of exponentials. Establish that the common denominator is nonzero by adding two strictly positive exponentials and negating the zero claim. Introduce the denominator as a local variable, then apply the add_div identity to show the sum of the separate fractions equals the total numerator over the denominator. Finish by invoking div_self on the nonzero denominator.
why it matters in Recognition Science
The result guarantees that probabilities extracted from recognition costs form a normalized measure, a necessary step before matching them to squared amplitudes in the Born-rule derivation. It directly supports the module goal of obtaining P(I) = |α_I|² from J and the amplitude bridge. In the Recognition Science setting this normalization precedes the identification with the S-matrix elements whose squared moduli give transition probabilities, consistent with the forcing chain that fixes J-uniqueness and the eight-tick octave.
scope and limits
- Does not derive the explicit functional form of the probabilities from the underlying J-cost.
- Does not treat measurements with more than two outcomes.
- Does not connect the costs C1 and C2 to the phi-ladder or spatial dimension D=3.
- Does not address phase factors or interference in the amplitude bridge.
formal statement (Lean)
46theorem probabilities_normalized (m : TwoOutcomeMeasurement) :
47 prob₁ m + prob₂ m = 1 := by
proof body
Tactic-mode proof.
48 unfold prob₁ prob₂
49 have hdenom : Real.exp (-m.C₁) + Real.exp (-m.C₂) ≠ 0 :=
50 (add_pos (Real.exp_pos _) (Real.exp_pos _)).ne'
51 set denom : ℝ := Real.exp (-m.C₁) + Real.exp (-m.C₂)
52 have hadd :
53 Real.exp (-m.C₁) / denom + Real.exp (-m.C₂) / denom = (Real.exp (-m.C₁) + Real.exp (-m.C₂)) / denom := by
54 simpa [denom] using (add_div (Real.exp (-m.C₁)) (Real.exp (-m.C₂)) denom).symm
55 -- Finish.
56 simpa [denom, hadd] using (div_self hdenom)
57
58/-- Born rule: probabilities match quantum amplitude squares -/