r0_order_constraints
plain-language theorem explainer
The sector φ-exponent offsets obey three order/sign constraints: the down-quark offset is negative, and lepton exceeds electroweak, which exceeds up-quark. Anyone filtering finite candidate yardstick assignments cites this. The proof unfolds the four closed-form integer formulas and evaluates them by norm_num.
Claim. With the derived sector offsets $r_0$ from wallpaper and cube geometry, one has $r_0(\mathrm{down})<0$, $r_0(\mathrm{lepton})>r_0(\mathrm{electroweak})$, and $r_0(\mathrm{electroweak})>r_0(\mathrm{up})$.
background
Open Problem O1 asks why each particle sector receives a specific binary power $B_{\mathrm{pow}}$ and offset $r_0$ from the counting layer. The module's answer is sector-to-cube coupling: each sector couples to a distinct level of the 3-cube hierarchy (passive edges, active edge, total edges), and the yardstick formulas encode that coupling.
The offsets $r_0$ are wallpaper-modulated integers built from $W=17$ (wallpaper groups), total edges $E=12$, and the active-edge count $A=1$: lepton $4W-6=62$, up $2W+A=35$, down $E-W=-5$, electroweak $3W+4=55$. As the anchor definition states, these are "NOT arbitrary—they come from wallpaper + cube geometry." Spatial dimension $D=3$ (forced by T8/T9) fixes the cube counts underlying $E$ and $A$.
The present result records only the sign and total order among those four integers. Downstream, the finite-choice filter for yardstick assignments treats them as hard constraints on admissible $r_0$ tuples.
proof idea
Term-mode proof by direct evaluation. First simp only rewrites each sector via the closed equalities r0_DownQuark_eq, r0_Lepton_eq, r0_Electroweak_eq, and r0_UpQuark_eq, replacing the four applications of r0 by the integers $-5$, $62$, $55$, and $35$. Then norm_num discharges the three concrete inequalities $-5<0$, $62>55$, and $55>35$. No induction or external arithmetic lemmas beyond normalization.
why it matters
This is one conjunct block of the $r_0$ finite-choice filter in the Yardstick Assignment Principle (O1). Downstream, anchor_r0_structural_identities packages exactly these three inequalities together with the sum identity against the target budget, stating that "the r0 filter constraints are satisfied by the anchor assignment, and each conjunct corresponds to proved ordering/sum identities."
In the broader RS chain the offsets sit on the φ-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Fixing their signs and order narrows which integer 4-tuples can arise from cube-plus-wallpaper geometry at $D=3$, so the uniqueness argument under exhaustion constraints can treat the anchor assignment as the unique survivor rather than an ad hoc fit. It does not itself derive the formulas; it certifies the filter predicates those formulas must pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.