SupportedBelow
plain-language theorem explainer
Defines the property that a shell-indexed phase map vanishes identically on every exact complexity shell at or above a fixed natural-number cap B. Gravity and continuum-blocker arguments cite it to encode finite-support (fixed-cap) phase witnesses. The body is a direct universal quantification: for all n ≥ B and all classes c in the exact shell, the phase is zero.
Claim. A phase assignment $\mathrm{phase}$ on exact complexity shells is supported below a cap $B\in\mathbb{N}$ when, for every complexity $n\ge B$ and every exact path class $c$ of complexity $n$, one has $\mathrm{phase}(n,c)=0$.
background
Module P2.4 (exact-shell phase-balance blocker) isolates what is missing for the phase obligation in the oscillatory-tail continuum blocker. Carrier facts already give finite exact shells, positive class masses, large shell mass, and one fixed-cap pairing witness, but no substrate action that resolves phases inside every late shell.
An exact path class at complexity $n$ is a combinatorially distinct exact complex of complexity exactly $n$: the disjoint union, over shell signatures, of the quotient of the exact labeled class by global equivalence. No bounded-complex cap type enters that shell type.
The ambient goal is genuine asymptotic intra-shell balance (at least vanishing late shell amplitudes, and ultimately the uniform contiguous-block control of an oscillatory tail). Limits are in the complexity cutoff only; they are not mesh refinement and make no geometric-continuum claim.
proof idea
Pure definitional abbreviation. The predicate is the Prop that $\forall n\ge B$, the phase map is identically zero on the entire exact shell of complexity $n$. No lemmas or tactics are involved.
why it matters
Feeds the blocker theorem that a fixed-cap cancellation witness cannot be promoted to a uniform oscillatory tail merely by extending it with zero phase beyond the witnessed cap. That theorem reduces the supported-below hypothesis to the already-proved fact that eventually-zero phase fails the oscillatory-tail condition.
In the Seven Gaps chain this seals one negative route: finite-cap pairing certificates, even when zero-extended, do not supply the missing P2.4 asymptotic intra-shell balance. It sits beside the sibling blockers for eventually-zero phase and shell-constant phase, all pointing at the same gap relative to the continuum phase obligation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.