Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.Baryon_Density_RS

show as:
view Lean formalization →

RS-native baryon-density certificate module: a domain cost, a positive canonical threshold, and an inhabited certificate record. Cosmologists in the Recognition framework cite it when wiring Ω_b to the J-cost stack. Structure is definitional plus elementary nonnegativity and positivity lemmas against Cost and Constants.

claimIntroduces a domain cost $C_{\mathrm{dom}}$, a canonical threshold $\theta_*>0$, and a baryon-density certificate asserting that the RS cost evaluation meets the threshold bound used for the cosmic baryon fraction.

background

Recognition Science reads cosmological densities from the same cost functional that forces the particle spectrum. The Cost import supplies $J(x)=(x+x^{-1})/2-1$ (the unique T5 cost), and Constants fixes the RS time quantum $\tau_0=1$ tick.

Baryon density is treated as a recognition threshold problem: a configuration counts as baryonic in the cosmic budget when its domain cost crosses a canonical level fixed by the golden-ratio ladder, rather than by a free fit to CMB data.

The module therefore sits between pure cost theory and any later $\Omega_b$ assembly, packaging the cost, the threshold, and a certificate type with an inhabited instance.

proof idea

Definition module with light supporting lemmas, not a deep derivation. The domain cost is defined, identified at a reference evaluation, and proved nonnegative. The canonical threshold is defined and proved strictly positive. A baryon-density certificate record is introduced, together with a concrete certificate value and an inhabitedness proof. Argument shape is algebraic identity plus elementary positivity against the imported Cost infrastructure.

why it matters in Recognition Science

Places an RS-native certificate at the cosmology boundary so baryon fraction can be attached to J-cost without extra parameters. The graph currently lists no downstream users, so this is a leaf certificate meant for later $\Omega_b$ assembly. It links Cost (T5 J-uniqueness, RCL) and Constants to the observational baryon slot, and is the natural hook for tying the threshold to eight-tick and $D=3$ forcing (T7, T8) once those cosmology bridges are closed.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)