CapPhaseFamily
plain-language theorem explainer
A cap phase family assigns, to every natural-number complexity cap, an oscillatory phase model on the bounded configurations at that cap. It is the basic input type for the phased quotient path-sum API in the Seven Gaps continuum-blocker module. Anyone stating cutoff removal, Cauchy criteria, or cap-to-shell compatibility cites it. The declaration is a pure type synonym with no proof content.
Claim. A cap phase family is a map sending each complexity cap $B \in \mathbb{N}$ to a phase model on the bounded configurations of complexity at most $B$: a real-valued phase on labeled configurations that is invariant under the stated relabeling equivalence.
background
The module isolates analytic obligations for removing the complexity cutoff from the phased quotient path sum (Seven Gaps, P2-a). Fixed-cap data can only express a family of phase models and hence a sequence of finite quotient sums; completeness of $\mathbb{C}$ then equates existence of a limit with the Cauchy property.
Upstream, a phase model at fixed cap $B$ is an explicit oscillatory phase on labeled bounded configurations together with relabeling invariance, so the phase descends to triangulation classes. The phase function itself is an input; a substrate-derived phase remains open. The polarized birth interface count $B$ and the object-level quotient appear only as ambient scaffolding for the configuration and path-class language.
The doc-comment is explicit: a phase choice at every complexity cap supplies no cross-cap coherence by itself. Coherence, tail cancellation, and cap-to-shell identification are separate obligations built on top of this type.
proof idea
Definitional abbrev only: the name is synonymous with the dependent function type sending each natural-number cap $B$ to a phase model at that cap. No tactics, no lemmas, no reduction.
why it matters
This type is the carrier for every cutoff-removal statement on the existing capped quotient sums. Downstream, the phased sequence, the complexity-limit predicate, the Cauchy criterion, and the headline iff all quantify over a cap phase family. Cap-shell compatibility is a structure on a family $P$ together with an exact-shell phase, requiring equality of the two finite sums at every cap.
The full-theory ledger certifies the Pillar 2 cutoff-limit blocker partly by quantifying over all such families once compatibility is assumed. The residual DAG records continuum residual R4 as existence of some family and exact-shell phase with that compatibility. Cap-shell bridge transports an exact-shell phase to a family of this type.
In the Recognition gravity stack this is bookkeeping for complexity-cutoff removal only, not mesh refinement, continuum geometry, or a derived measure. It sits under the open demand that a substrate-derived phase supply oscillatory tail cancellation (zero phase is the discriminating decoy).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.