exp_neg_C_cos_eq
plain-language theorem explainer
For any two-branch rotation, the Boltzmann weight of the complementary action equals cos squared of the mixing angle. Anyone citing the two-outcome Born certificate needs this identity to turn raw path weights into normalized probabilities. The proof is a short calc: cancel the double negative in the exponent, apply log-power and exp-log, using positivity of cos on the open first quadrant.
Claim. Let $\mathrm{rot}$ be a two-branch rotation with mixing angle $\theta_s \in (0,\pi/2)$. Write $C_{\cos}(\mathrm{rot}) := -2\log(\cos\theta_s)$. Then $\exp(-C_{\cos}(\mathrm{rot})) = \cos^2\theta_s$.
background
The Two-Outcome Born Certificate module upgrades the two-branch measurement bridge from a raw weight identity to normalized probabilities. The sin-side weight already comes from the proven bridge: $\exp(-2A)=\sin^2\theta_s$ via born_weight_from_rate. The complementary action is defined by hand as $C_{\cos}=-2\log(\cos\theta_s)$, so that its Boltzmann factor should be $\cos^2\theta_s$.
A TwoBranchRotation packages a mixing angle $\theta_s$ strictly inside $(0,\pi/2)$ together with the geodesic data that feed the recognition path action. The target right-hand side is the named complement amplitude squared, simply $(\cos\theta_s)^2$. The module deliberately avoids any measurement-axiom typeclass and works only from the C2A bridge and elementary trigonometry.
proof idea
Unfold both sides. First obtain $\cos\theta_s>0$ from the open-interval bounds on $\theta_s$ (via Real.cos_pos_of_mem_Ioo). Then a three-step calc: $\exp(-(-2\log\cos\theta_s))$ simplifies by ring to $\exp(2\log\cos\theta_s)$; the log-power identity rewrites the exponent as $\log((\cos\theta_s)^2)$; finally Real.exp_log on the positive square recovers $(\cos\theta_s)^2$. The pattern mirrors born_weight_from_rate on the sin side.
why it matters
This lemma is the cos half of the weight pair that feeds the normalized two-outcome probabilities. Downstream, P_cos_eq and P_sin_eq rewrite both Boltzmann factors and cancel the common denominator $\cos^2+\sin^2=1$, yielding $P_{\cos}=\cos^2\theta_s$ and $P_{\sin}=\sin^2\theta_s$. That closes the certificate that Recognition path weights, once normalized, reproduce the Born rule for a two-outcome measurement without extra axioms. It sits inside the verification layer that audits the measurement bridge rather than inside the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.