selfLoopClassTick_not_ShellSigTick
plain-language theorem explainer
The descended self-loop tick on exact path classes cannot be recovered from shell signatures alone; it needs quotient-internal incidence. Anyone assembling an enriched-carrier substrate for the continuum R5 residual cites this separation lemma. Proof is a short contradiction at n=2: two path classes share a shell signature yet receive distinct self-loop ticks.
Claim. The class-level self-loop tick (the descent of the self-loop count tick along the exact-path-class quotient) is not a shell-signature tick: there is no function of shell signatures alone that reproduces its values on every exact path class.
background
Module setting is the Wave C attack on the continuum R5 residual
$$\exists,\mathrm{phase},;\mathrm{OscillatoryTail}(\mathrm{phase})\land\neg\mathrm{OscillatoryTail}(0).$$
Signature-level Fin-8 blocking stalled (mesoscopic cube dominance only). Route A (enriched carrier forcing eventual mass balance) is the design surface; this file banks the carrier API and a concrete quotient-internal tick that escapes shell signature.
A shell-signature tick is one that factors through shell data alone: some $\sigma$ with tick$(n,[\gamma])=\sigma(n,\mathrm{shell}(\gamma))$ for every exact path class. The self-loop class tick is the descent of the self-loop count tick along the exact-path-class quotient (via the self-loop invariance lemma). Two named classes at $n=2$, the two-loops class and the two-bridges class, are the witnesses that this descent sees incidence inside the quotient, not only the shell.
proof idea
Assume for contradiction a shell-signature witness $\sigma$ for the self-loop class tick. Specialize at $n=2$ to the two-loops and two-bridges classes. Their underlying shells agree, so $\sigma$ returns the same value on both. The specialized evaluation lemmas rewrite the self-loop class tick on those two classes to concrete Fin 8 values, which decide shows are unequal. Chaining the two $\sigma$-equalities with that inequality yields the contradiction. Purely local: no continuum or mass-balance input.
why it matters
This is the separation fact that makes the self-loop tick a genuine enriched carrier rather than a shell rephrasing. Downstream it is wired as the not_shellSigTick field of selfLoopEnrichedSubstrate, the primary enriched-carrier substrate package in this module.
In the Seven Gaps gravity program it supports route C of decision D-qg-c1-r4-enriched-carrier: bank a sharper typed residual naming the enriched-carrier obligation, with characterization and bridge lemmas, while R5 itself stays open (uninhabited). It does not flip gap2_continuum_and_measure. The eight-tick (Fin 8) codomain is the T7 octave; the lemma only shows the tick uses more than shell data inside that octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.