capPhaseFamily
plain-language theorem explainer
Given any exact-shell phase (a real weight on exact path classes at each shell index), this definition builds the canonically transported capped phase family: at every complexity cap B it returns the phase model obtained by pushing the shell data across the cap–shell carrier bridge. Gravity and continuum-blocker arguments cite it as the unique constructed family that feeds CapShellCompatibility. The body is a one-line pointwise wrapper around the already-defined transport at a fixed cap.
Claim. For any exact-shell phase $\mathrm{phase}:\forall n\in\mathbb{N},\;\mathrm{ExactPathClass}(n)\to\mathbb{R}$, define the capped phase family by sending each complexity cap $B$ to the phase model at that cap obtained by transporting $\mathrm{phase}$ across the carrier equivalence between exact shells $n\le B$ and bounded complexes of complexity $\le B$.
background
Module P2.3 builds the missing carrier bridge between capped (bounded-complexity) quotient complexes and exact-shell complexes. At a fixed cap $B$, every bounded complex has a unique exact complexity $\max(n_V,n_E,n_T)\le B$; conversely an exact complex in shell $n\le B$ becomes bounded by reattaching the three cap proofs. Both maps preserve incidence data and relabeling witnesses, so they descend to inverse equivalences of the two quotient carriers and preserve automorphism cardinality (hence the $1/|\mathrm{Aut}|$ class measure).
An exact-shell phase is an arbitrary real assignment to exact path classes at each shell $n$. The sibling transport phaseModelAtCap pushes that assignment to a PhaseModel on the capped quotient at a single $B$. A CapPhaseFamily is simply the family of such models indexed by every cap. No continuum limit, convergence, or physical substrate phase is assumed here; the module only supplies the algebraic carrier and the transported weights needed for finite-sum reindexing against exactComplexityCutoff.
proof idea
One-line definitional wrapper. The body is the lambda fun B => phaseModelAtCap phase B: for each natural-number cap it applies the already-constructed pointwise transport of the given exact-shell phase to the capped carrier at that cap. No tactics, no new lemmas; the mathematical content lives in phaseModelAtCap and the underlying cap–shell equivalence.
why it matters
This is the canonical family that closes the P2.3 bridge obligation. Downstream, phasedZq_eq_exactComplexityCutoff reindexes the finite capped quotient sum along the carrier equivalence and obtains equality with the exact-shell cutoff through shell $B$. That equality is packaged as capShellCompatibility, the P2.3 closer: every exact-shell phase has a transported capped family satisfying the previously missing ZqContinuumBlocker.CapShellCompatibility.
In the full theory ledger, gap2_capshell_bridge_discharged records that only this constructed family (not an arbitrary CapPhaseFamily) discharges the missing-bridge premise of the Pillar-2 cutoff-limit blocker. That blocker certifies the convergence half of gap2_continuum_and_measure as complexity-cutoff statements (oscillatory-tail control and capped–exact compatibility), not mesh refinement. The definition therefore sits on the gravity seven-gaps path that links exact-shell UV data to the capped $Z_q$ API without claiming a geometric continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.