IndisputableMonolith.Measurement.BornRuleLight
Module that turns raw recognition weights into normalized Born-rule probabilities. Measurement and verification layers cite it when they need sum-to-one probabilities from a pair of recognition costs. The argument is elementary: divide each weight by the total weight so the two outcomes form a probability distribution.
claimFrom recognition costs $C_1, C_2 \in \mathbb{R}$, form unnormalized weights $w_i = e^{-C_i}$ (or the RS-native weight map) and set $p_i = w_i / (w_1 + w_2)$, so that $p_1 + p_2 = 1$ and $p_i \ge 0$.
background
In Recognition Science, measurement outcomes are scored by recognition costs rather than by an external Born postulate. A cost $C$ is converted to a positive weight; the physical probability is that weight normalized over the exclusive alternatives.
This module sits in the Measurement domain and supplies the light, Mathlib-only form of that normalization. It does not derive the exponential (or RS-native) weight map from the J-cost or the forcing chain; it only packages the passage from a pair of weights to a two-outcome probability vector.
Downstream, the probability-normalization certificate uses exactly this construction: any two recognition costs yield probabilities that sum to one.
proof idea
Definition-and-lemma module, not a deep derivation. It introduces the normalized Born map for two recognition-weighted outcomes and records the elementary identity that the resulting $p_1, p_2$ are nonnegative and sum to 1 whenever the total weight is positive. No forcing-chain or RCL lemmas are required; the algebra is plain division by the sum of weights.
why it matters in Recognition Science
Feeds ProbabilityNormalizationCert in the Verification layer, whose stated goal is that recognition-weighted probabilities are properly normalized: any two costs $C_1, C_2$ produce probabilities summing to 1. That certificate is the audit hook for the Born-rule side of RS measurement. The module is the minimal Measurement primitive those checks import, keeping the weight-to-probability step separate from heavier RS infrastructure (J-uniqueness, eight-tick structure, mass ladder).
scope and limits
- Does not derive the weight map from J-cost, RCL, or the T0–T8 forcing chain.
- Does not treat more than two exclusive outcomes in the core statement.
- Does not prove continuity, differentiability, or POVM-level quantum structure.
- Does not fix units or identify costs with laboratory Hamiltonians.