twoBranchSignal_normalized
plain-language theorem explainer
The two-branch embedding of a rotation angle places cos θ on mode 0 and sin θ on mode 1 of an eight-mode signal (zeros elsewhere) and has total squared-norm mass one. Anyone calibrating the DFT-8 sector measure against the two-outcome Born rule cites this normalisation. The proof collapses the eight-term sum by Fin-case distinctions and finishes with the Pythagorean identity.
Claim. For every two-branch rotation angle $\theta$, the eight-mode signal with $\cos\theta$ on mode $0$, $\sin\theta$ on mode $1$, and zero on modes $2, \ldots,7$ is normalised: $\sum_{k=0}^{7}\|\psi_k\|^2 = 1$.
background
This module forces the Born rule on eight-mode signals: the unique probability on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and consistent with the two-branch exp(−C) calibration is μ(S)=Σ_{k∈S}‖ψ_k‖² (equivalently the Parseval form in the DFT-8 basis). The setting rests on ComplexStructureForcing (Signal8, inner product, DFT-8, Parseval) and the two-outcome certificates P_cos_eq / P_sin_eq.
A signal ψ : Fin 8 → ℂ is normalised when Σ_k ‖ψ k‖² = 1. The two-branch embedding builds the elementary calibration state: real cos θ on mode 0, real sin θ on mode 1, and zero on the other six modes. That state is the bridge from the classical two-outcome Born rule into the eight-tick sector measure. The eight-mode lattice itself is the T7 octave (period 2³) of the forcing chain.
proof idea
Unfold normalisation and the two-branch embedding, then expand the Fin-8 sum. A block of decide facts separates indices 0 and 1 from {2,…,7}. After simplifying the if-then-else branches, the six off-support terms vanish by norm_zero and zero_pow / add_zero. The two surviving terms reduce via norm_ofReal_sq to cos²θ and sin²θ. linarith with Real.sin_sq_add_cos_sq closes the identity.
why it matters
Without this fact the two-branch calibration state is not a legal input to the sector measure, so the uniqueness theorem for μ(S)=Σ‖ψ_k‖² cannot fire. The module doc states that the development closes the Born-rule gap (replacing trivial placeholders) and depends on T5 (J-uniqueness), T7 (eight-tick octave), T8 (D=3), and the measurement mechanism F-009. The theorem supplies the missing normalisation step that lets the two-outcome certificates sit inside the DFT-8 probability calculus. No downstream consumers are wired yet in the graph; the immediate parent is the sector-measure uniqueness argument in this same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.