hubbleTensionCert
plain-language theorem explainer
Recognition Science cosmology assembles this certificate to confirm the predicted Hubble tension amplitude J(φ) log 2 lies in (0.075, 0.091). Researchers modeling the SH0ES-Planck discrepancy within the RS framework cite it to link the phi J-cost band to the observed 0.08-0.09 tension. The construction is a direct record assignment that pulls the interval (0.11, 0.13) from the sibling jcost_phi_band theorem and positivity from hubble_tension_pos.
Claim. The certificate consists of the conjunction that Jcost(φ) satisfies 0.11 < Jcost(φ) < 0.13 together with the assertion that the Hubble tension amplitude is positive, where the amplitude equals Jcost(φ) ⋅ log 2 and Jcost denotes the J-cost function evaluated at the golden ratio.
background
The module derives the Hubble tension from the Recognition Composition Law applied to the golden ratio. Jcost(φ) is the J-cost of φ, defined via the upstream Constants.Jcost_phi_val as the value that produces the band (0.11, 0.13). hubbleTensionAmplitude is the positive quantity Jcost(φ) log 2 that quantifies the relative difference H₀^local / H₀^CMB − 1. The local setting states that RS predicts this amplitude lies in (0.075, 0.091), matching the empirical SH0ES versus Planck tension of approximately 0.08-0.09. Upstream jcost_phi_band establishes the interval by rewriting to Jcost_phi_val and applying the bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo; hubble_tension_pos applies mul_pos to Jcost positivity and the positivity of log 2.
proof idea
The definition constructs the HubbleTensionCert record by direct field assignment. It sets the jcost_phi_band field to the theorem jcost_phi_band and the tension_pos field to the theorem hubble_tension_pos. This is a one-line record construction with no additional tactics or reductions.
why it matters
The certificate supplies the concrete RS band for the Hubble tension and is consumed by the hubbleTensionCert definitions in HubbleTensionBound and HubbleTensionPipelineFromZAging. It realizes the A5 cosmology prediction that J(φ) log 2 falls inside the observed discrepancy interval, closing the arc with zero axioms or sorrys. It connects to the J-uniqueness step (T5) of the forcing chain by using the fixed-point value of φ to generate the tension amplitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.