r0PrincipleConstraints
plain-language theorem explainer
Prop-level filter on integer r0 sector assignments: down is negative, lepton exceeds electroweak which exceeds up, and the four values sum to the structural target 147. Yardstick verification cites it when collapsing the finite r0 choice set to the canonical assignment. It is a four-conjunct definition, not a proved theorem.
Claim. An integer assignment $(r_\ell, r_u, r_d, r_{\mathrm{ew}})$ of $r_0$ values to the lepton, up, down, and electroweak sectors satisfies the principle constraints when $r_d < 0$, $r_\ell > r_{\mathrm{ew}} > r_u$, and $r_\ell + r_u + r_d + r_{\mathrm{ew}} = V\cdot W + E_{\mathrm{passive}}$ (the structural sum target, equal to $147$).
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $r_0$ values are assigned to the four sectors (lepton, up, down, electroweak) by enumerating permutations, then filtered by structural constraints. The valid choice set is claimed to collapse to a singleton.
An $r_0$ assignment is a 4-tuple of integers, one per sector. The structural sum target is $V\cdot W + E_{\mathrm{passive}}$, built from cube vertices in dimension $D$, wallpaper-group count, and passive-field edges; numerically it is $147$. The species labels up and down appear only as sector names here (their cosmological DOF counts are not used in the Prop).
The Boolean filter r0StructuralConstraints is the decidable counterpart; this definition is the Prop-level form of the same four conditions, used in classical reasoning and forcing lemmas.
proof idea
Definitional, not a proof. The body is the conjunction of four atomic conditions on the assignment fields: negativity of the down component, the two strict order inequalities lepton $>$ electroweak $>$ up, and equality of the four-way sum with the structural sum target. Downstream equivalence with the Boolean filter is a one-line unfold-and-simp argument.
why it matters
This Prop is the admissibility gate for $r_0$ in the yardstick choice-set story. It is the hypothesis that forces membership in the valid list and equality with the canonical assignment (r0_constraints_force_canonical). Equivalence with the Boolean structural filter (r0_constraints_true_iff) lets classical and decidable paths share one meaning.
Under fixed affine up/down roles and a depth gap, the order conjuncts become derived, so the full principle constraints reduce to the sum alone (r0_principle_iff_sum_under_affine_roles_and_depth_gap); the same package yields unrestricted forcing to canonical $r_0$ without pool membership. At module scale it feeds the cube-partition packaging that forces the joint $B_{\mathrm{pow}}$ and $r_0$ filter family without enumeration. That is the O1 progress claim: structural roles plus sum pin the yardstick, rather than an ad hoc pick among permutations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.