totalModeCost
plain-language theorem explainer
Defines the total recognition cost of an eight-tick signal in the DFT mode basis as the sum of J-costs of the eight mode moduli. Anyone proving phase invariance, unitary evolution, or the complex-structure certificate cites this scalar. The body is a direct finite sum of Cost.Jcost on complex norms; no proof obligations.
Claim. For a signal $f:\mathrm{Fin}\,8\to\mathbb{C}$ on the eight-tick cycle, the total mode cost is $\sum_{k=0}^{7} J(\|f(k)\|)$, where $J(x)=(x+x^{-1})/2-1$ is the unique recognition cost on positive reals.
background
The module Complex Structure Forcing shows that the eight-tick shift cannot be diagonalized over $\mathbb{R}$, so complexification is algebraically forced. A signal is a map $f:\mathrm{Fin},8\to\mathbb{C}$; the DFT-8 puts it in the eigenbasis of the cyclic shift $T$ with $T^8=I$.
The recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique functional fixed by the cost axioms (T5). It depends only on positive real ratios. Applying $J$ to each mode modulus $|f(k)|$ and summing yields a single real scalar that measures total recognition cost in the mode basis.
This scalar is the cost side of the later claim that cost is phase-invariant and that admissible evolutions (norm-preserving and cost non-increasing) are unitary.
proof idea
Definition only: expand as the finite sum $\sum_{k:\mathrm{Fin},8}\mathrm{Cost.Jcost},|f,k|$. No lemmas are applied; noncomputable because complex norm and $J$ are.
why it matters
This is the cost functional that makes the complex Hilbert-space story quantitative. Downstream, mode_cost_phase_invariant proves $U(1)^8$ gauge invariance of the sum, and UnitaryEvolution packages norm preservation plus cost non-increase as the admissibility conditions that force unitarity.
ComplexStructureCertificate lists cost_phase_invariant as one of its fields, closing the registry gap "Complex Hilbert space from cost" after T5 (J-uniqueness), T7 (eight-tick), and T8 ($D=3$). The same scalar is re-exported in OperatorCore and appears in the UnifiedForcingChain bridges T5_T7_To_CanonicalHamiltonian_Bridge and T7_To_CanonicalCarrier_Bridge, and in NullRecognitionMode certificates that demand vanishing total cost.
Without a mode-basis cost, phase invariance and the unitary-forcing step have nothing to act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.