Pith. sign in
module module low

IndisputableMonolith.Cosmology.CMB_Damping_Scale_v3

show as:
view Lean formalization →

Module packaging the Recognition Science treatment of the CMB photon diffusion (Silk) damping scale. It defines a domain cost on the relevant scale variable, a canonical positive threshold, and a small certificate bundle asserting the v3 numerical/structural claims. Cosmologists comparing RS predictions to the damping tail of the CMB power spectrum would cite it. Content is mostly definitions plus nonnegativity and inhabitance lemmas.

claimIntroduce a domain cost $C$ on the CMB damping-scale variable, prove $C \ge 0$ and evaluate it at the canonical point; fix a canonical threshold $\theta > 0$; and package a certificate $\mathrm{Cert}$ (with an inhabited instance) recording the v3 CMB damping-scale claims in RS-native units.

background

Recognition Science derives cosmology from the same cost geometry used elsewhere in the monolith. The cost module supplies the J-cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by the T5 step of the unified forcing chain. Constants supplies the RS time quantum $\tau_0 = 1$ tick and the golden-ratio ladder with $\varphi$ as the self-similar fixed point (T6).

In this setting the CMB damping scale is the comoving wavenumber (or length) at which photon diffusion erases acoustic peaks. The module treats that scale as a positive real on which a domain cost is evaluated, then compares it to a canonical positive threshold. The certificate object is the standard RS pattern: a structure bundling the numerical/structural assertions so downstream cosmology pages can depend on one inhabited prop rather than scattered lemmas.

proof idea

Definition-heavy module, not a single deep theorem. domainCost is introduced and related to evaluation at a point (domainCost_at_eq); nonnegativity (domainCost_nonneg) follows from the ambient cost axioms imported from Cost. canonicalThreshold is a positive constant (canonicalThreshold_pos). The certificate type CMBDampingScale_v3Cert (with cert and cert_inhabited) packages those facts into an inhabited record. No long tactic developments; the argument is definitional wiring plus positivity/nonnegativity from upstream cost structure.

why it matters in Recognition Science

Places the Silk damping scale inside the RS cost-and-ladder language so CMB observables sit on the same footing as particle masses and coupling constants. Upstream it rests only on Constants and Cost (J-uniqueness, $\varphi$, tick units). Downstream usage is not yet wired in this graph snapshot (used_by empty), so the module currently acts as a self-contained v3 certificate island for cosmology audits rather than a lemma feeding a named parent theorem. It touches the broader program of matching RS-native scales to classical cosmological lengths without introducing new free parameters beyond the forced $\varphi$-ladder.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)