exp_neg_C_sin_eq
plain-language theorem explainer
For a two-branch rotation, the exponential of minus the sin-branch recognition action equals the squared initial amplitude (sin² θ). Anyone deriving normalized Born probabilities from RS path weights cites this identity. The proof is a short rewrite of the measurement-bridge theorem weight_equals_born through the definitions of path weight and the sin-branch action.
Claim. For every two-branch rotation, $\exp(-C_{\sin})=\sin^2\theta$, where $C_{\sin}$ is the recognition path action of the geodesic induced by the rotation and $\sin^2\theta$ is the squared initial amplitude on the sin branch.
background
This 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}=\frac{e^{-C_{\cos}}}{e^{-C_{\cos}}+e^{-C_{\sin}}}=\cos^2\theta,\qquad P_{\sin}=\frac{e^{-C_{\sin}}}{e^{-C_{\cos}}+e^{-C_{\sin}}}=\sin^2\theta.$$
The sin-branch action $C_{\sin}$ is the recognition path action $C[\gamma]=\int J(r(t)),dt$ of the path built from the rotation, so $e^{-C_{\sin}}$ is the RS path weight $w[\gamma]=\exp(-C[\gamma])$. Upstream, weight_equals_born already states that this path weight equals the squared initial amplitude: $w(\mathrm{pathFromRotation},\mathrm{rot})=|\alpha_2|^2=\sin^2\theta$. The present lemma simply names that equality in terms of $C_{\sin}$.
proof idea
Apply the bridge theorem weight_equals_born to the given rotation, obtaining pathWeight(pathFromRotation rot) = initialAmplitudeSquared rot. Unfold pathWeight (definitionally $\exp(-\mathrm{pathAction})$) and $C_{\sin}$ (definitionally pathAction of that same path) with simpa, which rewrites the goal to $\exp(-C_{\sin})=\sin^2\theta$.
why it matters
This is the sin-side half of the two-outcome Born certificate. Downstream, P_cos_eq and P_sin_eq rewrite both exponentials and cancel the common denominator $\cos^2\theta+\sin^2\theta=1$, yielding the normalized Born probabilities without any measurement-axiom typeclass. The module relies only on the proven C2A bridge and elementary trigonometry. In the broader RS picture this converts recognition path actions into the Born rule for a two-outcome projective measurement, a verification step rather than a new forcing-chain landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.