vertex_dim_lt_edge_dim
plain-language theorem explainer
Vertices of the D-cube sit strictly below edges in CW dimension: dim(vertex)=0 < dim(edge)=1. Anyone citing the CW-filtration argument for generation torsion (edge before face) needs this elementary comparison. The proof is a one-step decidability check on the concrete naturals 0 and 1.
Claim. For the spatial dimension $D=3$, the CW dimension of a vertex subcell of the hypercube $Q_D$ is strictly less than the CW dimension of an edge subcell: $\mathrm{cwDim}(\mathrm{vertex}) < \mathrm{cwDim}(\mathrm{edge})$.
background
The module builds the edge-before-face excitation ordering for fermion generation torsion from the CW-filtration of the 3-cube $Q_3$. Subcells relevant to generation coupling are typed as vertices (CW-dim 0), edges (CW-dim 1), and faces (CW-dim 2). The inductive type CubeCell packages those three levels; its dimension map sends vertex to 0 and edge to 1.
Spatial dimension is fixed at $D=3$ by the forcing chain (T8). The 0-skeleton has 8 vertices, the 1-skeleton has 12 edges (11 passive), and the 2-skeleton has 6 faces. When excitations couple in CW-dimension order, the cumulative torsion schedule becomes ${0,11,17}$, and J-cost monotonicity on $\varphi$-power ratios then forces $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$.
This lemma is the first strict inequality in that dimensional ladder: vertices sit below edges.
proof idea
One-line decidability proof. After unfolding the CW-dimension clauses, the goal is the concrete inequality $0 < 1$ on naturals, which decide discharges. No lemmas are invoked.
why it matters
In the Recognition Science mass sector, generation torsion is otherwise labeled by hand as ground/edge/face modes inside the cube-admissible torsion schedule. The CW-filtration story replaces those labels by a single geometric principle: couple in order of subcell dimension. This comparison is the first rung of that ordering (dim 0 before dim 1); its sibling edge-before-face comparison is the second.
Together they underwrite why the first nontrivial excitation is edge-supported ($\tau=11$) and the next is face-supported ($\tau=17$), matching the canonical schedule and the strict J-cost chain on $\varphi$-powers. The module still treats "excitations couple in CW order" as a structural premise rather than a derived law; this lemma only supplies the geometric inequality that premise needs. No downstream theorems currently depend on it (used_by is empty), so it is infrastructure for the filtration argument itself and for any later closure of the remaining premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.