depths_exhaust_vertices
plain-language theorem explainer
The four sector depths on the wallpaper lattice (leptons 4, up quarks 2, down quarks −1, electroweak 3) sum to the 3-cube vertex count V = 8. Anyone auditing the yardstick assignment principle cites this as the vertex-exhaustion constraint. The proof is a one-line native decision of the integer equality 4+2+(−1)+3 = 2^3.
Claim. With spatial dimension $D = 3$, the sector depths satisfy $4 + 2 + (-1) + 3 = 2^D$. Equivalently, the W-multipliers in the $r_0$ formulas exhaust the vertices of the 3-cube: their sum equals $V = 8$.
background
Open Problem O1 asks why each particle sector receives its specific $B_{\mathrm{pow}}$ and $r_0$ yardstick formulas from the counting layer. The module's answer is a sector-to-cube coupling: each sector attaches to a distinct level of the 3-cube hierarchy, and the formulas encode that attachment.
The $r_0$ offsets are wallpaper-modulated: $r_0(\mathrm{Lepton}) = 4W-6$, $r_0(\mathrm{Up}) = 2W+A$, $r_0(\mathrm{Down}) = E-W$, $r_0(\mathrm{EW}) = 3W+4$, with $W = 17$. The integer multipliers of $W$ are the sector depths ${4, 2, -1, 3}$.
Upstream, $D := 3$ is the spatial dimension forced by the forcing chain (T8), and $\mathrm{cube_vertices}(D) := 2^D$ is the vertex count of the $D$-hypercube. For $D = 3$ one has $V = 8$, matching the eight-tick octave.
proof idea
Pure arithmetic discharge. After unfolding $D = 3$ and $\mathrm{cube_vertices}, D = 2^3$, the goal is the integer identity $4 + 2 + (-1) + 3 = 8$. The tactic native_decide evaluates both sides and closes the equality; no lemmas are invoked.
why it matters
This is one of the four structural constraints packaged into assignment_valid, which asserts that the current sector-to-yardstick map satisfies sign duality, lepton/EW complement to down, vertex exhaustion, and edge exhaustion. Downstream, vertex exhaustion is exactly the field filled by this theorem.
In the Recognition framework it ties the $r_0$ W-multipliers to the 3-cube geometry forced by T8 ($D = 3$) and to the eight-tick octave ($V = 2^3 = 8$). The module frames O1 as: the depths are not free parameters but a partition of the cube's vertices. Closing this equality is a necessary check that the wallpaper-modulated offsets are combinatorially complete rather than ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.