Cosmology Hubble Tension Pipeline From Zaging Hubble Band Contains Empirical

The empirical band

The Hubble tension is the disagreement between two ways of measuring the expansion rate of the universe. Measurements of nearby supernovae, the SH0ES program, give one value for the Hubble constant. Measurements of the early universe's relic light, the Planck satellite, give another. The ratio of these two values sits near 1.083, meaning the two methods disagree by about 8 percent.

In Recognition Science, a ledger, a discrete record of events, underlies a proposed explanation for this discrepancy. The framework's Z-aging model says that light from distant objects appears redshifted not only because space expands, but also because the ledger itself ages. This aging correction is built from five channels: matter density, radiation density, dark energy, curvature, and scalar perturbations. The framework's library, a machine-checked collection of formal theorems, proves a small but precise fact about this model.

The theorem hubbleBand_contains_empirical states that the number 1.083 lies strictly between 1.075 and 1.091. That is all it says. The band is defined as an interval, and the theorem verifies, by direct computation, that the empirical ratio falls inside it. The proof is a simple arithmetic check, not a derivation of the band from first principles.

The honesty of the framework matters here. The amplitude normalizer c, approximately 0.91, is fitted to the empirical ratio that the band is compared against. This means the band is a consistency check of the functional form, not a prediction. The framework does not claim to have derived the value 1.083 from its axioms. It claims only that its chosen band contains that value.

What would close the gap? Deriving the amplitude c from the five aging channels, each contributing its own golden-ratio ladder rung, would turn the consistency check into a prediction. Until then, the word "predicts" does not apply to this result. The theorem is a small, honest step: it confirms that the model's chosen range is not contradicted by the data it was fitted to.

theorem hubbleBand_contains_empirical : hubbleRatioBand.1 < 1.083 ∧ 1.083 < hubbleRatioBand.2 := by
  unfold hubbleRatioBand
  constructor <;> norm_num

/-- Hubble ratio band: (1.075, 1.091) contains empirical 1.083. -/
noncomputable def hubbleRatioBand : ℝ × ℝ := (1.075, 1.091)

What this page does not claim

The band (1.075, 1.091) is not a prediction, because its amplitude is fitted to the empirical ratio. The theorem does not derive the value 1.083 from the framework's axioms. The framework does not claim to resolve the Hubble tension, only to be consistent with one of its observed ratios.

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/HubbleTensionPipelineFromZAging.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: