C_cos
plain-language theorem explainer
Complementary recognition action for the cos-branch of a two-outcome measurement rotation. Defined by C_cos = -2 log(cos θ_s), so that exp(-C_cos) recovers cos²(θ_s). Cited wherever normalized two-outcome Born weights are built from RS actions rather than measurement axioms. Pure definitional abbreviation; no proof content.
Claim. For a two-branch rotation with starting angle $\theta_s \in (0, \pi/2)$, the complementary action is $C_{\cos}(\mathrm{rot}) := -2\log(\cos\theta_s)$.
background
The Two-Outcome Born Certificate module upgrades the two-branch measurement bridge from a raw path-weight identity to normalized probabilities. A TwoBranchRotation packages a starting angle $\theta_s \in (0,\pi/2)$ and a positive duration $T$; the angle fixes the initial amplitude split between the two branches.
The sibling action $C_{\sin}$ is the genuine RS path action of the geodesic built from the rotation, so $\exp(-C_{\sin})$ equals $\sin^2\theta_s$ by the C2A bridge. $C_{\cos}$ is the complementary real scalar chosen so that $\exp(-C_{\cos})$ equals $\cos^2\theta_s$. Together the two actions feed a Gibbs-style normalization that yields the Born probabilities without any measurement-axiom typeclass.
proof idea
Definitional one-liner: $C_{\cos}$ is set equal to $-2\log(\cos\theta_s)$. Positivity of $\cos\theta_s$ on $(0,\pi/2)$ is deferred to the companion lemma that proves $\exp(-C_{\cos})=\cos^2\theta_s$.
why it matters
Supplies the missing cos-branch weight so that the normalized pair
$P_{\cos}=\exp(-C_{\cos})/(\exp(-C_{\cos})+\exp(-C_{\sin}))$ and $P_{\sin}$ equal $\cos^2\theta_s$ and $\sin^2\theta_s$. Downstream, exp_neg_C_cos_eq discharges the exponential identity, P_cos/P_sin build the probabilities, and born_rule_from_C lifts the construction to the full Born-rule statement matching quantum amplitude squares. The module thereby closes the two-outcome certificate using only the proven C2A bridge and elementary trigonometry, avoiding measurement axioms entirely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.