merely
plain-language theorem explainer
A phase configuration that vanishes past a finite complexity cap is supported below that cap: zero-extend the witnessed finite piece and the support predicate holds. Gravity and continuum-blocker arguments cite it to package finite-cap pairing certificates. It is the introduction rule for that support predicate, not a deep calculation.
Claim. If a shell phase agrees with a finite-cap witness and is extended by zero phase for all complexities beyond that witnessed cap, then the phase is supported below the cap (finite complexity support, zero thereafter).
background
Module P2.4 (exact-shell phase-balance blocker) isolates what is still missing for the continuum oscillatory-tail obligation. 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 balances phases inside every late shell.
The local predicates separate weak necessary conditions from the full tail. ShellAmplitudeVanishes asks each late exact-shell amplitude to tend to zero. Support-below-a-cap packages the finite-witness situation: the phase is prescribed only up to a complexity bound and is zero past that bound. Limits are in the complexity cutoff, not mesh refinement; no geometric-continuum claim is made.
Upstream eight-tick phases ($k\pi/4$ for $k=0,\ldots,7$) fix the discrete phase vocabulary used elsewhere in the monolith; the present declaration only needs the idea of setting phase to zero outside a cap.
proof idea
Zero proof body: this is the introduction form for the support-below predicate. Feed a finite-cap phase witness and the zero extension past the cap; the constructor (or one-line intro) returns the support certificate. No cancellation estimate, limit, or shell-mass identity is invoked.
why it matters
P2.4 must show that finite-cap pairing and related finite edits cannot discharge OscillatoryTail. The module routes that through the support predicate: once a phase is supported below a cap, supportedBelow_not_oscillatoryTail (sibling) blocks the uniform tail. The same finite-edit moral appears in eventuallyZeroPhase_not_oscillatoryTail.
Together with the constant-per-shell blocker (norm equals diverging positive shell mass), this pins the missing input as genuine asymptotic intra-shell balance, at least shell-amplitude vanishing and in fact contiguous-block control. Relabeling invariance, finite-cap pairing, and complexity-only phases are ruled out as substitutes. No full-theory flag moves; the declaration only packages the finite-support hypothesis the blockers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.