cubeSig_components
plain-language theorem explainer
The cube shell signature at level n has equal vertex, edge, and tetrahedron counts, each exactly n. Gravity and shell-amplitude workers cite it to reduce cube Burnside mass to the diagonal evaluation burnsideMass(n,n,n). The proof is pure definitional equality: three reflexivity steps from the cube constructor.
Claim. For every natural number $n$, if $c_n$ denotes the cube shell signature $(n,n,n)$ at level $n$, then its vertex count, edge count, and tetrahedron count each equal $n$: $\mathrm{sig}_V(c_n)=n$, $\mathrm{sig}_E(c_n)=n$, and $\mathrm{sig}_T(c_n)=n$.
background
In the SevenGaps gravity stack, a shell signature at level $n$ is a triple of bounded counts (vertices, edges, tetrahedra) whose componentwise maximum is $n$. The projections $\mathrm{sig}_V$, $\mathrm{sig}_E$, $\mathrm{sig}_T$ read those three coordinates. The cube signature is the diagonal point $(n,n,n)$, packaged as a well-typed shell signature by the max-identity $\max(n,\max(n,n))=n$.
This module is the Wave C1 R4 terminal attack on the Fin-8 oscillatory tail blocker. The honest status is that the blocker Prop itself is not proved: single-signature mass concentration fails asymptotically, and cube dominance holds only in a mesoscopic window. What has landed are Burnside packaging lemmas, fiberwise amplitude grouping, and explicit cube-mass evaluations.
Upstream, cubeSig builds the diagonal signature, and the three sig* abbrevs are pure projections. The present fact simply records that those projections recover $n$ on the cube.
proof idea
Term-mode proof by a triple of reflexivity. Unfolding cubeSig n yields the triple of Fin values each equal to $n$ (with the max-self proof obligation already discharged in the constructor). Applying sigV, sigE, sigT is definitional projection, so each equality is rfl. No lemmas are invoked.
why it matters
Parent theorems signatureMass_cube and signatureMass_cube_two rewrite cube signature mass through the banked identity signatureMass = burnsideMass after substituting the three component equalities. That yields the general diagonal evaluation and the concrete shell-2 value $512 = 4096/8$.
In the Gap2 attack these cube masses diagnose the mesoscopic window where $(n,n,n)$ dominates shell mass (above $1/2$ for $n\lesssim 200$) before falling below $1/8$ by $n\approx 400$. The fact is scaffolding for the honest reformulation of the oscillatory-tail blocker as an explicit signature-mass cancellation sequence; it does not flip gap2_continuum_and_measure and sits outside the T0–T8 forcing chain proper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.