selfLoopEnrichedSubstrate
plain-language theorem explainer
A concrete witness that the enriched-carrier phase substrate is inhabited: the self-loop-count mod-8 labeled tick, with its global-equivalence invariance and the proof that its descended class tick is not a pure shell-signature tick. Gravity/Gap2 continuum workers cite it to discharge Nonempty on the substrate schema. The body is a three-field structure instance wiring existing lemmas.
Claim. Define an enriched-carrier phase substrate whose labeled tick is the self-loop count modulo $8$, whose global-equivalence invariance is the corresponding invariance theorem for that tick, and whose descended tick is certified not to be a shell-signature tick.
background
This module banks the Wave C R5 attack surface on the continuum residual that an oscillatory tail phase exists distinct from the zero phase. After signature-level Fin-8 blocking stalled, route C packages a sharper typed residual: an enriched carrier API that is inhabited while the analytic tail obligation stays open.
An EnrichedCarrierPhaseSubstrate is a triple: a labeled tick (phase label on loom configurations), a proof that the label is invariant under global equivalence of configurations, and a proof that the descended tick (after quotienting by that invariant) is not a shell-signature tick. Shell-signature ticks factor only through shell signature data; escaping them is the point of the enrichment.
The self-loop tick labels each configuration by its self-loop count mod 8. Upstream, that label is already shown globally equivalent-invariant, and the associated class tick is shown not to factor through shell signature alone (it distinguishes two-loops from two-bridges incidence at the same shell index).
proof idea
Pure structure instance: set the labeled tick field to the self-loop-count mod-8 tick, fill the invariance field with the existing global-equivalence invariance theorem for that tick, and fill the non-shell-signature field with the theorem that the self-loop class tick does not factor through shell signature. No new reasoning; three named upstream results are wired into the schema package.
why it matters
This is the concrete inhabitant that makes the enriched-carrier substrate nonempty. Downstream, enrichedCarrierPhaseSubstrate_nonempty is the one-line ⟨selfLoopEnrichedSubstrate⟩ witness. In the Gap2 continuum program it closes the "API inhabited" half of route C while leaving the analytic oscillatory-tail obligation open, so R5 itself remains uninhabited and gap2_continuum_and_measure is not flipped. It records decision D-qg-c1-r4-enriched-carrier: carrier forcing and Fin-8 signature blocking were refused; the credit-bearing terminal is the sharper typed residual plus this concrete quotient-internal tick that escapes shell signature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.