bpow_unrestricted_forcing_from_down_role
plain-language theorem explainer
Fixing the down-sector entry of a four-sector integer B_pow assignment to the total-energy amplification 2E_total−1, together with the principle constraints, forces the assignment to equal the canonical B_pow. Cite this when uniqueness of the yardstick power map is needed from a single sector role rather than a full edge-role package. The proof reduces the down fixation to passive-edge lepton coupling and hands off to the passive-coupling forcing lemma.
Claim. Let $a$ be an integer assignment of $B_{\mathrm{pow}}$ values to the lepton, up, down, and electroweak sectors. If $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$ and $a$ satisfies the principle constraints (sign pattern, complementarity, up negativity, electroweak positivity, and structural sum), then $a$ equals the canonical $B_{\mathrm{pow}}$ assignment.
background
The module treats O1 yardstick uniqueness as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are assigned to the four sectors (lepton, up, down, electroweak), then filtered by structural and principle constraints until only the canonical assignment survives.
A BPowAssignment is simply a 4-tuple of integers, one per sector. Principle constraints package the sign pattern, complementarity, up-sector negativity, electroweak positivity, and the structural sum against a fixed target (equal to 1). The sum target and the numerical identities $2E_{\mathrm{total}}-1=23$ and $2E_{\mathrm{passive}}=22$ are decided constants in the RS-native integer arithmetic used for rung offsets on the $\varphi$-ladder mass formula.
The weaker input here is only the down-sector role $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$ (the total-energy amplification), not a full edge-role package. That is enough, once principle constraints hold, to recover the canonical map.
proof idea
Destructure the principle-constraint bundle into its five conjuncts. From the structural sum and the sign conjunct, obtain $a_{\mathrm{lepton}}+a_{\mathrm{down}}$ equal to the sum target via linear arithmetic. Specialize the down hypothesis with native_decide to get $a_{\mathrm{down}}=23$. The sum target equals 1, so $a_{\mathrm{lepton}}=-22$. Another native_decide rewrites $-22$ as $-(2E_{\mathrm{passive}})$, i.e. passive-edge lepton coupling. Finish by applying the already-proved unrestricted forcing lemma that takes passive lepton coupling plus the same principle constraints and concludes equality with the canonical assignment.
why it matters
This is the down-role half of the unrestricted (enumeration-free) canonical forcing path for $B_{\mathrm{pow}}$. Its sole downstream consumer is the edge-role forcing theorem, which assumes down fixation together with sign-duality, electroweak magnitude, and the structural sum, and concludes the same uniqueness without scanning the finite choice set.
In the broader RS picture the canonical $B_{\mathrm{pow}}$ feeds the yardstick that multiplies $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ in the mass formula. Collapsing the assignment choice set to a singleton under weaker role data is exactly the O1 progress the module advertises: structural-plus-principle constraints already pin the power map, so later mass and coupling derivations need not carry a residual discrete ambiguity.
It sits downstream of the forcing-chain landmarks only indirectly (the integer constants $E_{\mathrm{total}}$, $E_{\mathrm{passive}}$ ultimately trace to DOF and octave bookkeeping), but it is a concrete verification lemma rather than a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.