bpowPrincipleConstraints
plain-language theorem explainer
Principle-level constraints on a four-sector integer B_pow assignment: up equals minus electroweak, absolute lepton plus absolute EW equals down, up negative, EW positive, and the four values sum to the structural target A. Downstream forcing theorems cite this Prop as the filter that collapses the enumerated choice set to the canonical assignment. It is the Prop form of the boolean structural predicate, written as a five-conjunct definition.
Claim. For an integer assignment $a$ of $B_{\mathrm{pow}}$ values to the lepton, up, down, and electroweak sectors, the principle constraints hold when $a_{\mathrm{up}}=-a_{\mathrm{ew}}$, $|a_{\ell}|+|a_{\mathrm{ew}}|=a_{\mathrm{down}}$, $a_{\mathrm{up}}<0$, $a_{\mathrm{ew}}>0$, and $a_{\ell}+a_{\mathrm{up}}+a_{\mathrm{down}}+a_{\mathrm{ew}}=A$, where $A$ is the structural sum target.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are assigned to the four sectors (lepton, up, down, electroweak) by enumerating permutations, then filtering by structural constraints. Valid choice sets collapse to singletons under those filters.
A BPowAssignment is simply a 4-tuple of integers $(a_\ell, a_{\mathrm{up}}, a_{\mathrm{down}}, a_{\mathrm{ew}})$. The sum target bpowSumTarget is the integer cast of the structural constant $A$ (documented as $A=1$). Upstream cosmology species labels for up and down quarks supply DOF context for the sector names but are not used in the Prop body itself.
The companion boolean predicate bpowStructuralConstraints is the executable filter used in enumeration; this definition is its Prop-level twin for theorem statements.
proof idea
Pure definition: five conjuncts on the four integer fields. Sign duality $a_{\mathrm{up}}=-a_{\mathrm{ew}}$; absolute-value balance $|a_\ell|+|a_{\mathrm{ew}}|=a_{\mathrm{down}}$; orientation $a_{\mathrm{up}}<0$ and $a_{\mathrm{ew}}>0$; and the structural sum equal to bpowSumTarget. No lemmas are applied. The equivalence theorem bpow_constraints_true_iff later unfolds both predicates and closes by simp and tauto.
why it matters
This Prop is the mathematical filter that the O1 yardstick forcing chain actually reasons about. Downstream, bpow_constraints_force_canonical shows every enumerated assignment satisfying it equals the canonical $B_{\mathrm{pow}}$ tuple. Role-based theorems derive the full conjunction from edge-role hypotheses (down role, sign duality, active-edge unit magnitude, structural sum), and equivalence forms reduce it to the single magnitude condition $|a_{\mathrm{ew}}|=A$ once roles and sum are fixed.
In the Recognition framework this sits in the verification layer that pins the mass-yardstick sector powers before the phi-ladder mass formula is applied. It does not itself invoke T5–T8 or the RCL; it only certifies which discrete $B_{\mathrm{pow}}$ assignment survives the structural sieve used in the paper’s O1 discussion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.