bpow_bool_constraints_forced_from_passive_active_roles
plain-language theorem explainer
Under passive-edge lepton role, opposite-sign up versus EW, positive EW of magnitude equal to the active-edge count A, and the four-sector sum target, the boolean structural filter on a B_pow assignment returns true. Anyone checking that edge-role assumptions force yardstick structural constraints without enumeration would cite this. The proof is a one-line transfer through the boolean/principle iff from the principle-level forcing lemma.
Claim. Let $a$ assign integers to the lepton, up, down, and electroweak sectors. If the lepton entry equals $-2 E_{\mathrm{passive}}$, the up entry equals the negation of the electroweak entry, the electroweak entry is positive with absolute value equal to the active-edge count $A$, and the four entries sum to the $B_{\mathrm{pow}}$ sum target, then the boolean structural constraints on $a$ evaluate to true.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to sectors by permutation, then filtered by structural constraints. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
A $B_{\mathrm{pow}}$ assignment is a four-tuple of integers (lepton, up, down, electroweak). The active-edge count $A$ is fixed at $1$ per tick in the gap derivation. The sum target is the principle-level total that the four sector powers must meet. Passive-edge lepton role supplies the lepton entry as $-2 E_{\mathrm{passive}}$; the remaining hypotheses encode sign opposition of up and EW, positivity and magnitude of EW, and the global sum.
The boolean structural filter is the decidable counterpart of the principle-level constraint predicate used in the yardstick assignment principle import.
proof idea
One-line term wrapper. Apply the right-to-left direction of the boolean/principle equivalence bpow_constraints_true_iff to the assignment, then feed the principle-level forcing lemma bpow_principle_constraints_forced_from_passive_active_roles with the same five role hypotheses (lepton passive role, up/EW sign opposition, EW positivity, EW magnitude $A$, and the four-sector sum). No new algebra is done here.
why it matters
Closes the boolean-filter side of the passive/active edge-role forcing for $B_{\mathrm{pow}}$ assignments inside the O1 yardstick choice-set enumeration. The module goal is that structural filters collapse the assignment pool to a singleton; this theorem shows the boolean filter is forced true once passive lepton role, EW magnitude $A$, and the sum target are assumed, without walking the finite enumeration.
It sits downstream of the principle-level forcing sibling and the yardstick assignment principle import. No further used-by edges are recorded yet, so it is a leaf in the current graph, but it is the form a decidable filter or #eval path would invoke. Framework contact is the mass yardstick on the $\varphi$-ladder (rung offsets and sector powers), not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.