Gravity Hubble Tension Sound Horizon Preservation

Sound horizon preservation

The sound horizon is the maximum distance a pressure wave could have traveled through the hot, dense plasma of the early universe before that plasma cooled into neutral atoms. This distance, set around redshift 1100, leaves a measurable imprint on the cosmic microwave background and provides a standard ruler for cosmology. The Recognition Science framework's library contains a machine-checked theorem, sound_horizon_preservation, that establishes a specific property: for any positive value of the sound horizon in the standard cosmological model, there exists an identical value in the framework's proposed modification. In plain language, the framework's modification does not change the sound horizon at all.

The theorem is a formal statement about the framework's own model, which it calls the ILG kernel. This kernel is designed to alter only the late-time inference of the Hubble constant, the rate of cosmic expansion, by adjusting how distant sources are weighted. The sound horizon, however, is fixed by early-universe physics, before that late-time weighting matters. The proof is a simple logical identity: it takes any positive sound horizon value from the standard model and returns the same value. The theorem's strength is that it is verified by a machine, not that it is physically surprising.

The framework uses this result to claim its proposed resolution of the Hubble tension is physically consistent. The Hubble tension is the discrepancy between measurements of the expansion rate from the early universe, which give about 68.8 km/s/Mpc, and from the late universe, which give about 73 km/s/Mpc. The framework's model predicts a late-time value of 71.8 km/s/Mpc, with an uncertainty of 1.2, which it claims reduces the tension from about 4 sigma to about 1 sigma. The sound horizon preservation is the piece that says this shift does not require rewriting early-universe physics.

What the declaration does not claim is just as important. It does not claim that the ILG kernel is a correct description of the universe, nor that the Hubble tension is actually resolved. The theorem only states a logical consistency condition within the framework's own definitions. It does not compare the model's predictions to any actual astronomical data, and it does not prove that the sound horizon is preserved in the real cosmos. The numbers 71.8 and 68.8 are defined constants in the framework, not measured values. The theorem is a formal statement about a model, not an empirical result.

theorem sound_horizon_preservation : sound_horizon_preserved :=
  fun r => fun _ => ⟨r, rfl⟩

/-- RS/ILG prediction for late-time H₀ (km/s/Mpc). -/
def H0_ILG : ℝ := 71.8

/-- Uncertainty on the ILG H₀ prediction. -/
def H0_ILG_sigma : ℝ := 1.2

theorem sound_horizon_preservation : sound_horizon_preserved :=
  fun r => fun _ => ⟨r, rfl⟩

What this page does not claim

The ILG kernel is a correct description of the universe. The Hubble tension is actually resolved by the framework's model. The sound horizon preservation theorem applies to any real cosmological data.

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/Gravity/HubbleTension.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: