fiberExcess
plain-language theorem explainer
The labeled-fiber excess is the explicit complex sum that separates the standing labeled path sum from the quotient-first path sum when weights are constant on triangulation classes. For each class it contributes (|fiber| − 1) times the projector coefficient μ at a representative times the class weight. Seven-Gaps and gravity authors cite it as the honest residue after the P2c panel killed unconditional labeled/quotient equality. The body is a plain finite sum over the finite class quotient; no cancellation is assumed.
Claim. For a bound $B\in\mathbb{N}$ and a class weight $w_q:\mathrm{TriangulationClass}_B\to\mathbb{C}$, define the fiber excess by $$E(B,w_q)=\sum_q\bigl(|\mathrm{fiber}(q)|-1\bigr)\,\mu(\mathrm{out}\,q)\,w_q(q),$$ summed over triangulation classes of bound $B$. Here $|\mathrm{fiber}(q)|$ is the cardinality of the relabeling fiber of $q$, $\mathrm{out}\,q$ is a chosen representative, and $\mu$ is the scalar coefficient in the quadratic projector relation.
background
Pillar 2 of the Seven Gaps program builds a quotient-first path-sum object on bounded triangulation classes. The standing labeled path sum $Z$, when the weight is constant on each relabeling class, expands as $\sum_q |\mathrm{fiber}(q)|,\mu(\mathrm{out},q),w_q(q)$. The promoted quotient-first object is the thinner sum $Z_q=\sum_q \mu(\mathrm{out},q),w_q(q)$ (intended, under orbit-stabilizer, to match a $1/|\mathrm{Aut}|$ weighting).
The module inherits a finite class quotient from ClassPushforward and the non-singleton fiber fact for edge classes. No global orbit-stabilizer theorem is proved for the full bounded carrier: signatures vary, so a single relabeling group action is not supplied. The honesty boundary is that labeled $Z$ and $Z_q$ are not unconditionally equal.
The scalar $\mu$ is the coefficient in the quadratic projector relation $A^2=\mu A$ from the cost/N-dim projector layer. Fiber cardinality is the size of the equivalence class under the relabeling setoid.
proof idea
Pure definition: a noncomputable finite sum over the finite type of triangulation classes of bound $B$. Each summand is the product of three complex factors: the integer fiber cardinality cast to $\mathbb{C}$ minus one, the real projector coefficient $\mu$ at Quotient.out q cast to $\mathbb{C}$, and the class weight $w_q(q)$. No lemmas are applied; the term is the mathematical object used by the exact-relation theorems.
why it matters
This is the booked residue after the P2c panel killed the unconditional claim $Z=\sum_q w_q/|\mathrm{Aut},q|$. The exact relation theorem writes the labeled class-constant path sum as $Z_q$ plus this excess, and is the honest replacement for that killed equality. The IFF form states $Z_q$ equals labeled $Z$ precisely when the excess vanishes; a sufficient singleton-fiber criterion forces vanishing, but ClassPushforward already shows non-singleton fibers in general.
Downstream, the Gap2 labeled-weight bridge class records that each class of $n$ labeled presentations contributes $n\cdot\mu$, with this excess as the residue and "no candidate for removing it." The grounding theorem for quotient-first status flags ties the RED flags to the inherited non-singleton fiber fact and keeps the fiber factor on the bridge. In the gravity Seven Gaps stack this definition is the explicit obstruction term, not a convention that erases it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.