zeroMode
plain-language theorem explainer
Short alias for the canonical null recognition mode: the eight-tick propagating mode with identity ratio at every tick. Downstream lemmas on ratio and total cost cite this name for backward compatibility. The body is a pure abbreviation of the canonical NRM definition.
Claim. Write $\mathrm{zeroMode}$ for the canonical null recognition mode: the propagating mode on the eight-tick cycle whose carrier event at every tick has ratio $1$.
background
The module isolates the null recognition mode (NRM) as 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 kinematics); those live in a separate photon module.
A propagating mode assigns a carrier event to each tick of the eight-tick cycle ($\mathrm{Fin},8$). The canonical NRM is the mode whose event at every tick is the identity-ratio carrier. The eight-tick period is the T7 landmark of the forcing chain (period $2^3$).
This declaration is only a backward-compatible short name for that canonical object.
proof idea
Definitional abbreviation: zeroMode is definitionally equal to canonicalNRM, which itself is the structure with event := fun _ => ⟨1, _⟩. No proof obligations beyond the carrier-event well-formedness already discharged in the canonical definition.
why it matters
Gives a stable short name used by the simp lemma that every tick has ratio $1$, and by the total-cost theorem that the mode costs zero (via the canonical zero-cost result). Those facts underwrite existence of a null recognition mode in the eight-tick cycle without committing to photon phenomenology. In the broader RS chain this is the zero-cost seed later specialized when the photon is identified as a zero-cost mode; here it stays purely recognition-theoretic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.