Cosmology Hubble Tension From Bit Jcost Phi Band

The predicted tension band

The Hubble tension is the disagreement between two ways of measuring how fast the universe expands. Local observations of supernovae give one rate, while the cosmic microwave background gives another. The two rates differ by roughly 8 to 9 percent, and no conventional model fully explains the gap.

In Recognition Science, a framework that derives physical constants from a single cost function, this gap is not a coincidence. The framework's library of formal theorems proves a specific band for the tension amplitude. The amplitude is defined as the product of two numbers: the cost function J evaluated at the golden ratio φ, and the natural logarithm of 2. The theorem jcost_phi_band establishes that J(φ) lies strictly between 0.11 and 0.13. Multiplying this by log 2 ≈ 0.693 gives a band for the tension amplitude between about 0.076 and 0.090, which overlaps the empirical 0.08 to 0.09 range.

This is a derived prediction, not a fit. The value of J(φ) comes from the framework's forced cost function, and φ is the golden ratio, not an adjustable parameter. The library also proves that the amplitude is positive, meaning the framework predicts a real discrepancy in the observed direction: local measurements higher than CMB ones.

What the declaration does not claim is equally important. It does not prove that the empirical tension is exactly this value, only that the framework's prediction falls in the observed range. It does not derive the Hubble constant itself, nor does it explain why the two measurement methods differ. The proof is about a number, not about the physics of supernovae or photons.

/-- 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

This does not claim the empirical tension is exactly the predicted value. This does not derive the Hubble constant or explain the physical cause of the discrepancy. This does not claim the framework's prediction is a measurement.

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: