IndisputableMonolith.Verification.TwoOutcomeBornCert
Certificate module for the two-outcome Born rule on a two-branch geodesic. Complementary recognition costs C_cos and C_sin obey exp(-C_cos)=cos²(θ_s) and exp(-C_sin)=sin²(θ_s), so the normalized weights are the Born probabilities. Born-rule forcing and RecogSpec import this package. The argument is algebraic: C=2A plus the residual rate action A=-ln(sin θ_s) and its cosine complement.
claimOn a two-branch measurement geodesic with selection angle $\theta_s$, define complementary recognition costs $C_{\cos}$ and $C_{\sin}$ via the $C=2A$ bridge. Then $e^{-C_{\cos}}=\cos^2\theta_s$ and $e^{-C_{\sin}}=\sin^2\theta_s$, and the normalized probabilities $P_{\cos}$, $P_{\sin}$ equal those Born weights.
background
Local-Collapse models a binary quantum measurement as a two-branch geodesic rotation. The residual norm is the geodesic length $|R|=\pi/2-\theta_s$, and the residual-model rate action is $A=-\ln(\sin\theta_s)$ (TwoBranchGeodesic). The C=2A bridge equates recognition cost to twice that action on any such geodesic: $C=2A$ exactly (C2ABridge).
This verification module packages the cosine complement of that identity. With $C_{\sin}=2A=-2\ln(\sin\theta_s)$ one gets $e^{-C_{\sin}}=\sin^2\theta_s$. The complementary cost $C_{\cos}$ is defined so that $e^{-C_{\cos}}=\cos^2\theta_s$. The resulting $P_{\cos}$ and $P_{\sin}$ are the normalized two-outcome Born weights.
Sibling definitions expose the raw costs ($C_{\cos}$, $C_{\sin}$), the probabilities ($P_{\cos}$, $P_{\sin}$), the exponential identities, and a bundled certificate TwoOutcomeBornCert.
proof idea
Definition-and-identity module, not a deep proof development. Costs are introduced from the upstream rate action via $C=2A$. The sine identity is immediate: $C_{\sin}=-2\ln(\sin\theta_s)$ yields $e^{-C_{\sin}}=\sin^2\theta_s$. The cosine side is the complementary action stated in the module doc, giving $e^{-C_{\cos}}=\cos^2\theta_s$. Probability aliases $P_{\cos}$, $P_{\sin}$ are those exponentials (already normalized on a binary outcome). Equalities are recorded as named lemmas; the bundle TwoOutcomeBornCert packages them for importers.
why it matters in Recognition Science
BornRuleForcing needs a concrete two-branch exp(-C) rule before it can force the unique DFT-8 sector measure. Its hypotheses require a probability measure that is normalised, phase-invariant, additive on disjoint modes, and "consistent with the two-branch exp(−C) Born rule"; this module supplies that two-branch anchor. RecogSpec.Spec also imports the certificate so the external specification surface can cite verified Born weights rather than an informal claim.
In the broader RS chain, the eight-tick octave (T7) and sector measure sit downstream of this binary case: once exp(-C) matches cos²/sin² on a geodesic, the multi-mode forcing argument can extend uniqueness. Without the C=2A bridge and the residual action $A=-\ln(\sin\theta_s)$, the cost-to-Born step would remain heuristic.
scope and limits
- Does not derive the multi-mode or DFT-8 Born measure; only the binary geodesic case.
- Does not prove C=2A or A=-ln(sin θ_s); those are imported from upstream modules.
- Does not address phase dependence, decoherence, or continuous-outcome POVMs.
- Does not fix units or identify θ_s with a laboratory angle beyond the geometric model.