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

hubbleTensionCert

show as:
view Lean formalization →

This definition assembles the Z-aging Hubble tension certificate by instantiating the HubbleTensionCert structure with the phi^5 identity, numerical bounds on phi^5, the five-channel count, and the empirical band containment. Cosmologists studying the late/early H_0 discrepancy via recognition-field aging would cite it as the A5 closure for the predicted ratio interval containing 1.083. The construction is a direct record instantiation that wires in the upstream lemmas for each field without additional reasoning.

claimLet $r_H$ be the late-to-early Hubble ratio and let $Z$-aging channels be the five configuration dimensions (matter density, radiation density, dark energy, curvature, scalar perturbation). The certificate asserts the identity $phi^5 = 5 phi + 3$, the bounds $11.05 < phi^5 < 11.11$, that the $Z$-aging channel type has cardinality 5, and that the predicted band for $r_H$ contains the empirical central value 1.083.

background

Recognition Science models the Hubble tension as the cumulative effect of $Z$-complexity aging of the recognition field across cosmic time. The module introduces five $Z$-aging channels, each tied to a rung of the phi-ladder, and gives the amplitude formula $r_H = 1 + (1/phi^5) c$ where $phi^5 = 5 phi + 3$ is the Fibonacci identity and $c$ is an amplitude normaliser. The local setting is the A5 precision closure that places the RS prediction inside the empirical SH0ES/Planck interval.

proof idea

This is a definition that constructs the HubbleTensionCert record by direct field assignment: phi5_fibonacci receives the theorem phi5_eq, phi5_lower receives phi5_gt, phi5_upper receives phi5_lt, five_channels receives zAgingChannel_count, and band_contains receives hubbleBand_contains_empirical. No tactics or further lemmas are applied beyond these assignments.

why it matters in Recognition Science

The declaration supplies the Z-aging instance of the Hubble tension certificate that is consumed by the general HubbleTensionCert definitions in the HubbleTensionBound and HubbleTensionFromBIT modules. It closes the A5 claim in the module documentation by verifying that the predicted ratio band contains the empirical value 1.083. In the framework it links the five-channel correction to the phi-ladder mass formula and the eight-tick octave structure.

scope and limits

formal statement (Lean)

  74noncomputable def hubbleTensionCert : HubbleTensionCert where
  75  phi5_fibonacci := phi5_eq

proof body

Definition body.

  76  phi5_lower := phi5_gt
  77  phi5_upper := phi5_lt
  78  five_channels := zAgingChannel_count
  79  band_contains := hubbleBand_contains_empirical
  80
  81end IndisputableMonolith.Cosmology.HubbleTensionPipelineFromZAging

used by (2)

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

depends on (16)

Lean names referenced from this declaration's body.