cubeAdmissible_ordered
plain-language theorem explainer
Any cube-admissible generation torsion schedule is strictly ordered: ground below edge mode below face+edge mode, for spatial dimension at least 2. Mass and generation authors cite it to get τ₁ < τ₂ < τ₃ from the structural coupling premise alone, without numeral lookup. The proof rewrites the three mode equations and applies the general generation-ordering lemma plus positivity of the face count.
Claim. Let $d\ge 2$ and let $\tau:\{\mathrm{first},\mathrm{second},\mathrm{third}\}\to\mathbb{Z}$ be cube-admissible: $\tau(\mathrm{first})=0$, $\tau(\mathrm{second})=E_{\mathrm{passive}}(d)$, and $\tau(\mathrm{third})=E_{\mathrm{passive}}(d)+F(d)$ with $F(d)=2d$ the hypercube face count. Then $\tau(\mathrm{first})<\tau(\mathrm{second})$ and $\tau(\mathrm{second})<\tau(\mathrm{third})$.
background
The module Generation Torsion Bridge is the geometric source of truth for charged-generation torsion. It derives the schedule from $D$-cube combinatorics rather than hardcoded integers: ground mode couples to nothing ($\tau=0$), second generation to passive edges ($E_{\mathrm{passive}}$), third to passive edges plus faces ($E_{\mathrm{passive}}+F$). At $D=3$ this yields ${0,11,17}$, matching Anchor and RecogSpec representations pointwise.
Cube-admissible torsion is the explicit structural premise encoding that coupling rule. Its fields fix $\tau$ on the three generations in terms of passive_field_edges and cube_faces (the latter is the standard $F=2d$ face count of the $D$-hypercube). The module stresses that this premise is not yet forced by the Recognition Composition Law alone; it upgrades "raw numerals" to "named structural hypothesis with uniqueness."
Upstream, face positivity is immediate from $F=2d$. The companion lemma generation_ordering_general already records $0<E_{\mathrm{passive}}(d)$ for $d\ge 2$, which supplies the first strict inequality once the ground and edge equations are substituted.
proof idea
Split the conjunction.
Left conjunct: rewrite $\tau(\mathrm{first})=0$ and $\tau(\mathrm{second})=E_{\mathrm{passive}}(d)$ from the admissibility hypothesis, then apply the first half of generation_ordering_general d hd and cast $\mathbb{N}$ to $\mathbb{Z}$.
Right conjunct: rewrite edge and face+edge modes so the goal is $E_{\mathrm{passive}}<E_{\mathrm{passive}}+F$. Unfold $F=2d$ and use omega to get $0<F$ in $\mathbb{N}$; cast to $\mathbb{Z}$ and finish by linarith. No native_decide and no $D=3$ specialization.
why it matters
Strict ordering of generation torsion is the combinatorial backbone of the three-generation mass ladder in Recognition Science. With ground at zero, edge-dressed second generation, and face+edge third generation, the inequalities $\tau_1<\tau_2<\tau_3$ guarantee a strict rung hierarchy before any $\varphi$-power mass formula is applied.
The module certifies that the geometric schedule agrees with Anchor integers and RecogSpec generation torsion, and that cube-admissible torsion has a unique solution. This theorem is the ordering half of that package: once admissibility is assumed, cube arithmetic alone forces the order, matching the CW-filtration intuition (edges before faces) developed more strongly in ExcitationOrdering.
Framework landmarks: $D=3$ spatial dimensions (T8) specializes $F=6$ and $E_{\mathrm{passive}}=11$, recovering the familiar ${0,11,17}$. The remaining open gap, stated in the module doc, is deriving the ground/edge/face coupling rule itself from the RCL rather than taking it as a structural premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.