Pith. sign in
theorem

W_multipliers_sum_to_V

proved
show as:
module
IndisputableMonolith.Verification.YardstickAssignmentPrinciple
domain
Verification
line
164 · github
papers citing
none yet

plain-language theorem explainer

The four sector multipliers on the wallpaper count W in the r₀ offsets sum to V = 8. Anyone checking the Yardstick Assignment Principle (O1) cites this as the integer closure of those multipliers on the eight-tick volume. The proof is a one-line norm_num arithmetic identity on ℤ.

Claim. The W-multipliers appearing in the four sector $r_0$ formulas satisfy $4 + 2 + (-1) + 3 = 8$, where $8$ is the eight-tick volume $V$.

background

The Yardstick Assignment Principle (open problem O1) asks why each particle sector receives a definite $B_{\mathrm{pow}}$ and $r_0$ formula from the counting layer of the 3-cube. Sectors couple to distinct levels of that hierarchy: leptons to passive edges, up quarks and electroweak to the active edge, down quarks to total edges.

The $r_0$ offsets are wallpaper-modulated linear forms in $W = 17$ (the number of wallpaper groups): $r_0(\mathrm{lepton}) = 4W - 6$, $r_0(\mathrm{up}) = 2W + A$, $r_0(\mathrm{down}) = E - W$, $r_0(\mathrm{EW}) = 3W + 4$. The integer coefficients of $W$ are therefore ${4, 2, -1, 3}$ (writing $E - W$ as $-W + E$).

Upstream, $E_{\mathrm{passive}} = 11$ is the passive-edge count $12 - 1$ on $Q_3$; it appears in the companion additive-correction identity, not in this multiplier sum. Here $V = 8$ is the combinatorial volume tied to the eight-tick octave.

proof idea

Pure closed arithmetic on $\mathbb{Z}$. The tactic norm_num evaluates $4 + 2 + (-1) + 3$ and checks equality with $8$. No lemmas about anchors, masses, or topology are invoked; the depends-on edges to $E_{\mathrm{passive}}$ are ambient module context, not proof ingredients.

why it matters

Inside the O1 module this is the structural checksum that the four $r_0$ multipliers close on $V = 8$. That volume is the Recognition landmark T7 (eight-tick octave, period $2^3$), so the identity ties sector yardstick offsets to the same discrete clock that forces $D = 3$ at T8.

No downstream theorems currently consume it (used-by is empty); it stands as a verified bookkeeping fact supporting the table of sector formulas and the claim that the W-multipliers are not arbitrary. Together with the sibling sum of additive corrections to $E_{\mathrm{passive}} = 11$, it completes the integer audit of $r_0 = m W + c$ across the four sectors.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.