cube_partition_budget
plain-language theorem explainer
At spatial dimension three, hypercube vertices, the atomic active edge, passive edges, and faces sum to a fixed combinatorial ledger of 26. Anyone working the yardstick assignment principle (Open Problem O1) cites this as the partition identity that ties particle sectors to cube hierarchy levels. The proof is a one-line native decision on the concrete integer constants.
Claim. For spatial dimension $D=3$, the sum of hypercube vertices $2^{D}$, the atomic active-edge count $A$, the passive-edge count $E_{\mathrm{passive}}$, and hypercube faces $2D$ equals $26$ as integers.
background
The Yardstick Assignment Principle module asks why each particle sector receives its specific $B_{\mathrm{pow}}$ and $r_0$ formulas from the counting layer. The organizing idea is sector-to-cube coupling: leptons, up quarks, down quarks, and the electroweak sector each attach to a distinct level of the 3-cube hierarchy (passive edges, active edge, total edges, faces/vertices).
Here $D=3$ is the spatial dimension forced by the Recognition chain. Hypercube vertices are $2^{D}=8$ and faces are $2D=6$. The atomic active-edge count is $A=1$; passive edges are $E_{\mathrm{passive}}=11$ (total edges $E=12$ minus the active edge). These four integers are the combinatorial sectors that the assignment ledger must exhaust.
Upstream definitions fix the geometry: cube_vertices and cube_faces are the standard $D$-cube counts, and $D$ is pinned at three. The module constraints (C1)–(C5) further require that $B_{\mathrm{pow}}$ combinations and $r_0$ wallpaper multipliers respect vertex exhaustion $V=8$ and passive-edge exhaustion $E_p=11$.
proof idea
Term-mode proof by native_decide. After unfolding $D=3$, vertices $2^3=8$, faces $2\cdot 3=6$, and the fixed integers $A=1$, $E_{\mathrm{passive}}=11$, the equality $8+1+11+6=26$ is a closed integer computation with no lemmas or case splits.
why it matters
This identity is the global budget check for Open Problem O1: sector formulas are not free parameters but allocations inside one 26-unit cube ledger. It anchors the module claim that vertex, atomic, passive-edge, and face sectors together exhaust the combinatorial resource that $B_{\mathrm{pow}}$ and $r_0$ draw from.
Framework landmarks: $D=3$ is the T8 spatial-dimension forcing; the eight vertices match the eight-tick octave (T7 Gray cycle on the 3-cube). The split $E=12=A+E_{\mathrm{passive}}$ with $A=1$, $E_p=11$ is exactly the edge accounting used in the lepton/EW/quark $B_{\mathrm{pow}}$ pairs ($|{-}22|+|1|=23$, etc.).
No downstream theorems currently depend on it (used_by is empty); it stands as a verified ledger fact that any future uniqueness proof of the four-sector assignment can invoke when closing the O1 constraint system (C1)–(C5) plus distinct yardsticks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.