complexityTick
plain-language theorem explainer
Assigns every exact path class of complexity n the residue n mod 8 in the eight-tick circle, ignoring the class itself. Gravity and QG authors cite it as the canonical decoy tick: shell-constant by construction, hence banked dead under the Gap-2 residual schema. The body is a one-line Fin constructor from natural-number remainder.
Claim. For every natural number $n$ and every exact path class of complexity exactly $n$, the raw complexity tick is the residue $n \bmod 8$, viewed as an element of $\{0,1,\ldots,7\}$. The assignment depends only on the shell index $n$, not on the representative class.
background
This module banks the Wave C1 R2 residual: a well-posed tick map from exact path classes into the eight-tick circle, together with equidistribution and escape fields that kill the dead classes ShellConstant and EventuallyZeroPhase.
An exact path class of complexity $n$ is the GlobalEquivalent quotient of combinatorially distinct exact complexes of complexity exactly $n$: a sigma-type over shell signatures of the quotient by the exact setoid. No bounded-complexity cap appears. The eight-tick API elsewhere is only a Fin-8 trace hypothesis; equidistribution content is developed independently in this module.
The derived phase associated to a tick is $2\pi \cdot \mathrm{tick}/8$. A tick that is constant on each shell is shell-constant and therefore dead for the residual schema: it cannot supply the intra-shell variance needed to escape the blockers.
proof idea
Definition, not a proof. The value is the subtype pair $\langle n \bmod 8,, p\rangle$ in Fin 8, where $p$ is the standard bound $n \bmod 8 < 8$ discharged by Nat.mod_lt and a trivial positivity check on 8. The path-class argument is unused (underscore), which is the mathematical content of the decoy.
why it matters
Feeds the derived real phase complexityTickPhase via the generic tickDerivedPhase wrapper. That phase is the decoy theorem of the module: raw complexity eight-tick phase is shell-constant, hence banked as a dead class under ZqShellBalanceBlocker. Escape from those dead classes requires genuine intra-shell tick variance; this assignment supplies none.
In the Recognition forcing chain the eight-tick octave is landmark T7 (period $2^3$). The module uses that Fin-8 structure as a phase substrate for Gap-2 continuum/measure work, but explicitly does not flip gap2_continuum_and_measure. Contiguous late-block tail cancellation and analytic OscillatoryTail for the signature-vertex witness remain open (R4).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.