omega_observed
plain-language theorem explainer
The declaration records the observed cosmic density parameter as the record with value 1.0 and uncertainty 0.0002. Cosmologists studying the flatness problem cite it to anchor the Recognition Science claim that only Ω = 1 is ledger-consistent. The definition is a direct record construction whose positivity field is discharged by norm_num.
Claim. The observed density parameter is the record with value 1.0, uncertainty 0.0002 and a proof that the value is positive, where Ω = ρ/ρ_c quantifies deviation from flat spatial geometry.
background
DensityParameter is the structure that encodes Ω = ρ/ρ_c with fields value : ℝ, uncertainty : ℝ and value_pos : value > 0. The module sets the local theoretical setting by stating that observations give Ω = 1.0000 ± 0.0002 while small deviations grow as |Ω − 1| ∝ a²(t), requiring extreme early-time fine-tuning unless ledger structure forces flatness.
proof idea
The definition is a direct record literal that sets value to 1.0 and uncertainty to 0.0002, with the positivity field proved by norm_num.
why it matters
This definition supplies the empirical anchor for the flatness problem resolution. It feeds sibling results on deviation growth and the necessity of flatness under J-cost minimization. The module links the observed value to the Recognition Science claim that Ω = 1 is the only ledger-consistent outcome, consistent with the RCL and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.