mode_budget_from_D3
plain-language theorem explainer
The vacuum mode budget equals two to the power of one more than the forced spatial dimension. With spatial dimension three this is sixteen, the combinatorial capacity used for the dark-energy fraction. Anyone deriving Ω_Λ from phase saturation of the D=3 ledger would cite this identity. The proof is pure definitional equality.
Claim. The total vacuum mode budget equals $2^{D_{\mathrm{phys}}+1}$, where $D_{\mathrm{phys}}=3$ is the forced spatial dimension, hence the budget is $2^{4}=16$.
background
This module derives the cosmological dark-energy fraction $\Omega_\Lambda=11/16-\alpha/\pi$ from phase saturation of the discrete ledger. At cosmic scale, matter excitations and vacuum modes equilibrate; the equilibrium vacuum fraction is identified with the passive mode fraction coming from $Q_3$ geometry.
Spatial dimension is forced to three by the Recognition Science chain (T8 / DimensionForcing). The mode budget is the total number of modes available to that D=3 ledger vacuum: defined as 16, read as $2^4$ from the three-cube doubled by double-entry bookkeeping. Active modes are five (three face-pair/generation modes plus two charge/parity modes); the remainder feeds the geometric seed 11/16.
Upstream, D_physical is the constant three, and several sibling D-constants in AlphaDerivation and GapDerivation likewise fix spatial dimension at three.
proof idea
One-line definitional proof. Unfolding both sides: the mode budget is the natural number 16, and the physical spatial dimension is 3, so the right-hand side is $2^{3+1}=16$. Lean closes by rfl.
why it matters
Anchors the combinatorial factor 16 that appears in $\Omega_\Lambda=11/16-\alpha/\pi$. Module status lists the mode budget, passive modes, and active modes as proved combinatorial infrastructure for the geometric seed equality (11/16 from mode counting). Framework landmark T8 forces $D=3$ spatial dimensions, which is exactly what makes the exponent $D+1$ equal four.
No downstream theorems yet depend on this identity (used_by is empty), but it is the D=3 pin for the counting that later bridges to cosmology. The open pieces remain the CosmicPhaseEquilibrium hypothesis and the vacuum-fraction bridge connecting ledger saturation to observed dark energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.