hubbleBand_width_pos
plain-language theorem explainer
The declaration establishes that the lower bound of the predicted Hubble ratio band is strictly below its upper bound. Cosmologists working within Recognition Science would cite this to confirm the interval (1.075, 1.091) is non-degenerate and contains the observed SH0ES/Planck ratio of 1.083. The proof is a one-line wrapper that unfolds the definition of the band and applies numerical normalization.
Claim. The lower endpoint of the Hubble ratio band is strictly less than the upper endpoint: $1.075 < 1.091$.
background
The module constructs a pipeline from Z-aging channels in the recognition field to a predicted late/early Hubble ratio band. The band is defined as the closed interval with endpoints 1.075 and 1.091, chosen so that it contains the empirical ratio 1.083. Upstream, the definition hubbleRatioBand supplies these fixed numerical bounds derived from the amplitude formula r_H = 1 + (1/φ^5) · c with φ^5 in (11.05, 11.1).
proof idea
The proof is a one-line wrapper that unfolds the definition of the Hubble ratio band and applies numerical normalization to verify the inequality between its endpoints.
why it matters
This result confirms the non-degeneracy of the interval that Recognition Science predicts for the Hubble tension via Z-complexity aging over cosmic time. It is a prerequisite step inside the A5 precision closure pipeline before any certification of the tension resolution can be stated. The module doc notes that the band arises from five Z-aging channels (D=5) each contributing a rung on the phi-ladder, with the numerical width fixed by the Fibonacci identity for φ^5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.