passive_modes
plain-language theorem explainer
Passive modes are the vacuum sector of the discrete ledger mode budget: eleven modes, counted as eight vertex ground states of the 3-cube plus three unexcited face-pair contributions. Anyone deriving the RS dark-energy fraction cites this integer as the numerator of the geometric seed 11/16. The declaration is a bare natural-number definition; the combinatorial split is recorded in a sibling native_decide theorem.
Claim. The number of passive (vacuum) modes equals $11$, identified as $8$ vertex ground states plus $3$ unexcited face-pair contributions on the $Q_3$ geometry.
background
The 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$ cube geometry.
Passive modes are the vacuum modes in that counting. The total mode budget is $2^{D+1} = 16$ once spatial dimension is forced to $D = 3$ (T8 in the forcing chain; the eight-tick octave is T7). The companion active-mode count is five, so active plus passive exhausts the budget of sixteen.
The local combinatorial claim is that the eleven passive modes split as eight vertex ground states ($2^D = 8$) plus three unexcited face-pair contributions. That split is stated separately; this declaration only fixes the integer.
proof idea
One-line definition: the natural number is set equal to 11. No tactics, no lemmas. The justifying decomposition (vertex ground states plus unexcited face modes) lives in the sibling theorem proved by native_decide; the partition against the full mode budget is likewise a one-line native_decide identity.
why it matters
This integer is the numerator of the geometric seed. Downstream, geometric_seed_eq proves (passive modes)/(mode budget) = 11/16 by norm_num on the two definitions. That seed enters $\Omega_\Lambda = 11/16 - \alpha/\pi$, the vacuum-energy-is-mode-fraction identity, and the structural consistency check for the cosmic phase-equilibrium hypothesis.
The parent certificate PhaseSaturationVacuumCert packages the resulting bounds ($0 < \Omega_\Lambda < 1$, $\Omega_\Lambda < 11/16$) together with the mode partition and the closure $\Omega_\Lambda + \Omega_{\mathrm{matter}} = 1$. In the broader RS picture the construction dissolves the $10^{120}$ vacuum-energy discrepancy by treating vacuum energy as a dimensionless $O(1)$ mode fraction rather than a density renormalized against $M_{\mathrm{Pl}}^4$. The open piece remains the hypothesis that cosmic equilibrium actually equals this passive fraction (explicit falsifier attached to that hypothesis interface).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.