PropagatingMode
plain-language theorem explainer
A propagating recognition mode is an assignment of one positive carrier ratio to each tick of the eight-tick cycle. It is the bare data type underlying the null recognition mode (NRM): zero-cost modes, gauge equivalence, and uniqueness live on this type. The declaration is a pure structure with a single field, no proof content.
Claim. A propagating recognition mode is a map $M : \{0,\ldots,7\} \to \mathbb{R}_{>0}$ that assigns a positive recognition ratio to each tick of the eight-tick recognition cycle.
background
The module isolates the null recognition mode as the unique zero-cost propagating mode of the eight-tick cycle, up to ratio-gauge equivalence. It deliberately withholds photon labels (spin, polarization, lightlike kinematics); those sit in a downstream photon module.
A carrier event is a single positive real ratio at one tick. The eight-tick period is the fundamental RS evolution window (one octave, period $2^3$), matching the T7 landmark of the forcing chain. Cost is measured by the J-cost on ratios: per-tick cost is $J$ of the mode's ratio at that tick, and total mode cost sums over the eight ticks.
Upstream cost and reciprocal infrastructure (CostAlgebra, LedgerForcing reciprocal events, multiplicative-recognizer derived cost) supply the $J$-based accounting used once modes are defined; this structure itself only packages the eight ratios.
proof idea
No proof: pure structure definition. One field event of type Fin 8 → CarrierEvent, where each carrier event is a positive real ratio. Downstream defs (canonical NRM, per-tick and total cost, gauge equivalence) pattern-match on this field.
why it matters
This is the carrier type for the entire NRM development. Downstream, the canonical NRM is the constant-identity mode; gauge equivalence is pointwise equality of ratios; per-tick and total costs are $J$ applied to those ratios. Existence of a zero-cost mode, nonnegativity of per-tick cost, vanishing of every tick when the total vanishes, and uniqueness up to gauge (every zero-cost mode matches the canonical NRM) are all stated on this type and packaged in the NRM certificate.
In the framework it is the recognition-theoretic precursor to a photon: the unique zero-cost eight-tick mode before physical labels are attached. It sits on the T7 eight-tick octave and feeds the zero-cost uniqueness story that later modules interpret as lightlike free propagation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.