NullRecognitionModeCert
plain-language theorem explainer
Certificate type bundling three facts about the null recognition mode: some propagating mode has zero total cost, the canonical identity-ratio mode has zero cost, and every zero-cost mode is ratio-gauge equivalent to that canonical mode. Physicists citing the unique zero-cost eight-tick carrier use this as the formal package. It is a pure structure definition, not a proved theorem.
Claim. A certificate consists of three propositions: (i) there exists a propagating mode $M$ (an assignment of carrier events to each tick of the eight-tick cycle) with total recognition cost zero; (ii) the canonical null mode (identity ratio at every tick) has total cost zero; (iii) every propagating mode of total cost zero is gauge-equivalent to the canonical null mode, meaning it shares the same recognition ratio at every tick.
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 withholds photon, spin, and lightlike labels; those live downstream in Physics.PhotonAsZeroCostMode.
A PropagatingMode assigns a carrier event to each tick $i \in \mathrm{Fin},8$. Total mode cost sums the per-tick reciprocal recognition costs over the cycle. Gauge equivalence means equal recognition ratios at every tick. The canonical NRM is the constant identity-ratio assignment.
Upstream, total mode cost in the complex-structure forcing layer is $\sum_k J(|c_k|)$ and is phase-invariant under independent $U(1)$ rotations of each mode. Here the local total cost is the eight-tick sum of per-tick $J$-costs of the mode's ratios.
proof idea
No proof body: this is a structure definition whose three fields are propositions. Inhabitation is supplied separately by nullRecognitionModeCert, which fills the fields with nullRecognitionMode_nonempty, nrm_totalCost_zero, and zeroCostMode_unique_up_to_gauge. The uniqueness field is the theorem that any zero-cost mode has ratio one at every tick, hence matches the canonical NRM under gauge equivalence.
why it matters
This certificate is the formal interface for the NRM uniqueness package. Downstream, nullRecognitionModeCert inhabits it and nullRecognitionModeCert_inhabited records nonemptiness, so later physics modules can depend on a single named object rather than three scattered lemmas.
In the Recognition framework the NRM is the upstream recognition-theoretic carrier of the eight-tick octave (forcing landmark T7). Uniqueness up to ratio gauge is what licenses treating "the" null mode as a well-defined object before any photon identification. The module's restraint (no spin, polarization, or lightlike claims) keeps the certificate clean for the later photon-as-zero-cost-mode step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.