exactPathClass_zero_subsingleton
plain-language theorem explainer
The exact complexity shell at level zero is a singleton: any two exact path classes of complexity zero coincide. Gap-analysis and gravity work cite this as the finite-head degeneracy that forces class-mass onto a single tick fiber for every phase assignment. The proof is a one-line Subsingleton constructor rewriting both arguments by the unique empty-class identification.
Claim. The type of exact path classes of complexity $0$ is a subsingleton: for all $a,b$ in that type, $a=b$. Equivalently, the exact complexity shell at level zero consists solely of the empty-signature class.
background
In the exact-shell gauge, an exact path class of complexity $n$ is a pair of a shell signature of weight $n$ with a quotient of labeled exact complexes by global equivalence. No bounded-complexity cap appears in the definition; the object is the full combinatorial shell.
At $n=0$ the only shell signature is the empty triple $(0,0,0)$, and every class collapses to the isolated empty-complex class. The sibling identification states that every class at shell zero equals that unique empty class.
This module hardens the R4 residual in the Gap-2 tick-phase story: finite-head impossibility (shell zero is a singleton, so mass cannot balance across the eight tick fibers) together with an eventual-balance repair that kills late amplitudes for oscillatory-tail arguments.
proof idea
Term-mode Subsingleton constructor. For arbitrary $a,b$ in the shell-zero path-class type, rewrite both sides by the unique-empty-class theorem; both become the isolated empty class, so $a=b$. No case analysis or induction beyond what that identification already performed.
why it matters
Feeds the design-named packaging theorem that pairs shell-zero subsingletonhood with the concrete mass-concentration statement: for every tick-phase assignment there is a single fiber carrying the full class measure at shell zero and all other fibers vanish. That packaging is the finite-head half of the all-shell balance impossibility used to block naive TickFiberMassBalanced hypotheses.
In the Wave C1 R4 hardening narrative this is clause (b): shell zero is a singleton class, so class-mass concentrates in one tick fiber for every phase map, hence no global tick-fiber mass balance exists. The residual open question remains existence of a substrate phase with oscillatory tail (the sharper SignatureFin8 blocker is defined but not proved). Does not touch the continuum-and-measure gap flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.