twoBranchSignal
plain-language theorem explainer
Embeds a two-branch measurement rotation into the eight-mode signal by placing cos θ_s on mode 0, sin θ_s on mode 1, and zero on the other six modes. Cited by anyone calibrating the DFT-8 sector measure against the two-outcome Born rule or proving uniqueness of μ(S)=Σ‖ψ_k‖². The body is a direct piecewise assignment on Fin 8.
Claim. Given a two-branch rotation with starting angle $\theta_s\in(0,\pi/2)$, define the eight-mode complex signal by $\psi_0=\cos\theta_s$, $\psi_1=\sin\theta_s$, and $\psi_k=0$ for all other modes $k\in\{2,\ldots,7\}$.
background
The module forces the Born rule on eight-mode signals: the unique probability measure that is normalised, phase-invariant, additive on disjoint mode sets, and consistent with the two-branch exp(−C) calibration is $\mu(S)=\sum_{k\in S}|\psi_k|^2$. By Parseval the same formula holds in the DFT-8 frequency basis.
A TwoBranchRotation packages a starting angle $\theta_s\in(0,\pi/2)$ and a positive duration $T$; it is the geometric data of a two-outcome quantum measurement geodesic. Signal8 is the complex eight-mode state space forced by the eight-tick octave (T7) and complex-structure forcing. The two-branch calibration identities $P_{\cos}$ and $P_{\sin}$ come from TwoOutcomeBornCert.
This definition is the concrete bridge that places that geodesic inside Signal8 so the sector measure can be evaluated on single-mode sets ${0}$ and ${1}$.
proof idea
Pure definition, not a proof. On input rot, return the function $k\mapsto$ Complex.ofReal(cos rot.θ_s) if $k=0$, Complex.ofReal(sin rot.θ_s) if $k=1$, and $0$ otherwise. No lemmas are applied; the piecewise if on Fin 8 is the entire construction.
why it matters
This embedding is the test state for the two-branch calibration half of Born-rule forcing. Downstream, twoBranchSignal_normalized shows $\cos^2\theta+\sin^2\theta=1$; sector_matches_cos_branch and sector_matches_sin_branch identify the singleton sector measures with $\cos^2\theta$ and $\sin^2\theta$; sector_matches_gibbs_born equates those to the exp(−C) Gibbs probabilities $P_{\cos}$ and $P_{\sin}$. Those identities feed dft8_sector_forcing (the unique measure theorem in this module) and the quantum-layer theorem born_rule_from_jcost.
In the Recognition chain it closes the Born-rule gap flagged in the module registry, using the eight-tick octave (T7), J-cost structure (T5), and the measurement mechanism F-009. Without this concrete two-mode state, the sector measure cannot be matched to the certified two-outcome Born rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.