DensityParameter
plain-language theorem explainer
DensityParameter packages the cosmic density parameter Ω = ρ/ρ_c with its uncertainty and a positivity constraint on the value. Cosmologists working within Recognition Science cite it when stating the observed near-flatness or when constructing instances such as the measured value. The declaration is a plain structure definition with three fields and no proof obligations.
Claim. The density parameter is the structure consisting of a real number $v > 0$ representing the ratio of energy density to critical density, a real uncertainty $u$, and a witness that $v$ is positive.
background
The module addresses the flatness problem: the observed spatial curvature satisfies Ω = ρ/ρ_c = 1.0000 ± 0.0002, yet |Ω − 1| grows proportionally to a²(t) and would have required extreme fine-tuning at the Planck epoch. Recognition Science resolves this by requiring Ω = 1 as the unique ledger-consistent value obtained from J-cost minimization under phi-constraints. The structure records the measured Ω together with its uncertainty so that downstream statements can refer to the observed datum without recomputing it.
proof idea
Structure definition that directly introduces the three fields value, uncertainty, and value_pos; no lemmas or tactics are applied.
why it matters
The definition supplies the type used by omega_observed to record the measured value 1.0000 ± 0.0002. It anchors the module’s claim that Ω = 1 is the only geometry consistent with ledger structure and J-cost minimization, thereby linking the flatness problem to the Recognition Composition Law and the phi-forcing chain. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.