classPhase_phaseModelAtCap
plain-language theorem explainer
On the capped triangulation quotient at bound B, the class-level phase obtained by transporting an exact-shell phase equals the original phase evaluated on the shell image of that class. Anyone reindexing phased Z_q sums across the cap–shell carrier bridge cites this identity. The proof is a one-step quotient induction that reduces to definitional equality on representatives.
Claim. Let $\mathrm{phase}$ assign a real value to every exact path class in every shell $n$. Fix a complexity cap $B$ and a triangulation class $q$ at that cap. Then the class phase of the transported phase model at $B$, evaluated on $q$, equals $\mathrm{phase}$ on the exact-shell pair $(\mathrm{capToShell}(q))$.
background
Module P2.3 builds the carrier equivalence behind CapShellCompatibility. At cap $B$, every bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$; conversely every 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 maps between the two quotient carriers (bounded triangulation classes and shells up to $B$).
An arbitrary exact-shell phase is transported to a PhaseModel at cap $B$ by reading the phase on the shell image of each bounded representative (phaseModelAtCap). The forward quotient map capToShell sends a triangulation class to its shell pair. Class phase is the well-defined real obtained by evaluating a PhaseModel on a quotient class.
No continuum limit, substrate phase, or physical interpretation is assumed; the setting is purely finite combinatorial reindexing of $1/|\mathrm{Aut}|$ weighted sums.
proof idea
Apply Quotient.inductionOn to the triangulation class $q$, reducing to a single bounded representative $K$. On representatives, both sides are definitionally the phase of the shell image of $K$ under boundedToShell, so rfl closes the goal. The invariance proof already baked into phaseModelAtCap guarantees the left-hand class phase is well-defined; this lemma only identifies it with the original shell phase after capToShell.
why it matters
This is the pointwise phase-matching step on the carrier bridge. Downstream, phasedZq_eq_exactComplexityCutoff (the headline finite-sum reindexing) unfolds the capped phased $Z_q$ sequence, substitutes the transported weight from phaseModelAtCap, and reindexes the finite quotient sum along the cap–shell equivalence; the present identity supplies the phase values after that reindex, equating the sum to exactComplexityCutoff phase B (shell range $B+1$).
Within Seven Gaps gravity, that equality is the combinatorial content of CapShellCompatibility: phased capped sums agree with exact-shell cutoffs without assuming convergence or a continuum. It sits upstream of any later continuum or physical reading of the $Z_q$ series, and closes a pure carrier bookkeeping obligation rather than a dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.