Cosmology Hubble Tension From Bit Hubble Tension Amplitude

The Hubble tension amplitude

The Hubble tension is the disagreement between two ways of measuring how fast the universe expands. Local observations of supernovae, led by the SH0ES team, give a higher value for the Hubble constant H_0 than the value inferred from the cosmic microwave background (CMB) as seen by Planck. The ratio of the two, H_0^local / H_0^CMB - 1, is the tension amplitude; observations place it around 0.08 to 0.09, meaning the local rate is about eight to nine percent higher.

In Recognition Science, the framework derives a specific value for this amplitude. The declaration hubbleTensionAmplitude defines the amplitude as J(φ) × log(2), where J is the recognition cost function and φ is the golden ratio. The framework's machine-checked library proves that J(φ) lies strictly between 0.11 and 0.13, and since log(2) is about 0.693, the product lies strictly between 0.076 and 0.090. This band overlaps the observed 0.08 to 0.09 range. The framework also proves the amplitude is positive, a trivial but formally checked fact.

What the declaration does not do is explain the physical mechanism behind the tension. It establishes a numerical band, not a causal story. It does not claim that the tension is resolved, nor that one measurement is wrong. It does not derive the Hubble constant itself, only the ratio between the two measured values. The comparison to observation is an empirical check, not a theorem; the framework's derivation of the band is what is proved.

/-- J(φ) ∈ (0.11, 0.13). -/
theorem jcost_phi_band :
    (0.11 : ℝ) < Jcost phi ∧ Jcost phi < 0.13 := by
  rw [Constants.Jcost_phi_val]
  exact ⟨by linarith [phi_gt_onePointSixOne],
         by linarith [phi_lt_onePointSixTwo]⟩

/-- RS Hubble tension amplitude = J(φ) × log(2). -/
noncomputable def hubbleTensionAmplitude : ℝ :=
  Jcost phi * Real.log 2

/-- Hubble tension > 0: J(φ) > 0 and log(2) > 0. -/
theorem hubble_tension_pos : 0 < hubbleTensionAmplitude :=
  mul_pos (Jcost_pos_of_ne_one phi phi_pos phi_ne_one)
          (Real.log_pos (by norm_num))

What this page does not claim

The framework does not explain why the SH0ES and Planck measurements differ. The framework does not claim that the Hubble tension is resolved or that either measurement is incorrect. The framework does not derive the Hubble constant itself, only the ratio between two measured values.

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/Cosmology/HubbleTensionFromBIT.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: