exactPathClass_zero_eq
plain-language theorem explainer
Every exact path class at complexity shell 0 coincides with the isolated empty-complex class. Gravity and QG residual work cite this as the atomic finite-head uniqueness step before the shell-0 Subsingleton and Finset.univ collapse. The proof cases on the Sigma, rewrites the signature via shellSig_zero_eq, then quotients the complex and applies exactComplex_zero_eq.
Claim. For every exact path class $c$ at complexity shell level $0$, one has $c$ equal to the isolated empty-complex class at level $0$.
background
This module hardens the R4 residual in the Gap-2 tick-phase tail blocker after the R2 cross-family correction. The finite-head half of the argument needs shell 0 to be a singleton: only the empty signature $(0,0,0)$ and its unique class, so that classMu-mass cannot spread across tick fibers at the head.
An exact path class packages a shell signature with a quotiented exact complex. At level 0 the companion lemmas already force both pieces: every shell signature equals the isolated signature, and every exact complex equals the empty complex. The isolated class is the canonical inhabitant built from those empty data.
The local setting is the Wave C1 R4 package: all-shell tick-fiber mass balance would zero every exact-shell amplitude (and thus give oscillatory-tail cancellation), but the finite head blocks that balance because shell 0 concentrates mass in one fiber.
proof idea
Case-split the class as a Sigma pair (s, q). Apply shellSig_zero_eq to replace s by the isolated signature at 0, then substitute. Extend the Sigma equality with rfl on the signature component. After reducing heterogeneous equality to ordinary equality, induct on the quotient q and rewrite the representative by exactComplex_zero_eq, finishing with rfl. Pure structural collapse; no analysis.
why it matters
This is the atomic uniqueness step for the finite-head fact in the Gap-2 tick-phase tail blocker. Downstream, exactPathClass_zero_subsingleton quotes it twice to prove Subsingleton (ExactPathClass 0), and finset_univ_exactPathClass_zero collapses Finset.univ to the singleton {isolatedClass 0}.
Those facts feed the impossibility half of the R4 residual: shell-0 mass concentrates in one tick fiber for every phase, so no global TickFiberMassBalanced exists. The module then repairs via eventual balance (late amplitudes die; the finite head is irrelevant to OscillatoryTail). The sharper terminal candidate SignatureFin8OscillatoryTailBlocker remains defined but open; this lemma does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.