born_rule_normalized
plain-language theorem explainer
Recognition weights given by normalized exponentials of negative costs yield squared moduli that sum to one. Modal actualization and wavefunction collapse arguments cite this lightweight normalization when exporting the Born rule without full quantum machinery. The proof substitutes the two hypotheses into a common-denominator expression and cancels via the division identity.
Claim. Let $C_1, C_2$ be real numbers and let $α_1, α_2$ be complex numbers. If $e^{-C_1}/(e^{-C_1}+e^{-C_2})=|α_1|^2$ and $e^{-C_2}/(e^{-C_1}+e^{-C_2})=|α_2|^2$, then $|α_1|^2 + |α_2|^2 = 1$.
background
The module supplies a minimal algebraic lemma for the Born rule in Recognition Science. Recognition costs determine weights via the exponential map, which are then read directly as squared moduli of amplitudes. The local setting is a lightweight export path that avoids heavy quantum dependencies while preserving the normalization step required for probabilities to sum to unity.
proof idea
The tactic proof first establishes that the common denominator exp(-C₁) + exp(-C₂) is nonzero by positivity of the exponential. It then rewrites the target sum by substituting the two given equalities, applies the common-denominator addition identity, and concludes with the self-division rule.
why it matters
This lemma supplies the normalization step required by the parent Born rule theorem in the main Measurement module and by the actualization and collapse results. It fills the algebraic gap in the lightweight export path for the paper. In the Recognition framework it supports the claim that recognition weights normalize to probabilities, consistent with the normalization used in path-sum and quantum-state arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.