Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.OmegaLambdaDerivation

show as:
view Lean formalization →

Derives the dark-energy density fraction Ω_Λ from eight-tick DFT mode counting plus a small positive electromagnetic correction. Cosmologists and RS auditors comparing the prediction to Planck cite the resulting strict band 0.683 < Ω_Λ < 0.686. The module fixes total and saturated phase-mode counts on the 8-tick cycle, forms their ratio, then shifts by a bounded EM term.

claimFrom the eight-tick DFT structure one fixes total and saturated phase-mode counts $N_{\mathrm{tot}}$ and $N_{\mathrm{sat}}$, sets $\Omega_{\mathrm{raw}} = N_{\mathrm{sat}}/N_{\mathrm{tot}}$, and applies a small positive electromagnetic correction $\varepsilon_{\mathrm{EM}}$ to obtain $\Omega_\Lambda = \Omega_{\mathrm{raw}} + \varepsilon_{\mathrm{EM}}$ with $0.683 < \Omega_\Lambda < 0.686$.

background

Recognition Science forces an eight-tick octave (forcing-chain T7): discrete time is organized in periods of length $2^3 = 8$, and phase modes of the associated DFT live on that cycle. This cosmology module imports only the RS constants layer and the quarantined external-anchor module used for empirical comparison; the cost-first core stays free of fitted cosmological parameters.

The raw dark-energy fraction is the ratio of saturated modes to total modes under tick addressing. A separate electromagnetic correction, proved positive and small, shifts that raw ratio into the narrow observational window. Downstream certificates then attach the band to the cosmological-constant problem and to Planck likelihood scoring.

proof idea

Definition-first module with supporting numeric inequalities. Total and saturated mode counts are fixed from the 8-tick DFT / tick-addressing structure; the raw ratio is defined from them, with an equality lemma and an evaluated numeric value. The EM correction is introduced as a positive quantity with an upper-bound lemma. Ω_Λ is the corrected sum; two comparison lemmas establish the strict bounds 0.683 < Ω_Λ < 0.686 by arithmetic on those definitions. No deep tactic development beyond the mode counts and the correction bounds.

why it matters in Recognition Science

Supplies the Ω_Λ band consumed by four parents: CosmologicalConstantDerivation (registry C-010: what fixes Λ, against the 10^120 QFT vacuum mismatch), Track4ACert (Track 4.A master certificate bundling the Ω_Λ band with η_B and Planck consistency), VacuumFluctuationStructural (Track 4.B structural address of the vacuum-fluctuation discrepancy), and OmegaLambdaPlanckLikelihood (dataset-specific likelihood certificate for the §7 Ω_Λ falsifier row). The mode count is the direct cosmology-side use of the eight-tick octave (T7). The narrow band is the RS-native target against which Planck data are scored.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (24)