zeroMode_ratio
plain-language theorem explainer
For every index in the eight-tick cycle, the zero mode's carrier event has recognition ratio exactly 1. Anyone working with null recognition modes or zero-cost propagation cites this as the defining ratio property of the zero mode. The proof is pure reflexivity from the definition of that mode.
Claim. For every tick index $i \in \{0,\ldots,7\}$, the ratio of the $i$-th carrier event of the zero mode equals $1$.
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.
A propagating mode assigns to each of the eight ticks a carrier event with a positive real ratio. Recognition cost is built from the J-cost of those ratios (the doubled J-cost under a ratio weight). The zero mode is the constant-ratio-1 assignment on the cycle. The fundamental time quantum is one tick ($\tau_0 = 1$), and one octave is eight ticks, matching the T7 eight-tick period in the forcing chain.
Upstream cost infrastructure (rung coarsening, multiplicative recognizer cost, observer forcing) supplies the same ratio-to-cost map used when later lemmas show that ratio 1 yields vanishing per-tick and total mode cost.
proof idea
One-line term proof by rfl. The zero mode is defined so that every tick's event has ratio definitionally equal to 1; the statement is that definitional equality, marked @[simp] for downstream rewriting.
why it matters
This pins the ratio content of the zero mode inside the NRM package: constant ratio 1 on the eight-tick octave (T7). Sibling results (canonicalNRM_ratio, zeroMode_totalCost, nrm_totalCost_zero, canonicalNRM_perTickCost) build the zero-cost claim from this identity and the J-cost normalization $J(1)=0$.
No used_by edges are recorded yet; the lemma is infrastructure for the NRM uniqueness-up-to-gauge story and for the later identification of the photon as a zero-cost mode. It does not itself force uniqueness or physical labels; it only freezes the ratio field of the named zero mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.