IsNormalized
plain-language theorem explainer
A DFT-8 signal is normalized when the sum of squared mode norms equals one. Born-rule forcing cites this as the unit-mass hypothesis on the eight-tick register. The definition is a one-line Prop: total ℓ² mass of ψ equals 1. Downstream sector-measure lemmas take it as the standing assumption that total probability is one.
Claim. A signal $\psi \in \mathbb{C}^8$ (an eight-mode recognition register) is normalized when $\sum_{k \in \mathrm{Fin}\,8} \|\psi_k\|^2 = 1$.
background
The module forces the Born rule on the eight-mode register: the unique probability on mode-sets that is normalized, phase-invariant, additive on disjoint sectors, and consistent with the two-branch exp(−C) calibration is μ(S) = Σ_{k∈S} ‖ψ_k‖². By Parseval the same mass is read in the DFT-8 frequency basis.
Signal8 is the complex 8-vector type from ComplexStructureForcing (inner product inner8, DFT-8, phase rotation). Normalization here is ordinary unit ℓ² mass on that register, not the cost-function condition F(1)=0 used in the T5 J-uniqueness chain. The eight modes are the T7 octave (period 2³) forced with D=3.
Sibling sectorMeasure assigns to each mode-set S the sum of ‖ψ_k‖² over k∈S and is proved non-negative, at most one, and total-mass one on normalized signals.
proof idea
Pure definition: the predicate is the equality ∑_{k:Fin 8} ‖ψ k‖² = 1. No tactics or lemmas. Downstream proofs unfold it (or simpa [IsNormalized]) when they need total mass one, e.g. sectorMeasure_total and the uniqueness argument for the sector measure.
why it matters
This is the standing unit-mass hypothesis for Born-rule forcing on the DFT-8 register. The module theorem states that the unique measure meeting normalization, phase invariance, additivity, and two-branch exp(−C) calibration is exactly the sum of squared norms; without IsNormalized the total-mass clause is undefined.
It closes the Born-rule gap flagged in the module registry (replacing trivial placeholders) and sits on T7 (eight-tick octave) together with the ComplexStructureForcing and TwoOutcomeBornCert imports. Sibling lemmas (sectorMeasure_nonneg, sectorMeasure_le_one, sectorMeasure_total, sectorMeasure_phase_invariant) all quantify over normalized signals. Framework-wise it is the probability side of the measurement mechanism (F-009), parallel to QuantumLedger.probability = Complex.normSq on amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.