excitation_ordering_implies_filtration
plain-language theorem explainer
Assuming the excitation ordering theorem on the 3-cube (edge before face by CW dimension, CW cumulative torsion equal to the canonical generation schedule, and strict J-cost ordering), the full cube generation filtration package holds for that schedule. Mass and generation-torsion arguments cite this as the bridge from the ordering hypothesis to the filtration API. Proof is a rewrite along the torsion-equality field, then the existing CW-torsion filtration lemma.
Claim. If the excitation ordering theorem holds on $Q_3$ (CW-dim(edge) $<$ CW-dim(face), CW cumulative torsion equals the canonical generation torsion schedule $\{0,11,17\}$, ground excitation cost is zero, and edge cost is strictly below face+edge cost), then the cube generation filtration package holds for the canonical generation torsion.
background
The module treats fermion generation torsion as arising from the CW-filtration of the spatial 3-cube $Q_3$ (forced $D=3$ in the RS chain). The 0-skeleton has 8 vertices; the 1-skeleton contributes 11 passive edges; the 2-skeleton adds 6 faces. Coupling excitations in CW-dimension order yields the cumulative torsion schedule ${0,11,17}$ for generations 1–3.
The excitation ordering theorem packages four facts: edge dimension strictly below face dimension; CW cumulative torsion equals the canonical generation torsion; ground cost vanishes; and the second rung costs strictly less than the third under the excitation cost (J-cost on $\varphi$-power ratios). The cube generation filtration is the structured package that records this schedule and its dimensional increments for downstream mass work.
J-cost is the unique nonnegative cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain (T5); monotonicity on $\varphi$-powers gives $J(\varphi^0)=0<J(\varphi^{11})<J(\varphi^{17})$.
proof idea
Term-mode, two steps. Rewrite the goal along the field of the hypothesis that equates CW cumulative torsion with the canonical generation torsion (so the filtration target becomes the CW object). Then apply the already-proved lemma that CW cumulative torsion carries a cube generation filtration. No new arithmetic; pure transport of structure along the equality.
why it matters
Closes the implication from the ordering hypothesis to the filtration API used by mass and generation bookkeeping. The sole downstream consumer is the excitation ordering certificate, which conjoins the ordering theorem, this filtration recovery, minimality of edge-supported nontrivial coupling, and the numerical comparison that faces are fewer than passive edges (yet edges come first by dimension).
In the framework this is the CW route to why edges precede faces in CubeAdmissibleTorsion: geometry of $Q_3$ (T8, $D=3$) plus J-monotonicity on the $\varphi$-ladder, rather than ad hoc mode labels. The module still treats “excitations couple in CW-dimension order” as a structural premise, not yet derived from the cost functional alone; this theorem does not discharge that premise, it only shows the premise yields the full filtration package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.