ordering_is_dimensional_not_numerical
plain-language theorem explainer
For the 3-cube, face count (6) is numerically smaller than passive edge count (11), yet edges precede faces in the CW filtration because dim(edge)=1 < dim(face)=2. Anyone citing the geometric origin of generation torsion order needs this split. The proof is a two-conjunct constructor: arithmetic simplification for the numerical inequality, and the existing edge-before-face dimension lemma for the geometric one.
Claim. With spatial dimension $D=3$, the number of cube faces is strictly less than the number of passive field edges as integers, $$2D < D\cdot 2^{D-1}-1,$$ while the CW dimension of an edge subcell is strictly less than that of a face subcell: $\mathrm{cwDim}(\mathrm{edge})=1 < 2=\mathrm{cwDim}(\mathrm{face})$.
background
The module derives fermion generation torsion ordering from the CW-filtration of the $D=3$ cube $Q_3$. Subcells relevant to generation coupling are vertices (CW-dim 0), edges (CW-dim 1), and faces (CW-dim 2). Passive field edges are total cube edges minus the single active edge per tick: for $D=3$ this is $12-1=11$. Cube faces number $2D=6$.
The cumulative torsion schedule is then ${0,11,17}$: ground couples only to the 0-skeleton; the first excitation adds 1-cells ($\tau=11$); the second adds 2-cells ($\tau=11+6=17$). J-cost monotonicity on $\varphi$-power ratios then gives $J(\varphi^0)<J(\varphi^{11})<J(\varphi^{17})$.
Upstream constants fix $D=3$ (forced by the linking/T8–T9 chain), $\mathrm{cube_edges}(d)=d\cdot 2^{d-1}$, $\mathrm{cube_faces}(d)=2d$, and $\mathrm{passive_field_edges}(d)=\mathrm{cube_edges}(d)-1$. The inductive type CubeCell packages the three subcell kinds with their CW dimensions.
proof idea
Term-mode proof by constructor on the conjunction.
Left conjunct: simp unfolds cube_faces, passive_field_edges, cube_edges, active_edges_per_tick, and $D$, reducing $6<11$ to true arithmetic.
Right conjunct: one-line application of the sibling lemma edge_dim_lt_face_dim, which is the pure geometric fact $\mathrm{cwDim}(\mathrm{edge})<\mathrm{cwDim}(\mathrm{face})$.
why it matters
This lemma is the explicit witness that generation ordering is geometric, not a "smallest torsion increment first" rule. Numerically faces (6) beat edges (11), so a pure size ordering would put faces first; the CW dimension reverses that. Downstream, excitation_ordering_certificate packages this fact as the first proved bullet of the full CW-filtration certificate (dimensional ordering, cumulative torsion matching the canonical schedule, J-cost strict order, first increment = passive edges, second = faces).
In the broader Recognition chain this sits under the mass/generation sector: $D=3$ is the T8 landmark, the eight-tick octave and passive-edge count 11 feed the $\varphi$-ladder mass formula, and the filtration principle replaces ad-hoc mode labels in CubeAdmissibleTorsion by a single geometric premise. The remaining open premise is that excitations actually couple in CW-dimension order; this theorem does not discharge that premise, only the dimensional-vs-numerical distinction once the premise is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.