Omega_Lambda_band_unconditional
plain-language theorem explainer
The RS dark-energy fraction sits strictly inside (0.5, 0.69). Cosmologists comparing the ledger prediction to the observed Ω_Λ band cite this as the unconditional numerical envelope. The proof is a one-line pairing of the already-proved lower and upper bounds.
Claim. Let $\Omega_\Lambda := 11/16 - \alpha/\pi$ be the Recognition Science dark-energy fraction (cube-geometry seed minus the electromagnetic correction). Then $0.5 < \Omega_\Lambda < 0.69$.
background
This module treats dark energy as the equilibrium vacuum share of a finite discrete ledger. Phase-saturation pressure on that ledger appears, at cosmic scale, as vacuum energy. The explicit prediction is $\Omega_\Lambda = 11/16 - \alpha/\pi$: the passive-mode fraction $11/16$ of the $D=3$ cube (mode budget $2^4=16$ after double-entry) corrected by the measured fine-structure constant over $\pi$.
Spatial dimension $D=3$ is forced upstream (T8/T9). The geometric seed $11/16=0.6875$ is already combinatorial. The two sibling bounds used here are $\Omega_\Lambda>0.5$ (from $\alpha/\pi<1/6$) and $\Omega_\Lambda<0.69$ (since $\Omega_\Lambda<11/16<0.69$).
The module still carries open hypotheses (CosmicPhaseEquilibrium, vacuum_fraction_bridge) that identify this number with the cosmological parameter; the present statement is purely the numerical band on the defined real.
proof idea
Term-mode pair constructor. The goal is a conjunction; the proof supplies the two conjuncts as ⟨Omega_Lambda_gt_05, Omega_Lambda_lt_069⟩.
The lower bound unfolds the definition and applies a tight $\alpha/\pi$ inequality via linarith. The upper bound is a short calc: $\Omega_\Lambda < 11/16$ (positive $\alpha/\pi$ correction) and $11/16 < 0.69$ by norm_num. No new arithmetic is done at this declaration.
why it matters
Closes the unconditional precision band advertised in the module header for the RS $\Omega_\Lambda$ prediction ($\approx 0.6852$). It packages the seed-minus-EM formula into a referee-ready interval that overlaps the observed dark-energy fraction without invoking the still-open cosmic-equilibrium hypotheses.
Framework landmarks in play: T8 forcing $D=3$ (cube geometry behind the $11/16$ seed), and the $\alpha$ band that supplies the small EM correction. Downstream use sites are not yet wired in-tree (used_by empty); the natural consumers are any comparison lemmas against Planck/SNIa $\Omega_\Lambda$ and any discharge of vacuum_fraction_bridge once the ledger-to-cosmology map is proved.
Does not itself settle whether phase saturation is the physical origin of $\Lambda$; it only locks the numerical claim once the definition is accepted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.