ProbabilityNormalizationCert
plain-language theorem explainer
Empty marker certificate whose verification predicate asserts that recognition-weighted two-outcome probabilities are non-negative, at most one, and sum to one under cost swap. Anyone auditing the Born-rule-light measurement layer cites it. The companion theorem discharges the predicate by applying three elementary lemmas on the cost-to-probability map.
Claim. A unit certificate type whose verification predicate holds iff for all real costs $C_1,C_2$, the recognition-weighted probability $p(C_1,C_2)=e^{-C_1}/(e^{-C_1}+e^{-C_2})$ satisfies $0\le p(C_1,C_2)\le 1$ and $p(C_1,C_2)+p(C_2,C_1)=1$.
background
This module sits in the Verification layer and certifies that recognition-weighted probabilities form a valid two-outcome distribution. The underlying map sends a pair of real recognition costs $(C_1,C_2)$ to
$$p(C_1,C_2)=\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}.$$
Sibling lemmas establish the three ingredients: non-negativity of $p$, the bound $p\le 1$, and exact complementary normalization $p(C_1,C_2)+p(C_2,C_1)=1$. The module doc stresses that the argument uses only positivity of $\exp$, the division identity $a/d+b/d=(a+b)/d$, and $x/x=1$ for $x\ne 0$; no physical hypotheses enter.
Upstream, related non-negativity and unit bounds appear for finite distinction probabilities in the Primitive Recognition Calculus, but the certificate here is purely about the continuous cost-to-probability map used by the light Born-rule measurement model.
proof idea
The structure itself is an empty marker (only Repr). The interesting object is the simp-normal verified predicate: a three-way conjunction of universal statements over real costs.
The top-level theorem verified_any is a one-line wrapper. It refines the conjunction into three goals and closes them by exact on the sibling lemmas prob_nonneg, prob_le_one, and prob_normalization respectively. No new analysis is performed at the certificate layer.
why it matters
Without normalization, the two-outcome recognition measurement model would not define a probability distribution. This certificate packages that algebraic fact so the Verification layer can assert, in one place, that recognition-weighted probabilities conserve probability, leave no missing mass, and introduce no excess mass.
It underwrites the light Born-rule path imported from Measurement.BornRuleLight: once costs are assigned to complementary outcomes, the exponential weighting automatically yields a valid Bernoulli law. The module doc emphasizes non-circularity: the proof is elementary real analysis (Mathlib exp_pos and div_self), independent of the forcing chain T0–T8, the J-cost uniqueness, or the phi ladder. No downstream consumers are wired yet (used_by is empty), so the certificate presently stands as a self-contained verification unit rather than a lemma inside a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.