additive_corrections_sum_to_Ep
plain-language theorem explainer
The four sector additive offsets in the r₀ yardstick formulas sum exactly to the passive-edge count 11. Anyone auditing the Yardstick Assignment Principle (open problem O1) cites this as the edge-exhaustion constraint. The proof is a one-line integer arithmetic check.
Claim. The integer identity $(-6)+1+12+4=11$ holds, where the left-hand summands are the additive corrections $c$ in the four sector $r_0$ formulas and the right-hand side equals the passive edge count $E_{\mathrm{passive}}$.
background
The Yardstick Assignment Principle module treats open problem O1: why each particle sector receives a specific $B_{\mathrm{pow}}$ and $r_0$ formula from the counting layer. Sectors couple to distinct levels of the 3-cube hierarchy (lepton to passive edges, up/EW to the active edge, down to total edges).
The $r_0$ offsets are wallpaper-modulated: lepton $4W-6$, up $2W+A$, down $E-W$, electroweak $3W+4$, with wallpaper count $W=17$, cube edges $E=12$, and active edge $A=1$. Writing each as $m_i W+c_i$, the additive corrections are $c\in{-6,1,12,4}$.
Upstream, $E_{\mathrm{passive}}$ is the passive field-edge count $12-1=11$ (Anchor / MassTopology). A companion identity (W-multipliers sum to $V=8$) is proved separately among the module siblings.
proof idea
One-line arithmetic discharge: norm_num evaluates the pure integer equality $(-6)+1+12+4=11$ with no lemmas and no hypotheses.
why it matters
Feeds assignment_valid, which packages every Yardstick Assignment constraint; this theorem fills the edge_exhaustion field. Together with vertex exhaustion (W-multipliers sum to $V=8$), it yields the global count $\sum r_0=V\cdot W+E_{\mathrm{passive}}=8\cdot 17+11=147$. That identity is the structural check that sector offsets exhaust the cube's passive edges rather than being free parameters. It closes one counting half of open problem O1 (sector-to-cube coupling) and sits on the 3-cube combinatorics underlying T7/T8 (eight vertices, twelve edges).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.