classMassPi
plain-language theorem explainer
Defines the π-weighted class mass of a fibre of named (4,2,0) incidences: the sum of the ambient stationary weight over that fibre. Gravity and coarea arguments cite it when comparing Aut-distinct complexes at equal census. The body is a one-line Finset sum of the named weight.
Claim. For a named stationary weight $\pi$ on $(4,2,0)$ incidences and a finite fibre $F$ of such incidences, the $\pi$-weighted class mass is $\sum_{e \in F} \pi(e) \in \mathbb{Q}$.
background
Gap 2 (A20, lane C16) studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Legal moves have rate 1; rate symmetry plus irreducibility force a unique stationary law that is uniform on each finite cap (measured at cap-3; derived-unformalized at cap-4, host of the equal-census witnesses).
A named weight $\pi$ is a rational function on incidences of type $\mathrm{Fin},2 \to \mathrm{Fin},4 \times \mathrm{Fin},4$, i.e. the ambient stationary law pulled back to the equal-census sector. A fibre is a finite set of such named incidences representing one Aut-distinct complex under the C35 firewall (process language never names Aut, orbit, or gauge class).
Related weight notions elsewhere (label density, quotient pushforward mass, Hamming weight, Gibbs weight) are distinct; here weight means only the named stationary coordinate summed over the fibre.
proof idea
Definitional one-liner: evaluate the Finset sum of $\pi$ over the fibre. No lemmas, no tactics beyond the sum notation. Downstream, the uniform specialization replaces each summand by $1/N$ and collapses via Finset.sum_const to fibre cardinality over $N$.
why it matters
This is the mass instrument for the Poisson coarea ratio test. The module headline requires that at equal census $(4,2,0)$ the stationary class-mass ratio of two Aut-distinct complexes is exactly $1/2$ (directed Aut correction). Downstream, classMassRatioPi forms the ratio of the two witness fibres, and classMassPi_of_uniform shows that under uniform $\pi=1/N$ the mass equals fibre-card$/N$, so the ratio becomes $24/48=1/2$.
The definition stays inside the C35 firewall: it never mentions Aut or gauge classes, only named weight summed on a fibre. Factorial emergence ($nV!,nE!,nT!$ as sort-respecting arrival count) and orbit-stabilizer appear only on the conclusion side when interpreting fibre sizes. Flag 8 is unmoved; FullTheoryLedger is not imported.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.