phaseModelAtCap
plain-language theorem explainer
Transports an arbitrary real-valued phase on exact-shell path classes to a phase model on the labeled bounded carrier at a fixed complexity cap B. Discrete-geometry and gravity workers cite it when moving phase data across the capped-quotient bridge of Seven Gaps P2.3. The construction evaluates the original phase on the exact-shell image of each bounded complex; the invariance field is a one-line rewrite by congruence of that forward map under relabeling.
Claim. Given a family of real-valued phases on exact path classes of every shell index $n$, and a complexity cap $B\in\mathbb{N}$, construct a phase model at $B$ by sending each bounded complex $K$ of complexity at most $B$ to the original phase of its exact-shell image (forget the three cap proofs, retain signature and incidence, enter the exact relabeling quotient). The assignment is invariant under bounded-complex relabeling.
background
Module CapShellBridge builds the missing carrier equivalence behind CapShellCompatibility (Seven Gaps P2.3). At cap $B$, a bounded complex has 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 three cap proofs. Both maps keep incidence data and relabeling witnesses, so they descend to inverse maps on the two quotient carriers.
The forward labeled map boundedToShell forgets the cap proofs, retains the exact signature, and enters the exact relabeling quotient as a pair (shell index, exact path class). A phase model at $B$ is a real assignment on bounded complexes that is constant on the bounded relabeling relation. The module assumes no target-sum equality, convergence, substrate phase, or continuum interpretation; it only moves combinatorial carriers and class measures $1/|\mathrm{Aut}|$.
proof idea
Structure construction, not a deep proof. The phase field of the returned PhaseModel B is the original exact-shell phase composed with the two projections of boundedToShell: shell index and exact path class. The invariance field is discharged in one rewrite: if two bounded complexes are related by a bounded relabeling witness $h$, then boundedToShell_congr h makes their shell images definitionally equal, so the pulled-back phases agree.
why it matters
This is the phase-transport half of the capped-to-exact bridge. Downstream, capPhaseFamily packages it at every cap; classPhase_phaseModelAtCap proves the transported phase descends exactly to the original phase after the carrier equivalence; and the headline finite-sum reindexing phasedZq_eq_exactComplexityCutoff uses that descent to equate the phased capped quotient sum with the exact-shell cutoff through shell $B$ (range $B+1$).
In the Seven Gaps program this closes the combinatorial gap between the bounded Zq continuum blocker and exact-shell complexity cutoffs, without claiming physical continuum content. It sits upstream of any later gravity or continuum limit that needs phased class sums to match across the two carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.