r0_sum_target_matches_principle
plain-language theorem explainer
The geometric r₀ sum target V·W + E_passive equals the sum of the four sector φ-exponent offsets (lepton, up, down, electroweak). Anyone checking O1 yardstick filters or the anchor r₀ assignment cites this identity. The proof is a two-step calc that routes both sides through the integer 147.
Claim. The structural sum target $V\cdot W + E_{\mathrm{passive}}$ equals $r_0(\mathrm{Lepton}) + r_0(\mathrm{UpQuark}) + r_0(\mathrm{DownQuark}) + r_0(\mathrm{Electroweak})$, where each $r_0$ is the derived $\varphi$-exponent offset of that sector.
background
This module turns the O1 yardstick discussion into a finite combinatorial search: assign four candidate $r_0$ values to the four sectors, then filter by structural constraints until only the anchor survives.
Each sector carries a derived $\varphi$-exponent offset $r_0$ from wallpaper-plus-cube geometry (lepton $4W-6=62$, up $2W+A=35$, down $E_{\mathrm{total}}-W=-5$, electroweak $3W+4=55$). Independently, the structural sum target is defined as $V\cdot W + E_{\mathrm{passive}}$ (cube vertices times wallpaper groups, plus passive field edges), which evaluates to 147.
Upstream, YardstickAssignmentPrinciple.r0_sum already proves the four sector offsets sum to 147, and a native-decide lemma shows the geometric target equals 147. This declaration equates the two presentations.
proof idea
Two-step calc. First rewrite the geometric target to 147 via r0_sum_target_eq_147 (native decide on the constants). Then identify 147 with the four-sector sum by symmetry of YardstickAssignmentPrinciple.r0_sum, which expands each sector formula and closes by norm_num.
why it matters
Feeds anchor_r0_structural_identities, whose last conjunct asserts that the anchor assignment sums exactly to the structural target. That filter is part of the O1 choice-set collapse: under ordering and sum constraints the enumerated $r_0$ assignments reduce to a singleton matching the geometric anchor.
In the broader RS picture the $r_0$ offsets sit on the $\varphi$-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Matching their sum to $V\cdot W + E_{\mathrm{passive}}$ ties sector exponents to the same cube/wallpaper counting that forces $D=3$ and the eight-tick structure elsewhere in the forcing chain. Without this bridge the combinatorial filter would compare against an unlinked integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.