nrm_totalCost_zero
plain-language theorem explainer
The canonical null recognition mode has vanishing total recognition cost on the eight-tick cycle. Existence and certificate constructions for zero-cost propagating modes cite this equality directly. The proof unfolds the mode-cost sum and invokes the already-proved per-tick vanishing lemma at every index.
Claim. The total recognition cost of the canonical null recognition mode equals $0$: summing the per-tick $J$-costs over the eight-tick register yields zero.
background
The module isolates the null recognition mode (NRM): the unique zero-cost propagating mode of the eight-tick recognition cycle, up to ratio-gauge equivalence. It deliberately withholds photon labels (spin, polarization, lightlike kinematics); those live in a downstream photon module.
Mode cost is the sum of the Recognition Science $J$-cost over the eight mode amplitudes. Upstream, the same pattern appears as total mode cost $\sum_k J(|c_k|)$ on an eight-component signal, with $J$ the unique cost forced by the Recognition Composition Law (T5). The canonical NRM is the distinguished representative whose per-tick costs already vanish.
Local siblings supply the carrier and propagating-mode types, the per-tick cost functional, gauge equivalence, and the canonical NRM together with its ratio and per-tick lemmas.
proof idea
Term-style tactic proof. Unfold the total mode cost definition to a finite sum over the eight-tick index set. Apply Finset.sum_eq_zero, then for each index invoke the sibling lemma that the canonical NRM has zero per-tick cost. No further algebraic work: the sum of zeros is zero.
why it matters
This is the cost half of the NRM package. Downstream, the existence theorem packages the canonical NRM with this equality as a witness that a zero-cost propagating mode exists. The backward-compatible zero-mode cost theorem is a one-line rename of the same fact. The certificate structure records it as the canonical zero-cost field alongside existence and uniqueness-up-to-gauge.
In the forcing chain this sits on the eight-tick octave (T7): a propagating mode on the $2^3$-period register whose total $J$-cost is exactly zero. The module stops short of identifying the mode with the photon; the zero-cost property is the recognition-theoretic input that the photon module later interprets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.