bpow_principle_constraints_forced_from_edge_roles
plain-language theorem explainer
Edge-role hypotheses on a four-sector integer assignment force the full B_pow principle constraint bundle. Yardstick-verification arguments cite this to replace enumeration filters by role axioms. The proof recovers the lepton coordinate from the down-role and sum, evaluates anchor constants by native decision, and assembles the five principle fields.
Claim. Let $a$ assign integers to the lepton, up, down, and electroweak sectors. If $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$, $a_{\mathrm{up}}=-a_{\mathrm{ew}}$, $a_{\mathrm{ew}}>0$ with $|a_{\mathrm{ew}}|=A$ (active-edge count), and the four coordinates sum to the B_pow sum target, then $a$ satisfies the full B_pow principle constraints: sign duality, absolute-value composition $|a_{\mathrm{lepton}}|+|a_{\mathrm{ew}}|=a_{\mathrm{down}}$, up negativity, electroweak positivity, and the structural sum.
background
The module treats O1 yardstick discussion as a finite combinatorial search: four candidate B_pow values and four r0 values are assigned to sectors by permutation, then filtered by structural constraints until valid choice sets collapse to singletons.
A B_pow assignment is a 4-tuple of integers (lepton, up, down, electroweak). Anchor data fix the active-edge count $A=1$ and the passive/total edge energies $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$ (here evaluating so that $2E_{\mathrm{total}}-1=23$ and $2E_{\mathrm{passive}}=22$). The sum target is the structural total required of any admissible assignment.
Edge roles encode sector identities used upstream: the down role sets down $=2E_{\mathrm{total}}-1$; sign duality pairs up with $-$electroweak; active-edge unit magnitude requires $|\mathrm{ew}|=A$ with positive orientation.
proof idea
Apply the forcing lemma that recovers the lepton coordinate from the down-role hypothesis, sign duality, and structural sum, giving lepton $=-(2E_{\mathrm{passive}})$. Native decision evaluates the anchors: down becomes $23$ and lepton becomes $-22$. With $A=1$ and positivity, the magnitude hypothesis forces electroweak $=1$, hence up $=-1$ by sign duality and nlinarith. Absolute-value composition $|\mathrm{lepton}|+|\mathrm{ew}|=\mathrm{down}$ is checked by simplification on these values. The five principle fields (sign, composition, up negativity, electroweak positivity, sum) are then packaged as the principle-constraint structure.
why it matters
Core forcing step that turns edge-role axioms into the full principle-constraint predicate used by the yardstick verification layer. Downstream it feeds the boolean-filter variant, the passive-active role twin, the equivalence of principle constraints with active-unit magnitude under down-role, unrestricted canonical forcing without enumeration, and the cube-partition packaging that forces the full admissibility filter family for both B_pow and r0.
In the Recognition mass ladder the yardstick fixes the sector-dependent base of the $\varphi$-power mass formula. Collapsing the choice set under role axioms is the module's O1 claim: the combinatorial search is not merely filtered but forced by edge geometry (active edges per tick $A=1$, passive/total edge counts).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.