IndisputableMonolith.Verification.ProbabilityNormalizationCert
Verification module certifying that probabilities built from recognition costs are nonnegative, at most one, and sum to one. Anyone exporting measurement or Born-rule claims from the lightweight measurement layer would cite it. The argument is elementary: positivity of exponential sums and algebraic normalization of Boltzmann-style weights.
claimGiven recognition costs $C_i$, define $p_i = e^{-C_i}/\sum_j e^{-C_j}$. Then $p_i \ge 0$, $p_i \le 1$, and $\sum_i p_i = 1$. The module packages these facts as a probability-normalization certificate relative to a second cost reference $C_2$.
background
Recognition Science treats measurement outcomes as normalized weights built from recognition costs rather than as primitive amplitudes. The lightweight Born-rule module supplies the minimal algebraic interface for paper exports, deliberately avoiding heavy analysis dependencies.
This verification module sits one layer above that interface. It takes cost-derived unnormalized weights of the form $e^{-C}$ and records the standard facts needed to call them probabilities: the partition sum is strictly positive (hence nonzero), each normalized weight is nonnegative and at most one, and the weights sum to one.
The local convention is Boltzmann-style normalization from a pair of costs (the doc line: probability from recognition cost $C_1$ relative to $C_2$), matching the RS habit of reading likelihood from cost differences on the recognition ladder.
proof idea
Definition-plus-lemmas layout, not a single deep theorem. A constructor builds the normalized weight from a cost. Two short positivity lemmas show the exponential partition sum is positive and therefore nonzero in the base field. Nonnegativity and the bound by one are then immediate from positivity of exponentials and the definition of the normalizing constant. Normalization itself is the usual cancelation $\sum_i e^{-C_i}/Z = 1$. A certificate bundle assembles these facts for downstream export.
why it matters in Recognition Science
Closes the elementary gap between cost-as-generator and probability-as-normalized-weight in the verification domain. The upstream lightweight Born-rule module is explicitly a minimal algebraic lemma for paper exports; this module supplies the normalization certificate those exports need so measurement claims are not left as informal side conditions.
No downstream Lean dependents are recorded yet, so its role is export and audit hygiene rather than a step inside the T0–T8 forcing chain. It does not derive the Born rule from the Recognition Composition Law; it only certifies that once costs are given, the induced weights are a probability distribution.
scope and limits
- Does not derive the Born rule from the Recognition Composition Law or J-uniqueness.
- Does not fix a physical units convention or identify cost with a specific Hamiltonian.
- Does not treat continuous spectra, operator measures, or infinite outcome sets.
- Does not prove uniqueness of the exponential link from cost to weight.
- Does not feed a recorded downstream theorem in the current graph.