Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.FlatnessProblem

show as:
view Lean formalization →

The Cosmology.FlatnessProblem module defines the density parameter Ω = ρ/ρ_c and assembles lemmas showing that flat geometry minimizes J-cost under phi-forcing. Cosmologists examining the flatness problem would cite its rs_flatness_necessity and flat_minimizes_cost results. The module aggregates definitions and supporting statements from the imported Constants, Cost, and PhiForcing modules.

claim$\Omega = \rho / \rho_c$ measures spatial curvature, with $\Omega=1$ for flat Euclidean geometry, $\Omega>1$ for positive curvature, and $\Omega<1$ for negative curvature; these quantities are related via J-cost minimization on the phi-ladder.

background

The module resides in the cosmology domain and imports the RS time quantum τ₀ = 1 tick from Constants, the J-cost structure from Cost, and the PhiForcing result that φ is forced by self-similarity in a discrete ledger with J-cost. The supplied module documentation states that Ω = ρ/ρ_c measures spatial curvature with the three cases listed above. Upstream PhiForcing supplies the self-similar fixed point that anchors the phi-ladder used for density and curvature relations.

proof idea

This is a definition module collecting DensityParameter, omega_observed, critical_density, omega_deviation_grows, planck_fine_tuning, extreme_fine_tuning_required, inflation_flattens, rs_flatness_necessity, curvatureCost, flat_minimizes_cost, critical_density_from_phi, and phi_cosmology_relations; it contains no internal proof bodies and relies on the imported modules for its supporting lemmas.

why it matters in Recognition Science

The module supplies the RS treatment of the flatness problem, linking J-cost minimization to the requirement that Ω = 1. It feeds the broader cosmological relations in the Recognition framework and connects to the forcing chain landmarks T5–T8 together with the Recognition Composition Law. No downstream uses are recorded.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)