complexityTickPhase_decoy_dead
plain-language theorem explainer
The raw complexity eight-tick phase (phase equal to 2π times n mod 8 over 8 on every class in shell n) is simultaneously shell-constant and not an oscillatory tail. Anyone auditing Gap-2 decoy elimination cites this pairing. The proof is a one-line product of the two banked decoy lemmas already proved for that phase.
Claim. The complexity-derived tick phase $\varphi_n(c) = 2\pi\,(n \bmod 8)/8$ on exact path classes satisfies both: (i) it is constant on each exact complexity shell $n$ (independent of the class $c$), and (ii) it fails the oscillatory-tail condition that late contiguous blocks of exact-shell amplitudes become arbitrarily small.
background
This module banks the Wave C1 R2 exact-shell tick-phase enrichment schema for Gap 2. Exact path classes are already the GlobalEquivalent quotient of shell signatures, so a tick assignment to Fin 8 is well-posed on classes. Dead classes are banked separately: a phase is shell-constant when it never distinguishes classes inside a fixed exact complexity shell (it may still depend on the shell index $n$). An oscillatory tail requires that every late contiguous block of exact-shell amplitudes is uniformly small in both endpoints, with no rate or summability hypothesis.
The decoy phase is the raw complexity tick: $\varphi_n(c) = 2\pi\cdot(n\bmod 8)/8$, obtained by feeding the complexity tick into the derived-phase constructor. Because the value depends only on $n$, it is constant on each shell. Upstream, shell-constant phases are already known not to be oscillatory tails: no intra-shell cancellation occurs, so full-shell amplitudes stay large (positive shell mass times one common unit phase).
proof idea
Term-mode pairing. The left conjunct is complexityTickPhase_shellConstant (proved by rfl after introducing shell and class: the phase definition ignores the class). The right conjunct is complexityTickPhase_not_oscillatoryTail, itself a one-line application of the banked blocker shellConstant_not_oscillatoryTail to that same shell-constant witness. No new algebra is done here.
why it matters
Module doc flags this as the explicit decoy kill: raw complexity tick $2\pi\cdot(n\bmod 8)/8$ is shell-constant, hence dead. In the Gap-2 residual DAG, escape from the banked dead classes requires genuine intra-shell tick variance; this theorem records that the naive complexity-mod-8 assignment fails that test on both counts at once.
It sits beside the live witness path (signature vertex-count mod 8), which does escape both dead classes, while analytic oscillatory-tail status for that witness remains open (R4). The eight-tick octave (T7) supplies the Fin-8 phase lattice, but equidistribution content is independent and lives in this module's substrate schema. No continuum or measure flip is claimed: gap2_continuum_and_measure stays unflipped. Currently unused downstream; it is a status certificate for decoy elimination in the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.