ShellConstant
plain-language theorem explainer
A phase on exact path classes is shell-constant when it is constant inside every fixed complexity shell, though it may still depend arbitrarily on the shell index. Gravity and continuum-blocker arguments cite this predicate when ruling out complexity-only phases. The body is a universal equality against the isolated reference class of each shell.
Claim. A phase assignment $\varphi$ sending each exact path class at complexity $n$ to a real number is shell-constant if, for every $n$ and every class $c$ at level $n$, $\varphi_n(c)=\varphi_n(c_n^*)$, where $c_n^*$ is the isolated reference class of shell $n$. Equivalently, $\varphi$ does not distinguish classes inside any exact complexity shell.
background
Module P2.4 isolates the missing phase input for the Zq continuum blocker. Carrier facts already give finite exact shells, positive class masses, large shell mass, and a fixed-cap pairing witness. They do not supply a substrate action that resolves phases inside every late shell. Limits here are complexity cutoffs, not mesh refinement or geometric continuum claims.
An exact path class is a gauge-UV class at fixed complexity $n$. The isolated class is a canonical representative of that shell. A phase is a real-valued assignment on those classes. Shell mass is the positive total mass of the shell; the exact shell amplitude is the coherent complex sum of class masses times unit phases.
Shell-constant is the complexity-only extreme: the phase may vary with $n$, but inside each shell every class shares one common value. The module contrasts this with eventually-zero phases (finite-cap repairs) and with the full oscillatory-tail demand of uniform contiguous-block cancellation.
proof idea
Pure definition: the predicate is the Prop that for every complexity $n$ and every class $c$ at that level, the phase of $c$ equals the phase of the isolated reference class of shell $n$. No lemmas or tactics; downstream theorems unfold this equality to factor the shell amplitude.
why it matters
This predicate is the complexity-only no-go input for P2.4. Downstream, exactShellAmplitude_shellConstant factors the shell amplitude as positive shell mass times one common unit phase, so the norm equals the diverging shell mass and no intra-shell cancellation occurs. That yields shellConstant_not_shellAmplitudeVanishes and then shellConstant_not_oscillatoryTail.
Those facts feed p24_shell_balance_blocker_certificate and the ledger theorem gap2_shell_balance_blocker_certified: oscillatory tails force per-shell amplitude vanishing, and neither finite-cap (eventually zero) phases nor shell-constant phases can supply it. Any closing phase must rebalance every late shell. The open obligation is genuine asymptotic intra-shell balance from richer substrate structure, not relabeling invariance or complexity-only phases. No full-theory flag is changed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.