burnsideMass_two_two_two
plain-language theorem explainer
The Burnside mass of exact complexes with two vertices, two edges, and two tetrahedra equals 512. Gap-2 gravity workers cite it as the numerical base case for cube-signature mass at shell 2. The proof rewrites through the power form of Burnside mass and evaluates the three factorials by norm_num.
Claim. The Burnside mass at signature $(v,e,t)=(2,2,2)$ equals $512$ in $\mathbb{R}$. Equivalently, under the banked identity $\mathrm{burnsideMass}(v,e,t)=|\mathrm{ExactComplex}\,v\,e\,t|/(v!\,e!\,t!)$, one has $|\mathrm{ExactComplex}\,2\,2\,2|/(2!)^3=4096/8=512$.
background
This module is the Wave C1 R4 terminal attack on the Fin-8 oscillatory tail blocker for Gap 2. Honest status: the blocker Prop itself is not proved; what lands are packaging lemmas for signature and Burnside masses, plus a stall diagnosis that single-signature concentration fails for large shells.
An ExactComplex v e t is a cap-free combinatorial complex with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra, carrying abstract incidence data and no cap inequalities. The banked Burnside identity packages orbit counting as
$$\mathrm{signatureMass}(v,e,t)=|\mathrm{ExactComplex},v,e,t|/(v!\cdot e!\cdot t!)=\mathrm{burnsideMass}(v,e,t).$$
Shell mass is the sum of signature masses over the shell. The cube signature $(n,n,n)$ is the natural diagonal test case; at $n=2$ the factorials are tiny and the count is elementary.
proof idea
Term/tactic hybrid, two steps. First rewrite with the sibling identity burnsideMass_eq_pow, which exposes Burnside mass as a concrete power/factorial expression in the three size parameters. Then norm_num with Nat.factorial evaluates $2!=2$ three times and finishes the arithmetic to $512$. No combinatorial enumeration is performed in-kernel; the cardinality side is already folded into the power form.
why it matters
Immediate parent is signatureMass_cube_two, which rewrites cube signature mass at shell 2 through signatureMass_eq_burnside and the cube-component projections, then applies this lemma to obtain $512$. That fact is listed among the landed theorems of the Wave C1 R4 attack (alongside fiberwise exact-shell amplitude and the honest reformulation of the blocker as a signature-mass cancellation sequence).
In the broader Gap-2 program these mass lemmas test whether a single dominant signature can obstruct Fin-8 cancellation. External enumeration shows cube dominance only in a mesoscopic window ($n\lesssim 200$); by $n\approx 400$ the top piece is below $1/8$ of shell mass. This $n=2$ evaluation is the smallest nontrivial cube check, not an asymptotic claim. It does not flip gap2_continuum_and_measure and introduces no sorry or new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.