complexityTickPhase
plain-language theorem explainer
Raw complexity eight-tick phase on exact path classes: each class maps to the real phase $2\pi\cdot k/8$ from its complexity tick. Gap-2 residual auditors cite it as the banked decoy witness. One-line composition of the complexity tick assignment with the standard tick-to-phase lift; downstream proofs show it is shell-constant, hence dead.
Claim. For every $n\in\mathbb{N}$ and every exact path class $c$ of shell $n$, the complexity tick-phase of $c$ is the real number obtained by lifting the complexity tick of $c$ through the eight-tick phase map $k\mapsto 2\pi k/8$.
background
Module Wave C1 R2 banks the exact-shell tick-phase enrichment schema for Gap 2. An ExactPathClass n is already a GlobalEquivalent quotient (sigma over shell signatures of the exact-setoid quotient), so a tick assignment into Fin 8 is well-posed on classes by construction. Dead residual classes are shell-constant phases and eventually-zero phases; escape needs genuine intra-shell tick variance.
The eight-tick API supplies only a Fin-8 trace hypothesis. Phase values are the standard octave angles $k\pi/4$ (equivalently $2\pi k/8$), matching the T7 eight-tick period. The fundamental RS time quantum is one tick ($\tau_0=1$). The complexity tick is the naive residue-of-complexity assignment; this definition lifts it to a real phase via the shared tickDerivedPhase constructor used by live witnesses as well.
proof idea
One-line definitional wrapper: apply the shared derived-phase constructor tickDerivedPhase to the raw complexity tick assignment. No tactics, no lemmas, no computation beyond that composition. The mathematical content of the phase is entirely inherited from how tickDerivedPhase turns a Fin 8 tick into $2\pi\cdot\mathrm{tick}/8$.
why it matters
This is the explicit decoy phase named in the module status: raw complexity tick $2\pi\cdot(n\bmod 8)/8$ is shell-constant, hence banked dead. It feeds three local theorems: shell-constancy (by rfl on classes), failure of oscillatory-tail (via the banked shellConstant_not_oscillatoryTail blocker), and the combined decoy-dead package.
In the Recognition framework it sits under the T7 eight-tick octave and the Gap-2 continuum residual program. It does not flip gap2_continuum_and_measure. Live escape requires a non-constant intra-shell tick (the signature vertex-count mod 8 witness); the decoy exists so residual auditors can see the naive complexity choice is already ruled out. OscillatoryTail for the live witness and strengthened late-block tick balance remain open (R4).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.