P_cos_eq
plain-language theorem explainer
The normalized two-outcome Gibbs probability on the cos-branch of a two-branch rotation equals the geometric complement amplitude squared, cos²(θ_s). Anyone citing the two-outcome Born certificate or the RS Gleason-style forcing of the Born weight uses this identity. The proof unfolds the exponential ratio, substitutes the closed forms exp(−C_cos)=cos² and exp(−C_sin)=sin², then cancels by cos²+sin²=1.
Claim. For every two-branch rotation with starting angle $\theta_s \in (0,\pi/2)$, the normalized cos-branch probability $P_{\cos}(\mathrm{rot}) = e^{-C_{\cos}}/(e^{-C_{\cos}}+e^{-C_{\sin}})$ equals the complement amplitude squared $\cos^2\theta_s$.
background
This module upgrades the two-branch measurement bridge from a raw path-weight identity (path weight = sin² θ) to normalized two-outcome probabilities. The cos-branch probability is the Gibbs ratio P_cos = exp(−C_cos)/(exp(−C_cos)+exp(−C_sin)), and the claim is that this equals cos² θ. Here C_sin is the recognition path action along the geodesic from the rotation, so exp(−C_sin) is the RS path weight; C_cos is the complementary action −2 log(cos θ), whose weight is cos² θ.
A TwoBranchRotation packages a starting angle θ_s in (0, π/2) and a positive duration T. From that geometry one reads off initialAmplitudeSquared = sin²(θ_s) and complementAmplitudeSquared = cos²(θ_s). The module deliberately avoids any measurement-axiom typeclass and relies only on the C2A bridge theorems plus elementary trigonometry.
Upstream, the sibling lemmas exp_neg_C_cos_eq and exp_neg_C_sin_eq already identify the un-normalized weights with those squared amplitudes; this theorem only normalizes.
proof idea
Term-mode proof in three steps. Unfold the definition of P_cos to the explicit ratio of exponentials. Rewrite the numerator and both summands via exp_neg_C_cos_eq and exp_neg_C_sin_eq, replacing exp(−C_cos) by cos²(θ_s) and exp(−C_sin) by sin²(θ_s). Then simp with the definitions of initialAmplitudeSquared and complementAmplitudeSquared together with Real.cos_sq_add_sin_sq at θ_s, which collapses the denominator cos²+sin² to 1 and leaves cos².
why it matters
This is one half of the two-outcome Born certificate: the verified predicate on TwoOutcomeBornCert asserts that both normalized Gibbs probabilities match cos²/sin² for every rotation, and P_cos_eq discharges the cos side. Downstream, sector_matches_gibbs_born rewrites the sector measure on the two-branch signal into these P_cos/P_sin values ("the sector measure agrees with the exp(−C) Gibbs probabilities proved in TwoOutcomeBornCert"). That calibration is the two-branch input to gleason_from_rs, which forces the Born weight w(r)=r² from phase invariance, additivity, and the Gibbs calibration. In the broader RS chain this is the concrete link from recognition action costs to the squared-amplitude Born rule, without external measurement postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.