P_sin_eq
plain-language theorem explainer
Normalized Gibbs weight of the sin branch on a two-branch rotation equals the geometric amplitude sin²(θ_s). Cited by anyone matching RS path weights to Born-rule probabilities, and by the two-outcome Born certificate. Proof unfolds the exponential ratio, substitutes the closed forms exp(−C)=cos²/sin², and cancels via cos²+sin²=1.
Claim. For every two-branch rotation with starting angle $\theta_s\in(0,\pi/2)$, the normalized sin-branch probability $e^{-C_{\sin}}/(e^{-C_{\cos}}+e^{-C_{\sin}})$ equals the initial amplitude squared $\sin^2(\theta_s)$.
background
The Two-Outcome Born Certificate module lifts the two-branch measurement bridge from a raw path-weight identity to normalized probabilities. A TwoBranchRotation is a geodesic rotation from angle $\theta_s\in(0,\pi/2)$ to $\pi/2$; its geometric amplitudes are $\sin^2(\theta_s)$ (initial) and $\cos^2(\theta_s)$ (complement).
Recognition actions supply the Gibbs weights: $C_{\sin}$ is the path action along the rotation (so $e^{-C_{\sin}}$ is the RS path weight), and $C_{\cos}=-2\log(\cos\theta_s)$ is the complementary action whose weight is $\cos^2\theta_s$. The normalized sin-branch probability is then $P_{\sin}=e^{-C_{\sin}}/(e^{-C_{\cos}}+e^{-C_{\sin}})$.
Sibling lemmas already give the closed forms $e^{-C_{\cos}}=\cos^2\theta_s$ and $e^{-C_{\sin}}=\sin^2\theta_s$. The module uses only the C2A bridge and elementary trigonometry, with no measurement-axiom typeclass.
proof idea
Term-mode proof in three steps. Unfold the definition of the normalized sin-branch probability. Rewrite the two exponential factors by the sibling identities exp_neg_C_cos_eq and exp_neg_C_sin_eq, replacing them with $\cos^2\theta_s$ and $\sin^2\theta_s$. Then simp with the amplitude definitions and the Pythagorean identity $\cos^2\theta_s+\sin^2\theta_s=1$ collapses the denominator, leaving $\sin^2\theta_s$, which is exactly the initial amplitude squared.
why it matters
Closes the sin half of the two-outcome Born certificate: together with the companion cos identity it proves that normalized Gibbs weights equal Born amplitudes, which is the verification predicate on TwoOutcomeBornCert.
Downstream, sector_matches_gibbs_born rewrites sector measures of the two-branch signal against $P_{\cos}$ and $P_{\sin}$ via this equality, calibrating the discrete sector measure to the exp(−C) Gibbs law. That calibration is the two-branch input to gleason_from_rs, the Gleason-style uniqueness result forcing the Born weight $r\mapsto r^2$ from RS axioms (phase invariance, additivity, and this Gibbs match).
In the broader framework this is the concrete link from recognition path action to quantum probabilities, without external measurement postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.