zeroMode_totalCost
plain-language theorem explainer
The zero-cost propagating mode on the eight-tick cycle has total recognition cost exactly zero. Cite this when working with null recognition modes or the later photon-as-zero-cost identification. The proof is a one-line term alias of the canonical NRM cost theorem.
Claim. The total recognition cost of the zero mode equals zero: if $m$ is the zero mode of the eight-tick cycle, then $\sum_{i \in \mathbb{F}_8} c(m,i) = 0$, where $c(m,i)$ is the per-tick recognition cost.
background
The null recognition mode (NRM) is the upstream recognition-theoretic object: the unique zero-cost propagating mode of the eight-tick recognition cycle, up to ratio-gauge equivalence. This module deliberately does not call the mode a photon and does not attach spin, polarization, or lightlike labels; those live in the photon-as-zero-cost module.
Total mode cost here is the sum of per-tick recognition costs over the eight ticks. Upstream, the foundation mode-cost is $\sum_k J(|c_k|)$ in the mode basis (phase-invariant under independent $U(1)$ rotations per mode). The eight-tick period is the T7 octave in the forcing chain.
The sibling result already proves that the canonical NRM has total cost zero by showing each per-tick cost vanishes. The zero mode is the backward-compatible name for that same object.
proof idea
One-line term proof: the statement is definitionally the same as the canonical NRM total-cost theorem, so the proof is just that theorem. Upstream, that result unfolds the eight-tick sum and applies the per-tick vanishing lemma at each index.
why it matters
Gives a stable, backward-compatible name for the fact that the zero mode carries zero total recognition cost. That fact is the cost half of the NRM story: a propagating mode on the eight-tick cycle (T7) with vanishing J-cost, before any photon labeling.
No downstream dependents are wired in the current graph; the natural landing site is the photon-as-zero-cost development, which is intentionally separated so this module stays label-free. The companion existence remark in the file ("a null recognition mode exists") sits next to this cost identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.