anchor_bpow_matches_canonical
plain-language theorem explainer
The sector-wise B_pow assignment taken from the mass-ladder anchor formulas equals the canonical combinatorial assignment used in the O1 choice-set search. Anyone citing uniqueness of the valid B_pow yardstick assignment needs this identification. The proof is a one-line native_decide on concrete integer field equality.
Claim. The anchor $B_{\mathrm{pow}}$ assignment (lepton, up, down, electroweak values read from the sector anchor formulas) equals the canonical assignment $(-2E_{\mathrm{passive}},\,-A,\,2E_{\mathrm{total}}-1,\,A)$.
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 the four sectors (lepton, up quark, down quark, electroweak) by permutation, then filtered by structural and principle constraints. Valid choice sets collapse to singletons under those filters.
A $B_{\mathrm{pow}}$ assignment is a four-tuple of integers, one per sector. The canonical assignment is the fixed record $(-2E_{\mathrm{passive}},,-A,,2E_{\mathrm{total}}-1,,A)$. The anchor assignment instead reads each sector from the existing $B_{\mathrm{pow}}$ formulas in the mass-anchor layer (lepton, up quark, down quark, electroweak). The mass formula itself is yardstick times $\varphi$ to a rung offset, so these integers are the discrete exponents that set sector yardsticks.
proof idea
One-line wrapper: both sides are closed integer records (no free variables), so propositional equality is decidable. native_decide evaluates the four field equalities and closes the goal. No intermediate lemmas are invoked beyond the two definitions being compared.
why it matters
Parent use is anchor_is_unique_valid_bpow, which rewrites the valid-$B_{\mathrm{pow}}$ set as the singleton of the canonical assignment and substitutes this equality to place the anchor inside that set. Together they discharge the O1 claim that structural filters leave a unique $B_{\mathrm{pow}}$ choice set, matching the physical anchor rather than a mirrored or permuted alternative.
In the broader Recognition chain this pins the discrete exponents that enter the phi-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). It is verification scaffolding for uniqueness of sector yardsticks, not a new forcing step (T5–T8 already fix $J$, $\varphi$, the eight-tick octave, and $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.