zeroCapPhaseFamily
plain-language theorem explainer
Constant-zero phase assignment at every complexity cap, packaged as a capped phase family. Gravity and continuum-blocker arguments cite it as the explicit discriminant: zero phase cannot both match exact-shell sums and admit a complexity-cutoff limit. The body is a trivial structure instance (phase identically zero; invariance by reflexivity).
Claim. The zero phase family is the map sending each complexity cap $B\in\mathbb{N}$ to the phase model whose phase on every class is $0$, with the cross-class phase-invariance obligation discharged by reflexivity.
background
Module Seven Gaps P2-a isolates analytic obligations for removing the complexity cutoff from the phased quotient path sum. A capped phase family is a choice, at every cap $B$, of a phase model on the capped quotient; it supplies no cross-cap coherence by itself. Finite phased sums at each cap form a sequence in $\mathbb{C}$; completeness gives the Cauchy criterion for a complexity-cutoff limit.
Separately, the cap-free exact-shell API defines $Z_{\mathrm{cap}}$ as the sum of exact quotient shells in range $B$, and an oscillatory tail predicate that uniformly bounds late contiguous shell blocks. Exact telescoping equates Cauchy behavior of $Z_{\mathrm{cap}}$ with that tail cancellation. The zero phase is the canonical witness that fails the cancellation criterion at epsilon one.
A still-missing bridge equates capped $Z_q$ sums with exact-shell sums at every finite cap. Under that bridge, convergence of the phased $Z_q$ sequence is equivalent to exact-shell tail cancellation. Limits here only remove a complexity cutoff; they are not mesh refinement and claim nothing about continuum geometry or rates.
proof idea
Definitional construction, not a proof. For every cap $B$, return the phase-model structure whose phase map is the constant function $0$ on classes, and whose invariance field is rfl (equality of zeros). No lemmas are applied.
why it matters
Supplies the concrete zero-phase input to zeroPhase_compatibility_and_limit_impossible, which states that a zero-phase capped family cannot simultaneously satisfy cap-shell compatibility and possess a phased $Z_q$ complexity-cutoff limit. That theorem is the module's explicit discriminant for any proposed bridge between capped quotients and exact-shell decompositions: the zero phase has an epsilon-one failure of exact-shell tail cancellation, so any substrate-derived phase that hopes to remove the cutoff must do strictly better than zero.
In the Recognition gravity stack this sits inside the Seven Gaps continuum-blocker path: it rules out the trivial phase before one invests in a Clifford or eight-tick-derived phase model. It does not itself invoke T5--T8 or the RCL; it is a local API witness that keeps the cutoff-removal claim honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.