bpow_constraints_true_iff
plain-language theorem explainer
Boolean structural filters on four-sector B_pow assignments are equivalent to the corresponding Prop-level principle constraints. Anyone checking the O1 yardstick choice-set enumeration cites this bridge when moving between decidable filters and proof hypotheses. The proof unfolds both definitions and closes by simplification plus tautology.
Claim. For every assignment $a$ of integers $(B_{\ell}, B_{u}, B_{d}, B_{\mathrm{ew}})$ to the lepton, up, down, and electroweak sectors, the boolean structural filter on $a$ evaluates to true if and only if the principle constraints hold: $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}}$ equals the fixed sum target.
background
The module treats O1 yardstick assignment as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are permuted across sectors, then filtered by structural constraints. Valid choice sets collapse to singletons under those filters.
A BPowAssignment is a 4-tuple of integers, one per sector (lepton, up, down, electroweak). The boolean filter bpowStructuralConstraints decides five conditions: opposite signs of up and electroweak powers, absolute-value balance of lepton and electroweak against down, strict negativity of up, strict positivity of electroweak, and exact sum equal to the module's sum target. The principle form is the same conjunction written as a Prop rather than a Bool, so it can appear as a hypothesis in ordinary proofs.
proof idea
Term-mode proof by definitional identity. Unfold the boolean filter and the Prop-level principle constraints; both expand to the same five atomic conditions (sign opposition, absolute-value balance, two strict inequalities, and the sum target). simp reduces the boolean decide wrappers and conjunctions; tauto closes the resulting propositional equivalence. No external lemmas are required.
why it matters
This equivalence is the bridge between the decidable enumeration filter and the Prop hypotheses used in uniqueness arguments. Downstream, bpow_constraints_force_canonical converts a principle hypothesis into a true boolean filter membership, then concludes the assignment equals the canonical $B_{\mathrm{pow}}$ tuple. Related parents give boolean-filter forms of edge-role and passive/active-role forcing, and equivalences that pin the electroweak magnitude to the active unit $A$ under down or passive-down roles.
In the broader Recognition picture this sits inside yardstick verification for the mass ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). It does not itself invoke T5--T8 or the RCL; it only certifies that the combinatorial filter used in O1 matches the principle statement those later uniqueness proofs assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.