module module high

`IndisputableMonolith.Physics.BAO`

The Physics.BAO module defines the baryon loading ratio R(z) and related plasma quantities for baryon acoustic oscillations inside the Recognition Science framework. Cosmologists adapting standard BAO calculations to RS units with phi-based constants would cite these objects when deriving the sound horizon or spectral index. The module consists of a core definition of R(z) decreasing with redshift, followed by sound-speed functions and elementary positivity lemmas verified algebraically from the J-cost core.

claim$R(z) = 3ρ_b/(4ρ_γ) = R_0/(1+z)$, where $R_0 = 3Ω_b/(4Ω_γ)$ at redshift zero.

background

Recognition Science builds cosmological quantities from the J-cost function supplied by the imported JcostCore module. The baryon loading ratio quantifies baryon inertia relative to the photon fluid and thereby controls acoustic-wave propagation before recombination. This module introduces R(z) as inversely proportional to (1+z) together with the sound speed in the baryon-photon plasma and its radiation-era limits.

proof idea

This is a definition module, no proofs. It introduces the baryon loading ratio from density ratios, defines sound speed as a function of R(z), and records basic properties such as positivity and monotonic decrease through direct algebraic verification.

why it matters in Recognition Science

These BAO definitions supply the plasma inputs needed for spectral-index and matter-density calculations in Recognition Science cosmology. They extend the J-cost framework to photon-baryon dynamics and support later derivations of the BAO scale, the alpha band, and the phi-ladder mass spectrum.

scope and limits

Does not compute the integrated sound horizon distance.
Does not include late-time dark energy contributions.
Does not model nonlinear structure formation.
Does not provide numerical fits to observational data.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (21)

def baryon_loading L30
theorem baryon_loading_decreasing L33
def sound_speed L41
theorem sound_speed_positive L44
theorem sound_speed_radiation_limit L52
theorem sound_speed_decreasing L58
def rs_omega_b_h2 L70
def rs_omega_m_h2 L73
theorem matter_exceeds_baryons L76
def rs_spectral_index L81
theorem spectral_index_60efolds L84
theorem spectral_index_red_tilt L90
def rs_drag_redshift L99
abbrev sound_horizon_approx L106
theorem sound_horizon_positive L109
theorem rs_sound_horizon_consistent L114
def bao_peak_wavenumber L121
theorem first_peak_wavenumber L125
theorem bao_peaks_evenly_spaced L132
def bao_correlation_peak L139
theorem bao_peak_approximately_150 L141