ExcitationOrderingTheorem
plain-language theorem explainer
Packages six conditions that constitute the excitation ordering theorem on the 3-cube: edge CW-dimension precedes face, CW-cumulative torsion equals canonical generation torsion, ground J-cost is zero, edge excitation is strictly cheaper than face-plus-edge, and the two torsion increments equal passive edges and faces. Mass and generation theorists cite it as the Prop interface between Q₃ CW filtration and fermion torsion. Definitional structure only; the inhabitant is assembled in a sibling theorem.
Claim. The excitation ordering theorem on the $D=3$ cube is the conjunction of: (i) CW-dimension of an edge cell is strictly less than that of a face cell; (ii) the CW-cumulative torsion schedule equals the canonical generation torsion; (iii) the excitation $J$-cost of the ground (first) torsion value is $0$; (iv) the $J$-cost of the second torsion value is strictly less than that of the third; (v) the first torsion increment equals the passive field-edge count; (vi) the second torsion increment equals the cube face count $2D$.
background
The module derives edge-before-face generation ordering from the CW filtration of the spatial 3-cube $Q_3$, with $D=3$ forced upstream (T8/T9). Subcells relevant to fermion coupling are the inductive types vertex, edge, face, with CW dimensions $0,1,2$. The 0-skeleton has $2^D=8$ vertices; the 1-skeleton contributes passive field edges (total edges minus the active edge per tick), equal to $11$ at $D=3$; the 2-skeleton contributes $2D=6$ faces.
When excitations couple in CW-dimension order, the cumulative torsion schedule is ${0, 11, 17}$: ground couples only to the 0-skeleton ($\tau=0$), the first excitation adds 1-cells ($\tau=$ passive edges), and the second adds 2-cells ($\tau=11+6$). The Recognition $J$-cost on $\varphi$-power ratios then gives the strict ordering $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$.
This structure records that geometric package as a single Prop. Upstream constants supply cube_faces ($2D$) and passive_field_edges; the remaining premise, that coupling respects CW dimension, is the filtration principle rather than a derived dynamical law.
proof idea
No proof body: this is a structure-as-Prop, a definitional bundle of six fields. Each field is a named hypothesis that a later inhabitant must discharge. The dimensional inequality is the geometric fact $\mathrm{cwDim}(\mathrm{edge})=1 < 2=\mathrm{cwDim}(\mathrm{face})$. Canonical matching equates the CW-cumulative schedule to generation torsion. Ground cost is the unit identity of $J$. Strict cost ordering compares $J$ on the second and third cumulative values. The two increment equations identify successive differences with the integer casts of passive field edges and cube faces. The sibling theorem that builds an inhabitant fills the fields from those lemmas.
why it matters
This is the named claim object for the CW route to generation torsion. Downstream, excitation_ordering_holds constructs an inhabitant for $Q_3$; excitation_ordering_certificate packages it with the cube-generation filtration, passive-coupling dimension bounds, and the numerical inequality faces $<$ passive edges; excitation_ordering_implies_filtration and cwTorsion_has_filtration recover the full filtration package from the canonical-matching field.
In the Recognition chain it explains why the torsion schedule ${0,11,17}$ is not an ad hoc mode label: the increments are forced by the 1- and 2-skeleta of $Q_3$ once coupling respects CW dimension, with $D=3$ from T8. That replaces unexplained ground/edge/face tags in cube-admissible torsion by one geometric principle plus $J$-monotonicity on the $\varphi$-ladder. The open residue is the filtration premise itself: that excitations couple in CW order remains a structural assumption about the coupling mechanism, not yet a consequence of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.