perTickCost_zero_of_total_zero
plain-language theorem explainer
If a propagating mode on the eight-tick cycle has vanishing total recognition cost, then the cost on every individual tick is zero. Cited when characterizing the null recognition mode and when forcing every tick ratio to the identity. The proof is a nonnegativity-plus-sum argument: the total is the sum of eight nonnegative per-tick costs, so each term vanishes.
Claim. Let $M$ be a propagating recognition mode on the eight-tick cycle. If the total mode cost of $M$ is zero, then for every tick index $i \in \{0,\ldots,7\}$ the per-tick reciprocal recognition cost of $M$ at $i$ is 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 avoids photon labels; those live downstream in PhotonAsZeroCostMode.
A PropagatingMode assigns a carrier event to each tick of the Fin 8 cycle. The per-tick cost is the reciprocal recognition cost (J-cost style) of that tick's event; the total mode cost is the sum of those eight contributions. The eight-tick period is the T7 octave of the forcing chain: one full recognition cycle has length $2^3$.
Nonnegativity of the underlying cost (J-cost / derived recognizer cost) is the key structural fact: each per-tick term is $\ge 0$, so a vanishing sum forces every summand to zero.
proof idea
Rewrite the hypothesis as $\sum_{j:\mathrm{Fin},8}\mathrm{perTickCost}(M,j)=0$. Establish pointwise nonnegativity via perTickCost_nonneg. Apply Mathlib's Finset.sum_eq_zero_iff_of_nonneg to conclude every summand is zero, then specialize to the given index $i$ (which is in the universe finset).
why it matters
This is the first half of the NRM zero-cost characterization. The immediate parent is ratio_eq_one_of_total_zero, which unfolds per-tick cost and invokes $J=0\Leftrightarrow$ ratio $=1$ to force every tick onto the identity ratio. Together they pin the unique zero-cost mode (up to gauge) that the module treats as the upstream recognition-theoretic object behind massless propagation.
Framework landmarks: T7 eight-tick octave (the Fin 8 sum), and the J-cost nonnegativity/uniqueness line (T5) that makes vanishing cost mean identity ratio. Without this lemma, total-cost zero would not pass to the pointwise identity-ratio statement used to define and uniqueness-argue the canonical NRM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.