dm_is_dominant
plain-language theorem explainer
Recognition Science cosmology states that the dark matter to baryon density ratio exceeds 5. Researchers modeling ledger shadows or phantom sectors would cite the result to match the observed dominance of non-luminous matter. The proof is a one-line wrapper that unfolds the ratio definition and evaluates the supplied constants by direct computation.
Claim. $0.27 / 0.05 > 5$
background
The module treats dark matter as ledger shadows arising from the σ=0, Z≠0 phantom sector at the temporal resolution of the 8-tick parity cycle. It supplies the conventional density parameters Ω_dm = 0.27 and Ω_b = 0.05 together with their ratio definition. These values are introduced as noncomputable reals that encode the observed requirement of roughly five times more non-luminous than baryonic matter.
proof idea
One-line wrapper that unfolds dm_baryon_ratio, omega_dm, and omega_b then applies norm_num to confirm the numerical inequality.
why it matters
The declaration anchors the numerical dominance required by the COS-010 ledger-shadow account inside the 8-tick phase structure. It supplies the concrete ratio that later unification steps in PhantomSectorStratification are expected to explain from the forcing chain. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.