totalModeCost
plain-language theorem explainer
Defines the total recognition cost of a propagating mode as the sum of its eight per-tick costs over one octave. Anyone proving that the null recognition mode is uniquely zero-cost, or bridging NRM into the complex-structure and Hamiltonian forcing chain, cites this scalar. The body is a one-line Fin-8 sum of the sibling per-tick cost.
Claim. For a propagating mode $M$ (a map from each of the eight ticks to a carrier event), the total recognition cost is $\mathrm{cost}(M) := \sum_{i=0}^{7} c_{\mathrm{tick}}(M,i)$, where $c_{\mathrm{tick}}(M,i)$ is the reciprocal recognition cost of $M$ at tick $i$.
background
The Null Recognition Mode module isolates the unique zero-cost propagating mode of the eight-tick recognition cycle, up to ratio-gauge equivalence. It deliberately avoids photon labels (spin, polarization, lightlike rays); those live downstream in PhotonAsZeroCostMode.
A propagating mode assigns a carrier event to every slot of the octave $\mathrm{Fin},8$. The sibling per-tick cost is the reciprocal recognition cost of that event at a fixed tick. The fundamental time quantum is one tick ($\tau_0 = 1$), and one octave is eight ticks, matching the T7 eight-tick period forced in the unified chain.
A parallel total-mode-cost in ComplexStructureForcing sums $J$-costs of mode amplitudes, $\sum_k J(|c_k|)$. The present definition is the NRM-side analogue: sum of per-tick reciprocal costs rather than $J$ of DFT coefficients.
proof idea
Pure definition, not a theorem. The right-hand side is the finite sum $\sum_{i:\mathrm{Fin},8} \mathrm{perTickCost}, M, i$. No lemmas are applied; evaluation reduces by unfolding the sum and the per-tick cost on a concrete mode (e.g. the canonical NRM or the zero mode).
why it matters
This scalar is the cost functional that the null recognition mode is required to annihilate. Downstream, nrm_totalCost_zero and zeroMode_totalCost use it to certify zero total cost. The same name appears in ComplexStructureForcing as the mode-basis $J$-sum that is phase-invariant and feeds UnitaryEvolution (cost non-increasing plus inner-product preservation).
In the forcing chain it sits under T5–T7 bridges: ComplexStructureCertificate packages eight-tick periodicity, imaginary eigenvalue of the shift, DFT unitarity, and cost-phase invariance; T5_T7_To_CanonicalHamiltonian_Bridge and T7_To_CanonicalCarrier_Bridge pull the octave cost into Hamiltonian and carrier emergence. Landmark alignment: T7 eight-tick octave and the $J$-cost uniqueness (T5) that makes zero total cost a sharp selection principle for the NRM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.