mode_budget_partition
plain-language theorem explainer
The D=3 ledger vacuum has total mode budget 16, which splits exactly into 5 active (matter) modes and 11 passive (vacuum) modes. Cosmologists deriving Ω_Λ from phase saturation cite this as the combinatorial partition behind the geometric seed 11/16. The proof is a one-line native decision on the three natural-number constants.
Claim. The total mode budget of the $D=3$ ledger vacuum equals the sum of active and passive modes: $5 + 11 = 16$.
background
This module identifies the cosmological dark-energy fraction $\Omega_\Lambda$ with the equilibrium vacuum share of a discrete ledger under phase saturation. The geometric seed is the passive-mode fraction $11/16$, later corrected by $\alpha/\pi$ to give $\Omega_\Lambda = 11/16 - \alpha/\pi$.
Three natural-number constants fix the counting. The total mode budget is $16 = 2^4$, from the $D=3$ cube doubled by double-entry bookkeeping (linked to the eight-tick octave and T8 forcing of three spatial dimensions). Active modes are the five matter excitations that participate in recognition: three face-pair/generation modes plus two charge/parity modes. Passive modes are the eleven vacuum modes: eight vertex ground states plus three unexcited face-pair contributions.
The partition statement simply asserts that these three constants add: active plus passive equals the budget.
proof idea
One-line native_decide on the three ℕ definitions active_modes := 5, passive_modes := 11, and mode_budget := 16. No lemmas are invoked; Lean reduces the ground equality $5+11=16$ by computation.
why it matters
Feeds directly into phase_saturation_vacuum_cert, which packages the Ω_Λ positivity, upper bounds, mode partition, and closure facts for the phase-saturation vacuum story. The module chain treats this combinatorial split as the source of the geometric seed $11/16$ (passive fraction), which is then adjusted by the fine-structure term $\alpha/\pi$ to match the observed dark-energy density.
Within Recognition Science the count sits on the D=3 / eight-tick side of the forcing chain (T7–T8): the $2^4$ budget is the doubled cube of three spatial dimensions. Downstream hypotheses (CosmicPhaseEquilibrium, vacuum_fraction_bridge) still connect ledger saturation at $\varphi^{45}$ to cosmology; this theorem closes only the pure mode-arithmetic step those bridges rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.