r0_sum_target_eq_147
plain-language theorem explainer
The structural sum target for the four sector base rungs equals 147. Yardstick-assignment and O1 choice-set arguments cite this identity whenever they replace the symbolic target by a concrete integer. The proof is a one-line native evaluation of the closed formula V·W + E_passive.
Claim. The structural $r_0$ sum target equals $147$, where that target is $V\cdot W + E_{\mathrm{passive}}$ with $V$ the number of cube vertices in dimension $D$, $W$ the number of wallpaper groups, and $E_{\mathrm{passive}}$ the passive-field edge count in dimension $D$.
background
This module turns the O1 yardstick discussion into a finite combinatorial search: four candidate base-rung values are assigned to the four sectors (lepton, up, down, electroweak), filtered by structural constraints, and shown to collapse to a singleton.
The structural sum target is the integer $V\cdot W + E_{\mathrm{passive}}$ built from the alpha-derivation constants: cube vertices in dimension $D$, wallpaper-group count, and passive-field edges in dimension $D$. In the Recognition chain, $D=3$ is forced (T8), so the expression is a fixed integer. The theorem records that integer as 147, matching the parenthetical identity in the definition's doc-comment.
Downstream forcing lemmas treat the four sector rungs as an assignment whose sum must hit this target; equating the symbolic target to 147 is the first arithmetic step in those arguments.
proof idea
One-line wrapper: native_decide evaluates the closed integer expression defining the sum target and confirms it equals 147. No lemmas are invoked beyond the definition of the target itself.
why it matters
Closes the arithmetic gap between the geometric formula $V\cdot W + E_{\mathrm{passive}}$ and the concrete integer used in all subsequent $r_0$ forcing.
Three parents depend on it. The principle-match theorem rewrites the target as the sum of the four canonical sector rungs by first substituting 147. The unrestricted forcing theorem assumes the assignment sum equals the target and, with affine up/down roles and the lepton–EW depth gap fixed by the cube hierarchy, concludes the assignment is the canonical one. The depth-gap equivalence under affine roles and sum likewise opens by replacing the target with 147 before rearranging.
In the broader framework this is bookkeeping for the phi-ladder mass formula (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$): the base rungs must sum to a geometrically fixed integer before sector masses can be read off. It is pure verification arithmetic, not a new forcing step in T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.