CubeCell
plain-language theorem explainer
Names the three subcell types of the hypercube Q_d that matter for fermion generation coupling: vertices (CW-dim 0), edges (CW-dim 1), and faces (CW-dim 2). Anyone working the generation-torsion schedule or the edge-before-face ordering cites this as the carrier type. It is a plain inductive enumeration with decidable equality; no proof content.
Claim. For each dimension $d \in \mathbb{N}$, the type of generation-relevant subcells of the hypercube $Q_d$ has three constructors: vertex (CW-dimension $0$), edge (CW-dimension $1$), and face (CW-dimension $2$), with decidable equality.
background
The module derives the edge-before-face excitation ordering for fermion generation torsion from the CW-filtration of the $D=3$ cube $Q_3$, together with $J$-cost monotonicity on $\varphi$-power ratios. The 3-cube has the standard skeleton filtration: 8 vertices (0-skeleton), 12 edges of which 11 are passive (1-skeleton), and 6 faces (2-skeleton).
When generation excitations couple to subcells in CW-dimension order, the cumulative torsion schedule ${0, 11, 17}$ appears: Gen 1 couples only to the 0-skeleton ($\tau=0$), Gen 2 adds 1-cells ($\tau=11$), Gen 3 adds 2-cells ($\tau=17$). The cost functional then gives the strict inequality $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$.
This inductive type is the discrete label set for those three skeleton levels. Companion maps assign CW-dimension ($0,1,2$), subcell counts, and passive-coupling multiplicities (vertices contribute $0$; edges contribute the passive-field count; faces contribute all six faces).
proof idea
No proof: this is an inductive definition with three nullary constructors and a derived DecidableEq instance. Downstream lemmas pattern-match on the constructors (e.g. cases cell) and read off the associated CW-dimension or passive-coupling value by definitional reduction.
why it matters
This type is the geometric vocabulary for the Excitation Ordering Theorem on $Q_3$. Downstream results that depend on it include the strict dimensional comparison $\mathrm{cwDim}(\mathrm{edge}) < \mathrm{cwDim}(\mathrm{face})$, the claim that edges are the minimal nontrivial excitation among cells with positive passive coupling, the structure packing the full ordering theorem, and the certificate that the CW-cumulative torsion matches the canonical generation schedule.
It makes precise why edges precede faces: the ordering is dimensional (CW-dim $1 < 2$), not numerical (face count $6$ is smaller than passive-edge count $11$). That distinction replaces ad-hoc mode labels in the older cube-admissible-torsion story with a single filtration principle tied to the $D=3$ cube forced by the T8 landmark. The remaining open premise is that excitations actually couple in CW-dimension order; the type itself only supplies the labels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.