mirroredBPow
plain-language theorem explainer
Defines the orientation-mirrored sector assignment of integer B-power exponents: lepton −2E_passive, up +A, down 2E_total−1, electroweak −A. It is the unique sign-dual of the canonical assignment under the same magnitudes. Downstream two-branch theorems cite it as the second admissible solution when EW orientation is free. The body is a pure structure literal from the anchor edge counts.
Claim. The mirrored $B_{\mathrm{pow}}$ assignment is the four-tuple of integer exponents $(\ell,u,d,w)=(-2E_{\mathrm{passive}},\,A,\,2E_{\mathrm{total}}-1,\,-A)$, i.e. the orientation reflection of the canonical assignment (same absolute values, opposite active-edge signs on the up and electroweak sectors).
background
The module enumerates yardstick $B_{\mathrm{pow}}$ assignments as a finite combinatorial choice set (O1 progress). A BPowAssignment is a four-sector integer record: lepton, up, down, and electroweak exponents. Structural filters (sum target, down-role, sign duality, active-unit magnitude) collapse the pool to a singleton once orientation is fixed.
Anchor constants supply the magnitudes: total cube edges $E_{\mathrm{total}}=12$, passive edges $E_{\mathrm{passive}}=11$, and active edges per tick $A=1$. The Recognition mass formula places sector masses on a $\varphi$-ladder whose rung offsets are these $B_{\mathrm{pow}}$ integers; the present definition only packages one admissible sign pattern.
Upstream, $A$ is the active-edge count per tick (also $\eta_B\Theta_{\mathrm{crit}}=\varphi^A$), while $E_{\mathrm{total}}$ and $E_{\mathrm{passive}}$ come from the $D=3$ cube edge inventory used throughout the mass-anchor layer.
proof idea
No proof: a definitional structure literal. It fills the four fields of BPowAssignment by casting the anchor naturals $E_{\mathrm{passive}}$, $A$, and $E_{\mathrm{total}}$ to $\mathbb{Z}$ and applying the mirrored sign pattern (negative lepton and electroweak, positive up, fixed down role $2E_{\mathrm{total}}-1$).
why it matters
Under down-role, sign-duality, active-unit magnitude, and the structural sum, the two-branch theorem states that every admissible assignment equals either the canonical package or this mirrored package. The orientation theorem then shows that requiring positive electroweak exponent selects the canonical branch and discards the mirror.
That collapse is the O1 claim of the module: the yardstick choice set is a singleton once orientation is fixed. In the broader Recognition chain the $B_{\mathrm{pow}}$ integers feed the $\varphi$-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and sit on the same edge-count geometry that forces $D=3$ and the eight-tick octave. The definition itself closes no open physics question; it names the second combinatorial witness the filters must rule out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.