TwoOutcomeBornCert
plain-language theorem explainer
Empty certificate type whose verification predicate asserts that normalized two-outcome recognition probabilities equal cos²θ and sin²θ for every two-branch rotation. RecogSpec cites it as the Born-rule compliance witness; Born-rule forcing uses the same bridge. Discharge is immediate from the sibling identities equating the Gibbs-normalized path weights to the trigonometric amplitudes.
Claim. A two-outcome Born certificate is a unit token. It is verified when, for every two-branch rotation $\mathrm{rot}$, the normalized cos-branch probability equals the complementary amplitude squared and the normalized sin-branch probability equals the initial amplitude squared: $P_{\cos}(\mathrm{rot})=\cos^2\theta$ and $P_{\sin}(\mathrm{rot})=\sin^2\theta$.
background
The module upgrades the two-branch measurement bridge from a raw path-weight identity (path weight $=\sin^2\theta$) to normalized two-outcome probabilities. Recognition actions supply the weights: $C_{\sin}$ is the path action of the geodesic from the rotation, so $\exp(-C_{\sin})$ is the RS path weight; $C_{\cos}$ is the complementary action $-2\log(\cos\theta)$ whose weight is $\cos^2\theta$. The normalized probabilities are then
$$P_{\cos}=\frac{e^{-C_{\cos}}}{e^{-C_{\cos}}+e^{-C_{\sin}}}=\cos^2\theta,\qquad P_{\sin}=\frac{e^{-C_{\sin}}}{e^{-C_{\cos}}+e^{-C_{\sin}}}=\sin^2\theta.$$
No measurement-axiom typeclass is used. The equalities rest on proven bridge theorems in Measurement/C2ABridge together with elementary trigonometry, and on the two-branch geodesic constructions that define initial and complementary amplitude squares.
proof idea
The structure is an empty token (no fields). The interesting content is the verified predicate: a universal quantification over two-branch rotations requiring $P_{\cos}=\mathrm{complementAmplitudeSquared}$ and $P_{\sin}=\mathrm{initialAmplitudeSquared}$.
The companion theorem verified_any is a one-line wrapper: introduce the rotation and pair the sibling lemmas P_cos_eq and P_sin_eq, which already establish those two equalities. No further algebra is done at this layer.
why it matters
This certificate is the RecogSpec Born-rule compliance witness. Downstream, bornHolds is defined as TwoOutcomeBornCert.verified {}, and born_from_TruthCore discharges it by verified_any. That closes the "recognition path weights match Born probabilities" slot in the universal dimensionless pack.
It also sits next to Born-rule forcing: sector_matches_sin_branch identifies the mode-1 sector measure of the two-branch signal with $\sin^2\theta$ (initial amplitude squared), so the normalized Gibbs weights certified here line up with the forced sector measures. In the broader RS chain this is the measurement-side counterpart of the J-cost and eight-tick structure: probabilities emerge from recognition actions rather than from a postulated Born axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.