Omega_Lambda_def
plain-language theorem explainer
The RS dark-energy fraction equals 11/16 minus α/π by definitional equality. Anyone citing the phase-saturation vacuum formula uses this to lock the symbolic expression to the named constant. The proof is pure reflexivity on the definition body.
Claim. The Recognition Science dark-energy density parameter satisfies $\Omega_\Lambda = \frac{11}{16} - \frac{\alpha}{\pi}$, where $\alpha$ is the measured fine-structure constant (CODATA anchor).
background
This module identifies the cosmological dark-energy fraction with the equilibrium vacuum share of a discrete ledger under phase saturation. The geometric seed is the passive-mode fraction from $Q_3$ cube counting, equal to $11/16$; an electromagnetic correction subtracts $\alpha/\pi$.
Locally, $\Omega_\Lambda$ is defined as the real $11/16 - \alpha/\pi$, and $\alpha$ is the single measured input Constants.ExternalAnchors.alpha_CODATA. The same formula appears as DEFINITION C-010 in the sibling cosmological-constant derivation module.
The broader chain (module doc) runs: finite phase capacity $\varphi^{45}$, cosmic equilibrium of matter excitations with vacuum modes, then vacuum fraction equal to the passive mode fraction, numerically $\approx 0.6852$.
proof idea
One-line term proof by rfl. The left-hand side is the named definition whose body is exactly $11/16 - \alpha/\pi$, so definitional equality closes immediately. No lemmas are applied.
why it matters
Pins the symbolic RS prediction for $\Omega_\Lambda$ so later positivity and upper-bound lemmas (Omega_Lambda_pos, Omega_Lambda_lt_seed, Omega_Lambda_lt_one, Omega_Lambda_bounds) can rewrite against a concrete arithmetic expression. It is the definitional half of the module's proved Omega_Lambda_RS package (definition plus basic bounds).
It does not close the physical bridge: CosmicPhaseEquilibrium and vacuum_fraction_bridge remain hypotheses with explicit falsifiers. The $11/16$ seed itself is combinatorial (proved elsewhere via mode counting); this declaration only records the seed-minus-$\alpha/\pi$ formula. No forcing-chain step (T0–T8) is discharged here; the link is cosmological identification, not dimensional forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.