nullRecognitionMode_nonempty
plain-language theorem explainer
A zero-cost propagating mode exists on the eight-tick recognition cycle: some assignment of carrier events to the eight ticks has vanishing total recognition cost. Anyone building the null-recognition-mode certificate or the photon-as-zero-cost story cites this existence step. The proof is a one-line term witness: the canonical identity-ratio mode, already shown to have total cost zero.
Claim. There exists a propagating recognition mode $M$ (an assignment of a carrier event to each tick of the eight-tick cycle) such that the total recognition cost of $M$ over the cycle is zero: $\sum_{i\in\mathrm{Fin}\,8}\mathrm{perTickCost}(M,i)=0$.
background
The module isolates the null recognition mode (NRM) as the upstream recognition-theoretic object: 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 propagation); those live downstream in Physics.PhotonAsZeroCostMode.
A PropagatingMode is a map from the eight ticks (Fin 8) to carrier events. The total mode cost is the sum of per-tick reciprocal recognition costs over that cycle, built from the J-cost of Recognition Science (the unique cost forced by the Recognition Composition Law). The eight-tick period is the T7 octave of the forcing chain.
The canonical NRM places the identity ratio at every tick. An upstream lemma already records that this mode has total cost zero, by reducing the sum to eight vanishing per-tick costs.
proof idea
One-line term-mode existence proof. The witness is the canonical null recognition mode (identity ratio on every tick). The second component of the pair is the already-proved fact that the total mode cost of that canonical mode is zero (itself a Finset sum-to-zero argument via the per-tick cost lemma). No further tactics or case splits.
why it matters
Existence of a zero-cost mode is the first half of the NRM package: the module's certificate bundles this existence with the canonical zero-cost identity and uniqueness up to gauge. Downstream, zeroCostMode_nonempty is a backward-compatible alias that simply re-exports this theorem, and nullRecognitionModeCert records exists_nrm from it.
In the broader framework this is the recognition-side seed for the photon story without yet naming the photon: a free, zero-J propagating mode on the T7 eight-tick octave. Uniqueness up to ratio gauge and the later physical identification sit in sibling and downstream results; this declaration only closes non-emptiness of the zero-cost locus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.