nullRecognitionModeCert
plain-language theorem explainer
Packages existence of a zero-cost propagating mode, zero total cost of the canonical null recognition mode, and uniqueness up to ratio-gauge into one certificate. Anyone citing the NRM as the unique zero-cost mode on the eight-tick cycle uses this object. The body is a structure instance that wires three already-proved theorems; no new math is done here.
Claim. A certificate record asserting three facts: there exists a propagating mode $M$ with total recognition cost zero; the canonical null recognition mode has total cost zero; and every propagating mode with total cost zero is ratio-gauge equivalent to the canonical null recognition mode.
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 a positive real ratio at each tick of the cycle. Per-tick cost is the J-cost of that ratio; total mode cost sums over the eight ticks. Gauge equivalence means the two modes have identical ratios tickwise (ratio-gauge). The canonical NRM is the constant-ratio-one mode, whose per-tick costs vanish.
Upstream, nrm_totalCost_zero shows the canonical mode has total cost zero by summing zero per-tick costs. Existence follows by exhibiting that mode. Uniqueness up to gauge reduces zero total cost to each tick ratio equaling one.
proof idea
One-line structure instance. Field exists_nrm is filled by the existence theorem that packages the canonical mode with its zero-cost proof. Field canonical_zero_cost is the direct theorem that total cost of the canonical NRM is zero. Field unique_up_to_gauge is the uniqueness theorem: any zero-cost mode is gauge-equivalent to the canonical NRM, proved by reducing total cost zero to ratio one at each tick. No tactics run at this declaration; it only assembles those three results.
why it matters
This certificate is the module's exportable claim bundle for the NRM story. Downstream, nullRecognitionModeCert_inhabited simply wraps it to give Nonempty NullRecognitionModeCert, the usual inhabitance witness for certificate-style APIs.
In the Recognition framework the NRM sits on the eight-tick octave (forcing step T7): a period-$2^3$ recognition cycle whose unique zero-cost propagating mode is the upstream object later identified with the photon in a separate module. Keeping the certificate free of spin and lightlike labels keeps the cost-theoretic uniqueness clean before physical interpretation is attached.
Anyone proving photon-as-zero-cost-mode results, or citing uniqueness of the free massless mode in RS units, depends on this packaged triple rather than on the three lemmas separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.