pith. machine review for the scientific record. sign in
structure definition def or abbrev

HubbleTensionCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 104structure HubbleTensionCert where
 105  shift_positive : 0 < delta_H0
 106  shift_value : delta_H0 = 3.0
 107  chi2_good : delta_chi2_improvement > 10
 108  sound_horizon_ok : sound_horizon_preserved
 109  A_L_ok : |A_L_eff_ILG - 1| < 0.05
 110

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.