EnrichedCarrierPhaseSubstrate
plain-language theorem explainer
Packages an enriched Fin-8 tick on labeled exact complexes that is constant on global-equivalence orbits and whose descent to exact path classes does not factor through shell signatures alone. Gravity Gap-2 continuum work cites it as the carrier schema for the R5 oscillatory-tail residual after signature-level Fin-8 attacks stalled. It is a bare structure: three fields, no proof body.
Claim. An enriched carrier-phase substrate is a triple $(L,I,N)$ where $L$ assigns to every labeled exact complex a value in $\mathrm{Fin}\,8$, $I$ asserts that $L$ is constant on global-equivalence orbits, and $N$ asserts that the descended tick on exact path classes does not factor through shell signatures $(v,e,t)$ alone.
background
The module attacks the continuum R5 residual
$$\exists,\mathrm{phase},;\mathrm{OscillatoryTail}(\mathrm{phase})\land\neg\mathrm{OscillatoryTail}(\mathrm{zeroPhase})$$
after the signature-level Fin-8 blocker stalled (mesoscopic-only cube dominance). Decision D-qg-c1-r4-enriched-carrier banks an enriched carrier API rather than forcing mass balance in one step.
A labeled tick is any map from exact complexes (indexed by vertex, edge, and tick counts) into $\mathrm{Fin},8$. The enrichment hypothesis requires constancy on global-equivalence orbits, so the tick descends via quotient lift to a well-defined map on exact path classes. Shell-signature ticks are those that factor through the coarse shell data $(v,e,t)$ only, ignoring quotient-internal incidence; the substrate demands a tick that escapes that class.
Upstream, descendedTick performs the orbit-constant lift, and ShellSigTick names the factoring property being negated.
proof idea
No proof: this is a structure declaration. The three fields are the labeled tick, the orbit-invariance proposition on that tick, and the negation that the descended tick is a shell-signature tick. Inhabitation is deferred to the concrete self-loop instance and the nonempty theorem that wraps it.
why it matters
This is the credit-bearing schema for route C on the Gap-2 continuum residual: a sharper typed residual that names the enriched-carrier obligation after routes A (eventual mass balance) and B (signature Fin-8 blocker) were refused. Downstream, the self-loop construction supplies a concrete inhabitant, enrichedCarrierPhaseSubstrate_nonempty records nonemptiness, and the exact-class carrier attack module re-exports that fact as superseded_by_enriched_carrier.
It sits inside the eight-tick (period $2^3$) octave of the forcing chain (T7): the carrier is a Fin-8 phase on exact complexes. The analytic tail (eventual fiber-mass balance or identical-zero late amplitudes) remains OPEN; R5 itself stays uninhabited. The package does not flip gap2_continuum_and_measure and introduces no sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.