bpow_bool_constraints_iff_active_unit_under_down_role
plain-language theorem explainer
Under a fixed down-role value, opposite-sign up versus EW, sector-sum target, and positive EW, the boolean structural B_pow filter holds exactly when the EW absolute value equals the active edge count A (=1). Anyone enumerating yardstick sector assignments cites this to collapse the choice set. Proof is a one-line rewrite from the boolean filter to the principle-level iff.
Claim. Let $a$ assign integers to the lepton, up, down, and electroweak sectors. Assume $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$, $a_{\mathrm{up}}=-a_{\mathrm{ew}}$, the four sector values sum to the $B_{\mathrm{pow}}$ sum target, and $a_{\mathrm{ew}}>0$. Then the structural boolean $B_{\mathrm{pow}}$ constraints hold if and only if $|a_{\mathrm{ew}}|=A$, where $A$ is the active edge count per tick.
background
This 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, electroweak) by permutation, then filtered by structural constraints. Valid choice sets are claimed to collapse to singletons.
A BPowAssignment is just four integers, one per sector. The constant $A$ is the active edge count per tick ($A=1$ in the gap derivation). $E_{\mathrm{total}}$ is the anchor total used to pin the down-role hypothesis $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$. The sum target is the structural total that all four sectors must meet.
The sibling principle-level statement equates the non-boolean principle constraints to $|a_{\mathrm{ew}}|=A$ under the same role hypotheses. The present theorem is the boolean-filter packaging of that equivalence, matching the enumeration pipeline that decides constraints by a Bool check.
proof idea
One-line term wrapper. Rewrite the left-hand side with the lemma that the structural boolean constraints equal true exactly when the principle constraints hold, then apply the already-proved principle-level equivalence under the same four hypotheses (fixed down role, opposite-sign up/EW, sector sum, positive EW).
why it matters
In the yardstick assignment enumeration, boolean filters are what the choice-set search actually runs. This theorem licenses replacing that filter, once the down-role and sign/sum hypotheses are in force, by the single arithmetic check $|a_{\mathrm{ew}}|=A$. That is the active-unit condition on the electroweak sector.
The module goal is that valid $B_{\mathrm{pow}}$ (and $r_0$) assignments collapse to singletons under structural constraints. Pinning EW to absolute value $A=1$ is a concrete step in that collapse. No downstream consumers are recorded yet; the result sits at the filter layer of the O1 progress module rather than feeding a named parent theorem in the forcing chain (T0–T8). It is local verification infrastructure for the mass yardstick, not a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.