selfLoopClassTick_twoBridges
plain-language theorem explainer
On the two-bridges path class at level 2, the descended self-loop class tick evaluates to zero. Gravity and continuum-R5 workers cite this as the concrete numerical witness that two-bridges carries no self-loop incidence. The proof is a short definitional simplification through the descended-tick constructor and the already-computed two-bridges self-loop count.
Claim. The self-loop class tick of the two-bridges equivalence class at level $2$ equals $0$ (as a valid tick index). In symbols: if $\tau_{\mathrm{sl}}$ is the class-level self-loop tick and $[\gamma_{2B}]$ is the two-bridges class, then $\tau_{\mathrm{sl}}(2,[\gamma_{2B}]) = 0$.
background
This module sits in the Gravity SevenGaps Wave-C attack on the continuum R5 residual: existence of a phase with an oscillatory tail that the zero phase lacks. After the Fin-8 signature blocker stalled, the session banks an enriched-carrier API: labeled ticks, descent to path classes, and quotient-internal invariants that can escape pure shell-signature data.
A tick is the fundamental RS time quantum ($\tau_0 = 1$). Self-loop count records how many edges of a representative close on themselves; the self-loop tick packages that count as a labeled tick, and the class-level version descends it through the path-class quotient so the value is invariant on the class. The two-bridges class is one concrete inequivalent carrier used as a test object against shell-signature-only maps.
Upstream scaffolding includes the descended-tick constructor and the numerical fact that the two-bridges self-loop count is zero, plus the broader class-pushforward and dynamics-kind infrastructure that keep class-level data honest relative to Burnside weights.
proof idea
Term-mode proof by simp only on five names: unfold the class-level self-loop tick, the two-bridges class, the descended-tick maker, the underlying self-loop tick, and the lemma that the two-bridges self-loop count is zero. After unfolding, the residual goal is the subtype witness $0$ with a trivial norm_num bound check already present in the statement. No case split or external arithmetic beyond that count lemma.
why it matters
Feeds the parent theorem that the self-loop class tick is not a shell-signature tick: that argument applies a hypothetical shell-signature factorization at level 2 to both the two-loops and two-bridges classes, uses equal shell signatures, and obtains a contradiction once the two class ticks differ. This lemma supplies the two-bridges side (value $0$).
In the R5 program it is the concrete quotient-internal witness promised by the module doc: a tick that uses incidence inside the class and therefore cannot factor through shell signature alone. It does not close the continuum residual or flip gap2_continuum_and_measure; R5 stays open. Framework-wise it is local gravity/carrier bookkeeping under the eight-tick octave, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.