anchor_bpow_structural_identities
plain-language theorem explainer
The anchor sector-to-B_pow assignment satisfies the five structural filter identities of the yardstick choice-set: up equals minus electroweak, absolute-value complementarity of lepton and electroweak with down, the two sign constraints, and the four-sector sum target. Anyone verifying that the canonical anchor survives the B_pow filter cites this. The proof is a five-way refine that unpacks the anchor definition and applies the matching identities from the yardstick assignment principle.
Claim. For the anchor $B_{\mathrm{pow}}$ assignment to the lepton, up, down, and electroweak sectors: $B_{\mathrm{up}}=-B_{\mathrm{ew}}$, $|\ell|+|B_{\mathrm{ew}}|=B_{\mathrm{down}}$ (as integers), $B_{\mathrm{up}}<0$, $B_{\mathrm{ew}}>0$, and $\ell+B_{\mathrm{up}}+B_{\mathrm{down}}+B_{\mathrm{ew}}$ equals the $B_{\mathrm{pow}}$ sum target.
background
This module turns the O1 yardstick discussion into a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to sectors by all permutations, 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 integer exponents, one per sector (lepton, up, down, electroweak). The anchor assignment is the distinguished tuple used in the mass-yardstick formulas. The structural filter demands opposite signs for up and electroweak, absolute-value complementarity of lepton and electroweak against down, strict sign inequalities, and a fixed four-sector sum equal to a named target (proved equal to one in a sibling lemma).
Those identities are already established abstractly in the yardstick assignment principle module; this theorem only specializes them to the concrete anchor tuple.
proof idea
Term-mode five-way refine on the conjunction. Each goal is discharged by simp or simpa after unfolding the anchor assignment:
- sign equality $B_{\mathrm{up}}=-B_{\mathrm{ew}}$ by direct simplification;
- absolute-value complementarity by the principle lemma that lepton and electroweak natAbs sum to down;
- the two strict inequalities by the two projections of the principle lemma that up is negative and electroweak is positive;
- the sum identity by the sibling that the sum target matches the principle, rewritten with
add_comm/add_assoc/add_left_comm.
why it matters
Immediate parent is anchor_bpow_constraints_from_principle, which packages these five identities into the Boolean structural-constraint predicate evaluating to true on the anchor. That step is the bridge from abstract principle lemmas to the concrete filter used in the choice-set enumeration.
In the broader Recognition picture the yardstick $B_{\mathrm{pow}}$ exponents sit on the phi-ladder mass formula (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Showing the anchor is the unique survivor of the structural filter is O1 progress toward forcing the sector exponents rather than fitting them. The module doc states the valid sets collapse to singletons; this theorem is the anchor half of that collapse for $B_{\mathrm{pow}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.