anchor_bpow_constraints_from_principle
plain-language theorem explainer
The anchor sector-to-B_pow assignment passes every structural Boolean filter in the yardstick choice-set enumeration. Anyone verifying that the O1 search collapses B_pow assignments to a singleton cites this certificate. The proof unpacks proved sign, ordering, complementarity, and sum identities for the anchor values and rewrites them into the decide-form of the filter.
Claim. The canonical anchor assignment of $B_{\mathrm{pow}}$ values to the lepton, up, down, and electroweak sectors satisfies all structural constraints: $|B_{\ell}|+|B_{\mathrm{ew}}|=B_{\mathrm{down}}$, the mirror relation $B_{\mathrm{up}}=-B_{\mathrm{ew}}$, the ordering $B_{\mathrm{up}}<0<B_{\mathrm{ew}}$, and $B_{\ell}+B_{\mathrm{up}}+B_{\mathrm{down}}+B_{\mathrm{ew}}$ equal to the fixed $B_{\mathrm{pow}}$ sum target.
background
The module treats the O1 yardstick discussion as a finite combinatorial search. Four candidate $B_{\mathrm{pow}}$ values are assigned to four sectors (lepton, up, down, electroweak) by enumerating permutations, then filtering by structural constraints already forced in the Yardstick Assignment Principle.
Those constraints are a Boolean package on a four-tuple: absolute-value complementarity of lepton and electroweak with the down sector, the mirror identity $B_{\mathrm{up}}=-B_{\mathrm{ew}}$, the sign conditions $B_{\mathrm{up}}<0$ and $B_{\mathrm{ew}}>0$, and a four-sector sum equal to a fixed target (a sibling proves the target is one in native units). The anchor assignment is the distinguished tuple coming from the mass-ladder formulas.
Upstream, the packed lemma of structural identities for the anchor supplies the raw equalities and inequalities; the principle-level lepton-electroweak complementarity identity supplies the absolute-value clause after specialization to the anchor tuple.
proof idea
Destructure the packed anchor structural identities into sign, complementarity, up-negative, ew-positive, and sum facts (the raw complementarity conjunct is discarded). Rebuild the absolute-value complementarity clause by simplifying the principle lemma on lepton-electroweak complementarity against the concrete anchor assignment. Convert each Prop-level fact into a decide ... = true certificate via decide_eq_true. Unfold the Boolean structural-constraint predicate and discharge all conjuncts by simplification against those certificates.
why it matters
This is the positive half of the O1 B_pow uniqueness argument inside the verification layer: the enumeration keeps only assignments that return true under the structural filter, and the anchor is shown to survive. Together with the parallel pool and sum-target lemmas, it supports the module claim that valid B_pow choice sets collapse to a singleton under the stated constraints.
No downstream declaration currently depends on it, so it is a leaf certificate in the yardstick pipeline rather than a step in the T0-T8 forcing chain. It closes the structural side of the B_pow filter before the analogous r0 filter is applied. The mass-ladder yardstick (rung shifts by powers of $\varphi$) is the broader RS context, but this lemma only certifies the discrete assignment filter, not the continuum mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.