CarrierEvent
plain-language theorem explainer
A carrier event is one tick's payload: a positive real recognition ratio with an explicit positivity witness. Anyone building propagating modes or the null recognition mode cites it as the atomic slot type on the eight-tick cycle. It is a bare structure definition, so there is no proof content beyond the field types.
Claim. A carrier event is a pair $(r,h)$ with $r\in\mathbb{R}$ a recognition ratio and $h$ a proof that $0<r$.
background
The module studies 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 physics module.
Time is discrete in RS-native units. The fundamental quantum is one tick ($\tau_0=1$), and one octave is eight ticks, the fundamental evolution period forced by the T7 step of the forcing chain. A propagating mode will assign data to each of the eight slots Fin 8.
The atomic datum at a single tick is a recognition ratio: a positive real that will later enter the reciprocal J-cost from the Cost import. Positivity is required so that logarithms and the self-similar fixed point $\varphi$ remain well-defined when costs and gauges are formed.
proof idea
No proof. The declaration is a structure with two fields: a real ratio and a proposition field witnessing 0 < ratio. Lean treats the positivity witness as part of the data, so every constructed carrier event is definitionally positive.
why it matters
This is the payload type for PropagatingMode, which maps each of the eight ticks to a carrier event. All later NRM constructions (per-tick cost, total mode cost, gauge equivalence, the canonical NRM, and the zero mode) sit on that eight-slot assignment and therefore depend on this structure.
In the broader framework it is the local, one-tick face of recognition composition on the T7 eight-tick octave. Keeping the type free of spin or lightlike labels preserves the module's claim that NRM is an upstream recognition object, not yet a named particle. The separation lets zero-cost uniqueness be proved before any photon identification is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.