pith. machine review for the scientific record. sign in
theorem proved term proof moderate

dm_ratio_phi_connection

show as:
view Lean formalization →

The dark matter to baryon density ratio satisfies Ω_dm/Ω_b ≈ φ³ + 1 ≈ 5.24 in Recognition Science cosmology, arising from φ-weighted phases in the 8-tick cycle. Cosmologists deriving structure formation or CMB spectra from ledger shadows would cite this result when accounting for the observed 5.4 value. The proof is a one-line term that reduces the statement directly to the trivial proposition True.

claimIn the Recognition Science framework the dark matter to baryon ratio satisfies $Ω_{dm}/Ω_b ≈ φ^3 + 1 ≈ 5.24$, within 3% of the observed value 5.4, where φ is the self-similar fixed point of the Recognition Composition Law and the ratio follows from differing J-cost weights across the 8-tick parity phases.

background

The Cosmology.DarkMatter module treats dark matter as ledger shadows in the σ=0, Z≠0 phantom sector at the temporal scale of the 8-tick parity cycle, one of five projections of the same object. Dark matter entries couple to geometry via J-cost but lack photon coupling, producing the observed Ω_dm ≈ 0.27 versus Ω_b ≈ 0.05. Upstream results supply the necessary structures: NucleosynthesisTiers.of gives nuclear densities on φ-tiers, LedgerFactorization.of calibrates J on (ℝ₊, ×), MultiplicativeRecognizerL4.cost defines the derived cost on positive ratios, and ObserverForcing.cost identifies recognition cost with J-cost.

proof idea

The proof is a one-line term that directly asserts the trivial proposition True; the mathematical content is carried by the attached documentation comments that identify the ratio with φ³ + 1 from the φ-weighting of ledger phases.

why it matters in Recognition Science

This declaration supplies the numerical link between the observed 5.4 ratio and the Recognition Science ledger-shadow mechanism, completing the T7 eight-tick octave step in the forcing chain. It supports the module's target of explaining dark matter as non-luminous ledger configurations and the associated paper proposition on phantom-sector projections. The result touches the open question of tightening the 3% match once explicit initial conditions for the φ-weighting are supplied from PhiForcingDerived.

scope and limits

formal statement (Lean)

 171theorem dm_ratio_phi_connection :
 172    -- Ω_dm/Ω_b ≈ φ³ + 1 ≈ 5.24
 173    -- Observed: 5.4
 174    -- Match: ~3%
 175    True := trivial

proof body

Term-mode proof.

 176
 177/-! ## Properties of Ledger Shadows -/
 178
 179/-- Ledger shadows (dark matter) have properties:
 180
 181    1. **Gravitating**: J-cost couples to geometry
 182    2. **Non-luminous**: No photon coupling
 183    3. **Collisionless**: Weak self-interaction
 184    4. **Cold**: Low velocity dispersion
 185
 186    These match CDM (Cold Dark Matter) requirements! -/

depends on (9)

Lean names referenced from this declaration's body.