endpointReversalThenTetSlotRotation_ge
plain-language theorem explainer
Endpoint reversal followed by tetrahedron slot rotation preserves global gauge equivalence of exact complexes of fixed signature. Gravity and Gap-2 workers cite it when treating that composite as a well-defined class map on shells. The proof is a one-line composition of the two separate equivalence-preservation lemmas.
Claim. Let $K$ and $K'$ be exact complexes of the same signature $(v,e,t)$. If $K$ and $K'$ are globally equivalent, then the complexes obtained by applying endpoint reversal and then tetrahedron slot rotation to each are again globally equivalent.
background
This module is the Wave C1 R4 bank for Gap-2: a conditional bridge from a structure hypothesis TailFiberShift (a tail of classMu-preserving shell automorphisms that rotate the Fin-8 tick by $+1$) into eventual tick-fiber mass balance and oscillatory tails. Existence of such a free action is left open; the module also records no-go fallbacks for obvious candidate operations.
An exact complex packages bounded vertex, edge, and tetrahedron data at a shell whose complexity is $\max(n_V,n_E,n_T)$. Global equivalence is the gauge relation identifying complexes that differ only by admissible relabeling. Endpoint reversal swaps the two ends of every edge; tetrahedron slot rotation cycles the four tet vertex slots by $+1$ on $\mathrm{Fin},4$. Their composite is the operation studied here.
The sibling lemmas already show each factor alone sends globally equivalent complexes to globally equivalent complexes. That is the only upstream content this declaration needs.
proof idea
Term-mode one-liner. Apply the tetrahedron-slot-rotation equivalence-preservation lemma to the image of the hypothesis under the endpoint-reversal equivalence-preservation lemma: if $h:K\simeq K'$ globally, then endpoint reversal yields a global equivalence, and slot rotation of both sides yields the desired global equivalence of the composites.
why it matters
In the Gap-2 residual R4 story, candidate shell operations must induce well-defined maps on global-equivalence classes before one can ask whether they implement a free Fin-8 tick shift. This lemma closes that bookkeeping for the composite of endpoint reversal and tet slot rotation.
The module doc then uses the induced class map in the no-go: the composite fixes a degenerate labeled complex in every shell (all-loops / constant-tet data), so the class map has a fixed point and cannot satisfy $\tau c=\tau c+1$ on $\mathrm{Fin},8$. That blocks these signature-level routes as TailFiberShift witnesses, complementing the Burnside stall in the signature Fin-8 oscillatory-tail blocker.
R4 itself stays open (uninhabited TailFiberShift); gap2_continuum_and_measure stays false. No downstream consumers are wired yet; the lemma is local infrastructure for the no-go section and any later class-map arguments on the same composite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.