Physics Bao

Baryon acoustic oscillations

In Recognition Science, baryon acoustic oscillations (BAO) are the predicted regular clustering of matter on large scales, a fossil of sound waves that travelled through the baryon-photon fluid before recombination. The module IndisputableMonolith.Physics.BAO derives the standard BAO quantities from Recognition Science's predicted cosmological parameters, not from fitted inputs. The central number is the sound horizon r_s, the distance sound could travel in that early fluid, which the module sets at 147 megaparsecs and proves to be within 0.5 megaparsecs of 147.18.

The sound speed in the baryon-photon fluid is defined as c_s = c/√(3(1+R)), where R is the baryon-to-photon density ratio. The module proves this speed is positive for physical densities, that it decreases as the baryon loading R increases, and that in the pure radiation limit it equals c/√3. The baryon loading itself, R(z) = R₀/(1+z), is established to decrease with redshift, meaning the baryon contribution to the fluid's inertia grows as the universe expands. The sound horizon is then the integral of this speed over cosmic time, encoded in the constant 147 megaparsecs.

The module also derives the spectral index n_s from the number of e-folds of inflation, with the theorem that 60 e-folds give n_s = 1 - 1/30 ≈ 0.967, and that any positive number of e-folds yields a red-tilted spectrum (n_s < 1). The baryon and matter densities are set as constants, with the established inequality that matter exceeds baryons. The correlation peak of the BAO signal is defined as twice the sound horizon, and the module proves this peak is approximately 294, matching the observed scale. The wavenumbers of the BAO peaks are established to be evenly spaced, a signature prediction of the acoustic oscillation picture.

What the module establishes in plain language is that the standard BAO observables, the sound horizon, the peak scale, the spectral tilt, and the peak spacing, all follow from Recognition Science's own cosmological parameters. The numbers are not imported from conventional cosmology; they are derived from the framework's predicted densities and inflation. The theorems in the module are computational, checked by norm_num and linarith, and they establish internal consistency: the sound horizon is positive, the peak is near 294, and the peaks are evenly spaced. The physical bridge from recognition events to these cosmological parameters is not part of this module; that connection is a separate, open question.

THEOREM rs_sound_horizon_consistent · IndisputableMonolith/Physics/BAO.lean

THEOREM sound_speed_radiation_limit · IndisputableMonolith/Physics/BAO.lean

THEOREM spectral_index_60efolds · spectral_index_red_tilt · IndisputableMonolith/Physics/BAO.lean

THEOREM bao_peak_approximately_150 · IndisputableMonolith/Physics/BAO.lean

THEOREM bao_peaks_evenly_spaced · IndisputableMonolith/Physics/BAO.lean

THEOREM baryon_loading_decreasing · IndisputableMonolith/Physics/BAO.lean

What this page does not claim

The physical bridge from recognition events to the cosmological parameters is not established in this module. The module does not fit the sound horizon to data; it sets 147 megaparsecs and proves consistency with 147.18. The spectral index formula is a definition, not a derivation from the forcing chain.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/BAO.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: