C_sin

The module upgrades the two-branch measurement bridge from a raw weight identity (path weight equals $\sin^2\theta$) to normalized two-outcome probabilities $P_{\cos}=\cos^2\theta$ and $P_{\sin}=\sin^2\theta$. No measurement-axiom typeclass is used; only the proven bridge in Measurement/C2ABridge and elementary trigonometry.

A two-branch rotation packages the angle $\theta_s$ that splits amplitude between complementary cos and sin channels. The measurement bridge builds a continuous path $\gamma_{\mathrm{rot}}$ from that rotation (pathFromRotation) and assigns it a recognition path action $S[\gamma]$ (pathAction). The RS path weight is then $e^{-S[\gamma]}$.

Upstream, the bridge theorem weight_equals_born already equates that path weight to the initial amplitude squared $\sin^2\theta_s$. The complementary cos cost is defined separately as $-2\log(\cos\theta_s)$, so the two Boltzmann factors sum and normalize cleanly.

Pure definitional wrapper: $C_{\sin}$ is literally pathAction (pathFromRotation rot). No tactics or lemmas are invoked at the definition site. Downstream lemmas (e.g. exp_neg_C_sin_eq) unfold this abbreviation, apply weight_equals_born, and rewrite pathWeight = exp(-pathAction) to obtain $e^{-C_{\sin}}=\sin^2\theta_s$.

This cost is the sin-channel half of the two-outcome Born certificate. Normalized probabilities $P_{\sin}$ and $P_{\cos}$ are built from $e^{-C_{\sin}}$ and $e^{-C_{\cos}}$; the lemma exp_neg_C_sin_eq turns the definition into the identity $e^{-C_{\sin}}=\sin^2\theta_s$. Downstream, born_rule_from_C in Measurement.BornRule uses the pair of costs to exhibit a two-outcome measurement whose outcome probabilities match quantum amplitude squares, closing the bridge from RS path action to the Born rule without extra measurement postulates.