vertex_count_from_D3
plain-language theorem explainer
The ledger's vertex ground-state count equals 2^D with D the forced spatial dimension 3, hence equals 8. Cosmologists and RS mode-counters cite it when tying Q₃ passive modes to dimension forcing. The proof is pure definitional equality (rfl): both sides reduce to the numeral 8.
Claim. The number of vertex ground states equals $2^{D}$, where $D = 3$ is the spatial dimension fixed by dimension forcing. Explicitly, that count is $8$.
background
This module identifies the dark-energy fraction $\Omega_\Lambda$ with the equilibrium vacuum share of a discrete ledger under phase saturation, aiming at $\Omega_\Lambda = 11/16 - \alpha/\pi$ from $Q_3$ mode geometry.
vertex_ground_states is the constant $8$: the eight vertices of the 3-cube $Q_3$ that feed passive modes. D_physical is the RS spatial dimension, fixed at $3$ in Foundation.DimensionForcing (forcing-chain landmark T8). The identity $2^D = 8$ is the combinatorial bridge between that dimension and the vertex census used later in passive/active mode budgets.
Upstream, dimension forcing supplies $D = 3$ as a definitional constant; the local def simply hard-codes the matching vertex count.
proof idea
One-line definitional proof: rfl. The left side is the nat literal $8$; the right side is $2^{D_{\mathrm{physical}}}$ with $D_{\mathrm{physical}} := 3$, so both sides compute to $8$ and are definitionally equal. No lemmas are invoked.
why it matters
Pins the vertex census of $Q_3$ to the forced spatial dimension rather than an ad hoc count of 8. In the module chain, that census feeds passive-mode counting and the geometric seed $11/16$ behind $\Omega_\Lambda$. Framework landmark: T8 ($D = 3$). The graph lists no direct used_by edges yet; sibling material on $\Omega_\Lambda$ bounds and mode budgets is the intended landing zone. Does not itself close the still-open hypotheses CosmicPhaseEquilibrium or vacuum_fraction_bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.