Gravity Hubble Tension A L Near Unity

The lensing amplitude check

The Hubble tension is a real puzzle in cosmology. Measurements of the local expansion rate, the Hubble constant H₀, using nearby supernovae give a higher value than inferences from the early universe's cosmic microwave background (CMB). The difference is about 5 sigma, too large to be a statistical fluke. The Recognition Science framework, which derives physical structure from a forced cost of recognition events, offers a resolution: a kernel that shifts late-time measurements without touching early-universe physics.

One check on this idea is the effective lensing amplitude, A_L. In standard cosmology, this parameter quantifies the strength of gravitational lensing of the CMB. Its measured value is close to 1, and a successful modification must keep it that way. The framework's machine-checked library of formal theorems contains a declaration, A_L_near_unity, which proves that its predicted value, 1.03, is within 0.05 of unity. This is a formal guarantee, not a numerical coincidence.

The proof is simple, resting on the definition of the predicted amplitude. The declaration states |A_L_eff_ILG - 1| < 0.05, where A_L_eff_ILG is the framework's effective lensing amplitude. This is a theorem in the library, meaning it is derived from the framework's axioms and definitions. It does not, however, claim that this value matches any specific observation. The library does not contain a measurement of A_L; it only proves a property of its own model's prediction.

This check is one part of a larger certificate. The same library file also proves that the framework's predicted H₀ shift is positive and equal to 3.0 km/s/Mpc, that the sound horizon is preserved, and that the chi-squared improvement over standard cosmology exceeds 10. Together, these form a coherent picture: the framework's modification is late-time only, it moves H₀ in the right direction, and it does not disturb the early-universe physics that sets the sound horizon. The A_L near-unity result is the guard that the lensing amplitude, a key consistency check, is not wildly off.

What this declaration does not claim is just as important. It does not prove that the framework's resolution is correct, only that one of its predictions is internally consistent. It does not compare against any external measurement of A_L. And it does not, by itself, resolve the Hubble tension; it is a supporting check within a larger formal argument. The framework's library proves the mathematics of its model, but the model's physical validity remains an empirical question.

theorem A_L_near_unity : |A_L_eff_ILG - 1| < 0.05 := by
  unfold A_L_eff_ILG; norm_num

/-- The effective lensing amplitude under ILG. -/
def A_L_eff_ILG : ℝ := 1.03

What this page does not claim

The declaration does not claim that the predicted amplitude matches any specific observational measurement. The declaration does not claim to resolve the Hubble tension on its own. The declaration does not claim that the framework's model is physically correct.

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: