Cosmology Hubble Tension From Bit Hubble Tension Pos

The positive tension

The Hubble tension is the disagreement between two ways of measuring how fast the universe expands. Local measurements of nearby supernovae give a higher rate than the rate inferred from the cosmic microwave background. The discrepancy is usually quoted as a few percent, around 0.08 to 0.09 in fractional terms.

In Recognition Science, this discrepancy has a proposed origin. The framework models the expansion history as a discrete record of events, and it derives a predicted amplitude for the tension from its core cost function. The predicted band is H_0^local / H_0^CMB - 1 = J(φ) × log 2, which falls between 0.075 and 0.091. This band overlaps the empirical range from the SH0ES and Planck collaborations.

Within this framework, the declaration hubble_tension_pos establishes a narrow but necessary fact: the predicted amplitude is greater than zero. The proof is short. The cost function J(φ) is positive, and the natural logarithm of 2 is positive, so their product is positive. The theorem is checked in the machine-checked library of formal theorems with no unproved assumptions.

That positivity is not the substantive cosmological claim. The substantive claim is the numerical band itself, which is a separate theorem in the same module. The positivity result is a supporting lemma, the kind of fact that must hold before the band can be meaningful. It rules out the possibility that the framework predicts a negative tension, which would mean local measurements giving a lower rate than the CMB.

What the declaration does not claim is just as important. It does not prove that the Hubble tension exists, that the framework's predicted band is correct, or that the framework's model of cosmology is the right one. It only proves that the specific expression the framework uses for the tension amplitude is positive. The empirical agreement is a comparison, not a derivation.

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

/-- J(φ) > 0. -/
theorem jcost_phi_pos : 0 < Jcost phi :=
  Jcost_pos_of_ne_one phi phi_pos phi_ne_one

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

What this page does not claim

The theorem does not prove that the Hubble tension exists in the observed universe. The theorem does not prove that the framework's predicted band for the tension is correct. The theorem does not establish the framework's cosmological model as the true description of reality.

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: