bpowStructuralConstraints
plain-language theorem explainer
Boolean filter on four-sector B_pow integer assignments: opposite up/EW signs with positive EW, absolute-value complement of lepton and EW equaling down, and sector sum equal to the structural target A=1. Used by the O1 yardstick choice-set enumeration to discard non-structural permutations before uniqueness. Pure conjunction of decidable equalities and inequalities; no proof content.
Claim. For an integer assignment $(B_\ell, B_u, B_d, B_{\mathrm{EW}})$ to the lepton, up, down, and electroweak sectors, the structural filter returns true iff $B_u = -B_{\mathrm{EW}}$, $|B_\ell| + |B_{\mathrm{EW}}| = B_d$, $B_u < 0$, $B_{\mathrm{EW}} > 0$, and $B_\ell + B_u + B_d + B_{\mathrm{EW}} = A$ with structural target $A = 1$.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are assigned to the four sectors (lepton, up, down, EW) by enumerating permutations, then filtered by structural constraints from the yardstick principle. Valid survivors collapse to a singleton.
A sector assignment is a four-tuple of integers. The structural sum target is the anchor constant $A$, cast to $\mathbb{Z}$ and equal to $1$. Upstream cosmology species labels (up/down quark DOF counts) are only ambient context; the filter itself is purely arithmetic on the four integers.
The companion principle-level constraints package the same conditions as a Prop; this definition is the decidable Bool form used for list filtering.
proof idea
Definition, not a theorem. It is the conjunction of five decide atoms: (i) up equals minus EW; (ii) absolute values of lepton and EW sum to down; (iii) up strictly negative; (iv) EW strictly positive; (v) the four components sum to the structural target $A=1$. Evaluation is by native integer decidability.
why it matters
This is the gate used by validBPowAssignments and by the forcing theorems that collapse the choice set. Downstream results show the filter holds for the anchor assignment, that principle-level constraints are equivalent to the boolean filter, and that any assignment in the full permutation pool satisfying the principle constraints must equal the canonical $B_{\mathrm{pow}}$ tuple. Related equivalences tie the filter to active-unit magnitude $|B_{\mathrm{EW}}|=A$ once down-role or passive/active edge roles are fixed. In the Recognition yardstick story this is the concrete O1 sieve that turns a finite assignment search into uniqueness of the sector powers on the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.