P_sin
plain-language theorem explainer
Normalized Gibbs probability for the sin branch of a two-branch measurement rotation. It is exp of minus the RS path action, divided by the sum of both branch weights, and equals sin squared of the starting angle once the bridge identities fire. Cited by the two-outcome Born certificate and by sector-calibration lemmas that force the Born rule from J-cost structure. Pure definitional packaging of the normalized path weight.
Claim. For a two-branch rotation with starting angle $\theta_s\in(0,\pi/2)$, the normalized sin-branch probability is $P_{\sin}=e^{-C_{\sin}}/(e^{-C_{\cos}}+e^{-C_{\sin}})$, where $C_{\sin}$ is the recognition path action along the geodesic from $\theta_s$ to $\pi/2$ and $C_{\cos}=-2\log\cos\theta_s$.
background
The module upgrades the two-branch measurement bridge from a raw weight identity (path weight equals $\sin^2\theta$) to normalized two-outcome probabilities. No measurement-axiom typeclass is used; only the proven C2A bridge and elementary trig identities.
A TwoBranchRotation packages a starting angle $\theta_s\in(0,\pi/2)$ and a positive duration $T$. The complementary action $C_{\cos}=-2\log\cos\theta_s$ is chosen so that $\exp(-C_{\cos})=\cos^2\theta_s$. The RS action $C_{\sin}$ is the path action of the geodesic built from the rotation, so $\exp(-C_{\sin})$ is the RS path weight, already known to equal $\sin^2\theta_s$ via the measurement bridge.
The sibling $P_{\cos}$ is the same Gibbs form with the cos weight in the numerator. Together they form a two-outcome probability pair that the certificate later equates to $(\cos^2\theta_s,\sin^2\theta_s)$.
proof idea
Definitional, not a proof. The body is the standard two-outcome Gibbs normalization: numerator $\exp(-C_{\sin},\mathrm{rot})$, denominator the sum of $\exp(-C_{\cos},\mathrm{rot})$ and $\exp(-C_{\sin},\mathrm{rot})$. Downstream theorems (P_sin_eq, the exp-neg identities) discharge the equality to $\sin^2\theta_s$ by unfolding this def and simplifying with $\cos^2+\sin^2=1$.
why it matters
This is the sin half of the normalized two-outcome Born certificate. Downstream, P_sin_eq proves it equals the initial amplitude squared, and the certificate structure packages both branches as a verification predicate.
Foundation consumers use it for two-branch calibration: sector_matches_gibbs_born equates DFT-8 sector measures on a two-branch signal to $(P_{\cos},P_{\sin})$. That calibration is one of the four axioms in dft8_sector_forcing and in born_rule_from_jcost, which uniquely force the Born rule $\mu(S)=\sum_{k\in S}|\psi_k|^2$ from J-cost structure on normalized eight-tick signals. It therefore sits on the path from the recognition action to the Born rule without external measurement postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.