r0StructuralConstraints
plain-language theorem explainer
Boolean filter on four-sector integer r0 assignments: down is negative, lepton exceeds electroweak which exceeds up, and the four values sum to the fixed structural target 147. The O1 yardstick enumeration uses it to cut the full permutation list down to the canonical assignment. Implemented as a pure conjunction of four decidable integer comparisons.
Claim. Given an integer assignment $a$ to the lepton, up, down, and electroweak sectors, return true if and only if $a_{\mathrm{down}} < 0$, $a_{\mathrm{lepton}} > a_{\mathrm{ew}} > a_{\mathrm{up}}$, and $a_{\mathrm{lepton}} + a_{\mathrm{up}} + a_{\mathrm{down}} + a_{\mathrm{ew}} = V\cdot W + E_{\mathrm{passive}}$ (the structural r0 sum target, equal to 147).
background
The module treats the O1 yardstick discussion as a finite combinatorial search. One starts from four candidate r0 values, forms every sector-to-value assignment (all permutations of four integers onto lepton, up, down, electroweak), and retains only those that pass structural filters drawn from the yardstick principle. The surviving choice set is expected to collapse to a singleton.
An r0 assignment is simply a 4-tuple of integers, one per sector. The sum target is fixed by geometry and counting: cube vertices in dimension $D$ times the number of wallpaper groups, plus the passive-field edge count, which evaluates to 147. The filter also encodes a sign and ordering pattern: the down sector is negative, and the remaining three sectors are strictly ordered lepton above electroweak above up.
Upstream, the same module defines the parallel B_pow structural filter and the shared enumeration scaffolding. Cosmology species labels for up and down appear only as naming context for the sectors, not as dynamical input to this predicate.
proof idea
Definition, not a proof. The body is the Boolean conjunction of four decide calls on integer propositions: down negative, lepton strictly above electroweak, electroweak strictly above up, and the four-sector sum equal to the fixed r0 sum target. No lemmas are invoked; decidability of integer comparison and equality supplies the Bool values.
why it matters
This predicate is the gate for the r0 half of the O1 choice-set collapse. Downstream, validR0Assignments is exactly the full permutation list filtered by it. The equivalence r0_constraints_true_iff identifies the Bool form with the Prop-level principle constraints, so uniqueness theorems can switch representations freely.
Under affine sector-role hypotheses and a depth-gap relation, the filter reduces to the sum condition alone (r0_bool_constraints_iff_sum_under_affine_roles_and_depth_gap), and those same roles force the filter to hold (r0_bool_constraints_forced_from_affine_roles_and_sum). The anchor assignment is shown to pass (anchor_r0_constraints_from_principle), and any assignment in the enumerated pool that satisfies the principle constraints is forced equal to the canonical r0 tuple (r0_constraints_force_canonical). Together these close the combinatorial side of the yardstick r0 assignment, parallel to the B_pow singleton collapse in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.