totalModeCost
plain-language theorem explainer
Re-export of the total mode-basis recognition cost: for an eight-tick complex signal, sum J of the modulus of each Fourier mode coefficient. Cited wherever cost-phase invariance, unitary evolution, or the complex-structure certificate needs a scalar cost on Signal8. The body is a pure alias of the Foundation definition; no new proof.
Claim. For a signal $f : \mathrm{Fin}\,8 \to \mathbb{C}$, the total mode cost is $\sum_{k=0}^{7} J(\lVert f(k)\rVert)$, where $J$ is the unique cost $J(x)=\cosh(\ln x)-1$.
background
In the complex-structure forcing layer, the canonical carrier forced by the eight-tick period is $\mathrm{Signal8} = \mathrm{Fin},8 \to \mathbb{C}$. Modes are the values $f(k)$ in that basis (equivalently DFT coefficients of a cyclic eight-tick signal).
The scalar cost on a mode is the Recognition Science $J$-cost of its modulus: $J(x) = \cosh(\ln x) - 1$, uniquely fixed by the cost axioms (forcing step T5). Summing over the eight modes gives a single real number, the total mode cost. Because $J$ depends only on modulus, independent $U(1)$ phases on each mode leave the sum unchanged.
This module's OperatorCore layer re-exports that Foundation definition so downstream certificates and bridges can name the cost without a long qualified path. A sibling notion in NullRecognitionMode sums per-tick costs on a propagating mode; the present alias is the mode-basis $\sum J(\lVert c_k\rVert)$ version.
proof idea
No proof: the declaration is an abbrev that points at Foundation.ComplexStructureForcing.totalModeCost, whose body is the finite sum $\sum_{k:\mathrm{Fin},8} J(\lVert f,k\rVert)$. All mathematical content lives at that target definition.
why it matters
The total mode cost is the scalar that makes complex structure and unitary dynamics cost-forced. Downstream, mode_cost_phase_invariant shows rotating each mode by an independent phase leaves the sum fixed, i.e. a $U(1)^8$ gauge symmetry on the cost landscape. UnitaryEvolution requires cost non-increasing together with inner-product preservation, which jointly force unitarity on $\mathbb{C}^8$.
ComplexStructureCertificate packages this with eight-tick periodicity, the imaginary eigenvalue of the cyclic shift, and DFT unitarity: the master claim that cost plus eight-tick forces complex structure (T5–T8 chain). UnifiedForcingChain bridges T7_To_CanonicalCarrier_Bridge and T5_T7_To_CanonicalHamiltonian_Bridge name the same cost when linking the eight-tick carrier and the small-deviation Hamiltonian $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$.
NullRecognitionMode certificates reuse the name for zero total cost of a null mode. Without this scalar, phase invariance and admissible evolution have nothing to minimize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.