complexityTickPhase_shellConstant
plain-language theorem explainer
The naive eight-tick phase built only from path complexity is constant on every exact complexity shell: it cannot tell classes inside a shell apart. Gravity residual auditors cite it to mark that assignment as a banked dead class. The proof is definitional reflexivity after introducing shell index and class.
Claim. Let $\varphi$ be the phase that sends each exact path class of complexity $n$ to the eight-tick angle $2\pi\cdot(\text{complexity tick})/8$. Then $\varphi$ is shell-constant: for every $n$ and every class $c$ in the exact shell of complexity $n$, $\varphi_n(c)=\varphi_n(c_\star)$ where $c_\star$ is the isolated reference class of that shell.
background
This module banks the Wave C1 Gap2 residual R2 schema: tick assignments on ExactPathClass n (the GlobalEquivalent quotient of exact shells) and the dead-class blockers already recorded in the Zq shell-balance layer. A phase on exact path classes is shell-constant when, inside every fixed complexity shell, it takes the same real value on every class; it may still depend on the shell index $n$. No intra-shell cancellation can occur for such a phase: the full shell amplitude is just positive shell mass times one common unit phase.
The decoy phase under study is the raw complexity tick phase: compose the complexity-derived Fin-8 tick with the standard derived phase $2\pi\cdot\mathrm{tick}/8$. The eight-tick API supplies only a Fin-8 trace hypothesis; equidistribution and escape from dead classes are independent Props developed here. Upstream, shellConstant_not_oscillatoryTail already proves the complexity-phase no-go: any shell-constant phase fails the oscillatory-tail predicate.
proof idea
Term-mode proof by definitional equality. Introduce shell index $n$ and class $c$, then rfl: by construction the complexity tick (hence the derived phase) depends only on $n$, so evaluating on $c$ and on the isolated reference class of the shell yields identical reals. No lemmas beyond the definitions of the decoy phase and of shell-constancy are required.
why it matters
Marks the raw complexity eight-tick phase as a banked dead class inside the Gap2 tick-phase substrate. Downstream, complexityTickPhase_not_oscillatoryTail feeds this fact into the banked no-go shellConstant_not_oscillatoryTail, and complexityTickPhase_decoy_dead packages the conjunction shell-constant and not oscillatory-tail. That decoy kill is part of the module's THEOREM list: escape from dead classes requires genuine intra-shell tick variance, not a function of $n$ alone.
In the broader Recognition gravity residual program this protects the eight-tick octave story (T7) from a false positive: shell-level complexity phase cannot produce the amplitude cancellation needed for continuum/measure progress on gap2. The real witness path is the signature vertex-count mod 8 (which escapes both dead classes); its analytic oscillatory tail remains open (R4), as does strengthened late-block tick balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.