generation_ordering
plain-language theorem explainer
The declaration proves that the count of passive field edges at dimension three lies strictly between zero and the number of wallpaper groups. Mass baseline work in Recognition Science cites the result to treat generation torsion ordering as derived rather than assumed. The proof reduces to two direct numerical checks on the concrete values eleven and seventeen.
Claim. For spatial dimension $D=3$, let $E_ {pass}(D)$ be the number of passive field edges and $W$ the number of wallpaper groups. Then $0 < E_{pass}(D) < W$.
background
The module derives baseline rung integers from the combinatorics of the three-cube $Q_3$, upgrading several former boundary assumptions to derived status. Passive field edges are defined as total cube edges minus active edges per tick, giving the concrete value 11 at $D=3$. Wallpaper groups are the fixed crystallographic count of 17 distinct two-dimensional symmetry groups. The local setting traces every integer result in the file to the single input $D=3$.
proof idea
The proof is a one-line wrapper that applies native_decide twice: once to confirm zero is less than eleven, once to confirm eleven is less than seventeen.
why it matters
This supplies the B-14 derived item confirming generation torsion is strictly ordered. It feeds the neutrino rung theorem that sets the neutrino baseline integer to negative fifty-four. The result closes one of the boundary assumptions listed in the module by showing all such quantities follow from cube geometry at $D=3$, consistent with the framework's reduction of spatial dimension to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.