sector_matches_sin_branch
plain-language theorem explainer
For a two-branch rotation that places cos θ on DFT-8 mode 0 and sin θ on mode 1, the Born sector measure on the singleton {1} equals sin²θ (the squared initial amplitude of that branch). Anyone matching the eight-mode sector measure to the two-outcome Born calibration cites this identity. The proof is a short simplification: singleton reduction, branch embedding, and the real-embedding norm-square lemma.
Claim. Let a two-branch rotation have angle $\theta$. Embed the state with $\cos\theta$ on mode $0$, $\sin\theta$ on mode $1$, and zero on the other six DFT-8 modes. Then the sector measure of that state on the singleton mode set $\{1\}$ equals $\sin^2\theta$, i.e. the squared initial amplitude of the sine branch.
background
The module forces the Born rule on eight-mode signals: the unique probability on mode sectors that is normalised, phase-invariant, additive on disjoint mode sets, and consistent with the two-branch exp(−C) calibration is μ(S) = Σ_{k∈S} ‖ψ_k‖². By Parseval the same formula holds in the DFT-8 frequency basis.
Sector measure is exactly that sum of squared moduli over a Finset of Fin 8 indices. The two-branch embedding places Real.cos θ as a real complex on mode 0 and Real.sin θ on mode 1, with zeros elsewhere; it is already normalised because cos²θ + sin²θ = 1. The singleton lemma collapses the sum on {k} to a single ‖ψ k‖² term. A private norm identity states ‖Complex.ofReal r‖² = r².
Upstream calibration lives in TwoOutcomeBornCert (P_cos_eq, P_sin_eq). The local setting depends on ComplexStructureForcing (Signal8, inner product, DFT-8, Parseval, phase invariance) and on the eight-tick octave (T7) that fixes the mode count at 8.
proof idea
Decide that (1 : Fin 8) ≠ 0, so the embedding lands on the sine branch rather than the cosine branch. Then simp with the singleton identity (sector measure on {k} is ‖ψ k‖²), the definition of the two-branch embedding, the inequality just proved (so the if-then-else selects sin θ), the definition of initial amplitude squared, and the real-embedding norm-square lemma. The goal reduces to sin²θ = sin²θ.
why it matters
This is one half of the two-branch calibration that feeds sector_matches_gibbs_born: that parent theorem asserts sector measure on {0} equals P_cos and on {1} equals P_sin, by rewriting through the cosine and sine branch identities and the TwoOutcomeBornCert equalities. Together they close the Born-rule gap flagged in the module registry (replacing trivial True placeholders) and discharge consistency condition (4) of the uniqueness theorem for the eight-mode sector measure.
Framework landmarks: T7 (eight-tick octave) fixes the mode lattice; the measure is the unique one compatible with phase invariance and the exp(−C) Gibbs form already proved for two outcomes. Downstream the same μ is identified, via Parseval, with the frequency-basis Born weights used in measurement mechanism F-009.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.