bpow_principle_iff_active_unit_under_down_role
plain-language theorem explainer
Under fixed down-role, up/EW sign duality, structural sum, and positive EW orientation, full B_pow principle constraints on a four-sector integer assignment are equivalent to the electroweak magnitude equaling the active-edge unit A (=1). O1 yardstick verification cites this to collapse the combinatorial assignment search. One direction forces lepton and down to concrete integers then uses linear arithmetic; the converse is a forcing lemma.
Claim. Let $a$ assign integers $B_{\mathrm{pow}}$ to the lepton, up, down, and electroweak sectors. Assume the down role $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$, sign duality $a_{\mathrm{up}}=-a_{\mathrm{ew}}$, the structural sum $a_{\mathrm{lepton}}+a_{\mathrm{up}}+a_{\mathrm{down}}+a_{\mathrm{ew}}$ equals the B_pow sum target, and $a_{\mathrm{ew}}>0$. Then $a$ satisfies the full $B_{\mathrm{pow}}$ principle constraints if and only if $|a_{\mathrm{ew}}|=A$, where $A=1$ is the active-edge count per tick.
background
The module treats O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are assigned to the four sectors (lepton, up, down, electroweak), all permutations are enumerated, and structural filters are applied. Valid choice sets collapse to singletons under those constraints.
A BPowAssignment is simply four integers, one per sector. The constant $A$ is the active-edge count per tick, fixed at $1$ in the gap derivation. Downstream mass and yardstick formulas use $E_{\mathrm{passive}}$ and $E_{\mathrm{total}}$ as fixed integer energy anchors; the down-role hypothesis pins the down sector to $2E_{\mathrm{total}}-1$, while the lepton sector is forced (via an upstream lemma) to $-2E_{\mathrm{passive}}$ once sign duality and the structural sum are in place.
Principle constraints package the full yardstick $B_{\mathrm{pow}}$ package (sign pattern, complementarity, orientation, and sum). The claim isolates the single remaining free magnitude: the electroweak absolute value.
proof idea
Bidirectional constructor.
Forward: unpack principle constraints to obtain complementarity. Apply bpow_lepton_forced_from_down_role_and_sign_sum to get $a_{\mathrm{lepton}}=-(2E_{\mathrm{passive}})$, then native_decide evaluates that to $-22$. The down hypothesis similarly evaluates to $23$. Absolute values $|a_{\mathrm{lepton}}|=22$ and the complementarity relation feed nlinarith, yielding $|a_{\mathrm{ew}}|=1$. Since $A=1$ by definition, this is $|a_{\mathrm{ew}}|=A$.
Converse: one-line application of bpow_principle_constraints_forced_from_edge_roles, which rebuilds the full principle package from the down role, sign duality, positive EW orientation, the unit-magnitude hypothesis, and the structural sum.
why it matters
This is a key reduction step in the O1 yardstick choice-set enumeration: once down-role, sign duality, sum, and EW orientation are fixed, the entire principle package collapses to the single arithmetic condition $|a_{\mathrm{ew}}|=A$. That matches the framework landmark that the active-edge count per tick is $A=1$.
Two immediate parents consume it. bpow_bool_constraints_iff_active_unit_under_down_role rewrites the same equivalence in Boolean-filter form for the enumeration pipeline. bpow_principle_iff_active_unit_under_passive_down_roles weakens the hypotheses by taking the passive lepton role as given and deriving the sign internally. Together they justify why the filtered assignment lists collapse to singletons for $B_{\mathrm{pow}}$, closing the combinatorial half of the yardstick uniqueness argument that feeds the mass ladder (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.