r0SumTarget
plain-language theorem explainer
Integer sum target for the four sector base rungs r0: V·W + E_passive, equal to 147 at D=3. Yardstick choice-set filters and principle-constraint lemmas cite it as the fixed total. Defined by casting cube vertices, wallpaper groups, and passive field edges to integers and combining them.
Claim. The structural sum target for the four sector base rungs is the integer $V\cdot W+E_{\mathrm{passive}}$, where $V=2^{D}$ is the number of vertices of the $D$-cube, $W=17$ is the number of 2D wallpaper groups, and $E_{\mathrm{passive}}$ is the number of passive field edges on that cube. For the forced spatial dimension $D=3$ one has $8\cdot 17+11=147$.
background
This module turns the O1 yardstick discussion into 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 until only singleton choice sets remain.
The building blocks come from the alpha-derivation constants. Spatial dimension is fixed at $D=3$ (linking forces three space dimensions). Cube vertices are $V=2^{D}$, so eight for $D=3$. Wallpaper groups are the classical crystallographic count $W=17$ (Fedorov 1891). Passive field edges are total cube edges minus the single active edge per tick; the upstream note records that this equals 11 when $D=3$.
Those three naturals are cast to $\mathbb{Z}$ and combined into one integer that every $r_0$ assignment is required to sum to.
proof idea
Pure definition, not a proved equality. The body is the integer expression
$(V(D):\mathbb{Z})\cdot(W:\mathbb{Z})+(E_{\mathrm{passive}}(D):\mathbb{Z})$
with $V$, $W$, and $E_{\mathrm{passive}}$ taken from Constants.AlphaDerivation at the fixed $D=3$. No tactics or lemmas; the arithmetic $8\cdot 17+11=147$ is left implicit in the closed form.
why it matters
Every structural and principle filter on $r_0$ assignments uses this constant as the required four-sector sum. Downstream, r0PrincipleConstraints packages the ordering inequalities together with equality of the sector sum to this target; anchor_r0_structural_identities and anchor_r0_constraints_from_principle verify that the anchor assignment meets it; and the forcing lemmas (r0_bool_constraints_forced_from_affine_roles_and_sum, r0_principle_iff_sum_under_affine_roles_and_depth_gap, r0_depth_gap_iff_ew_role_under_affine_roles_and_sum) treat the sum as the last free constraint that collapses affine role data to a unique assignment.
In the broader Recognition chain this sits inside verification of the mass yardstick (phi-ladder rungs), not inside T0–T8 forcing itself. It packages the geometric ingredients already fixed by $D=3$ and the wallpaper count into the single integer the O1 choice-set enumeration needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.