perTickCost
plain-language theorem explainer
Assigns to each tick of a propagating recognition mode the reciprocal J-cost of that tick's carrier ratio. Downstream NRM uniqueness and zero-cost arguments cite it as the local cost density on the eight-tick cycle. The body is a one-line application of Jcost to the event ratio.
Claim. For a propagating recognition mode $M$ (a map from the eight ticks to carrier events) and tick index $i \in \{0,\ldots,7\}$, the per-tick cost is $J\bigl(r_i(M)\bigr)$, where $r_i(M)$ is the positive ratio of the carrier event at tick $i$ and $J(x)=(x+x^{-1})/2-1$.
background
The module isolates the null recognition mode: the unique zero-cost propagating mode of the eight-tick recognition cycle, up to ratio-gauge equivalence. It deliberately avoids photon labels (spin, polarization, lightlike kinematics); those live downstream.
A propagating mode is a structure assigning a carrier event to each tick of the octave $i:\mathrm{Fin},8$. Each carrier event carries a positive ratio. The recognition cost on positive ratios is the standard RS functional $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$, forced uniquely by the Recognition Composition Law (T5).
The fundamental time quantum is one tick ($\tau_0=1$ in RS-native units); one octave is eight ticks. Per-tick cost is the local density that the total mode cost later sums over the cycle.
proof idea
Pure definition: evaluate $J$ at the ratio of the carrier event at tick $i$. No lemmas are applied in the body; nonnegativity, vanishing criteria, and summation identities are proved downstream from properties of $J$.
why it matters
This is the local cost density for null-recognition-mode analysis. Total mode cost is the sum of per-tick costs over $\mathrm{Fin},8$. Downstream theorems use it to show: the canonical NRM has zero cost at every tick; per-tick costs are nonnegative; vanishing total cost forces every per-tick cost (hence every ratio) to the identity. Those facts pin the unique zero-cost mode up to gauge equivalence, the upstream object later identified with the photon in a separate module. The eight-tick domain is the T7 octave forced by the foundation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.