bPowValuePool
plain-language theorem explainer
Four integer candidates for sector B_pow values, written from the cube-edge counts A, E_passive, and E_total. Anyone running the O1 yardstick choice-set enumeration cites this pool as the raw value set before permutation and filtering. The body is a pure definitional list of four closed forms; no proof work.
Claim. The candidate pool of $B_{\mathrm{pow}}$ values is the integer list $\bigl[-2 E_{\mathrm{passive}},\, -A,\, 2 E_{\mathrm{total}}-1,\, A\bigr]$, where $A$ is the active-edge count per tick, $E_{\mathrm{passive}}$ the passive-edge count, and $E_{\mathrm{total}}$ the total cube-edge count.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to sectors by permutation, then filtered by structural constraints. Valid choice sets collapse to singletons under those filters.
The integers here come from the $D=3$ cube topology used in the mass anchor. Total cube edges are $E_{\mathrm{total}}=12$; active edges per tick are $A=1$; passive edges are $E_{\mathrm{passive}}=11$. These are the same counts that appear in the anchor mass formulas and in the MassTopology layer for $Q_3$.
The four closed forms $-2E_{\mathrm{passive}}$, $-A$, $2E_{\mathrm{total}}-1$, and $A$ are exactly the sector $B_{\mathrm{pow}}$ expressions already fixed on the lepton, up-quark, down-quark, and electroweak sides of the anchor.
proof idea
Definitional list, not a proved statement. The four entries are the integer casts of $-2 E_{\mathrm{passive}}$, $-A$, $2 E_{\mathrm{total}}-1$, and $A$, in that order. No lemmas or tactics; the matching theorem later discharges equality to the named sector formulas by rfl.
why it matters
This pool is the raw value set for the O1 yardstick enumeration. Downstream, allBPowAssignments takes all permutations of the pool and filters them into sector assignments; bpow_pool_matches_anchor_formulas proves the list equals the four named sector $B_{\mathrm{pow}}$ formulas (lepton, up quark, down quark, electroweak) by reflexivity.
In the broader Recognition chain the edge counts sit on the $D=3$ cube forced at T8, with $A=1$ the active-edge-per-tick constant from the gap derivation. The combinatorial collapse of the choice set to a singleton is the verification content of O1: the yardstick assignment is not free once structural sum and sector constraints are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.