P_cos
plain-language theorem explainer
Defines the normalized Gibbs probability of the cos-branch for a two-branch rotation: exp(−C_cos) over the sum of both branch weights. Anyone citing the two-outcome Born certificate or the DFT-8 sector calibration uses this as the cos-side probability. The body is a direct quotient of the two exponential path weights; no proof obligations.
Claim. For a two-branch rotation $\mathrm{rot}$, the normalized cos-branch probability is $$P_{\cos}(\mathrm{rot}) = \frac{e^{-C_{\cos}(\mathrm{rot})}}{e^{-C_{\cos}(\mathrm{rot})}+e^{-C_{\sin}(\mathrm{rot})}},$$ where $C_{\cos}$ and $C_{\sin}$ are the complementary and sin-branch recognition actions.
background
The Two-Outcome Born Certificate module upgrades the two-branch measurement bridge from a bare path-weight identity (path weight equals $\sin^2\theta$) to normalized two-outcome probabilities. The sin-branch action $C_{\sin}$ is the recognition path action of the geodesic built from the rotation; its exponential weight is the RS path weight. The cos-branch action $C_{\cos}$ is the complementary cost $-2\log(\cos\theta)$, so $\exp(-C_{\cos})=\cos^2\theta$.
Normalization is the elementary Gibbs quotient of the two weights. The module deliberately avoids measurement-axiom typeclasses and relies only on the proven C2A bridge and elementary trigonometry. Related amplitude-normalization notions elsewhere (squared-norm one on finite amplitudes, Born-weight sums on FRS displays, QuantumLedger configuration probabilities) supply the broader Born-rule vocabulary this certificate feeds.
proof idea
Definitional, not a theorem. The body is the single quotient $\exp(-C_{\cos})/(\exp(-C_{\cos})+\exp(-C_{\sin}))$. Downstream equalities such as $P_{\cos}=\cos^2\theta$ unfold this definition and rewrite via the exponential identities for the two actions, then cancel with $\cos^2+\sin^2=1$.
why it matters
This is the cos-side normalized probability that the two-outcome Born certificate asserts equals $\cos^2\theta$. It is consumed by $P_{\cos_eq}$, by the certificate structure itself, and by the two-branch calibration theorem that equates DFT-8 sector measure on the two-branch signal with these Gibbs probabilities. That calibration is one of the four axioms in DFT-8 sector forcing and in the uniqueness theorem deriving the Born rule from J-cost structure on normalized Signal8 states (normalisation, phase invariance, additivity, two-branch calibration). In the Recognition framework it closes the measurement bridge without extra axioms, tying path-action weights to the Born rule on the eight-tick register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.