lower_pos
plain-language theorem explainer
The RS-predicted lower bound on the late-to-early Hubble ratio is strictly positive. Cosmologists working within the BIT-Z-aging model cite this to confirm the predictive interval begins above zero. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. $1.075 > 0$, where $1.075$ denotes the RS-predicted lower bound on the late-to-early $H_0$ ratio.
background
The module records the RS prediction for the Hubble tension as a band on the late-to-early $H_0$ ratio. Recognition Science derives this band from cosmic Z-aging on the BIT kernel, placing the interval at $(1.075, 1.091)$ around the central empirical value $1.083$. The lower edge is introduced as the explicit constant $1.075$ in RS-native units.
proof idea
This is a one-line wrapper that unfolds the definition of the lower bound constant to expose the literal value $1.075$ and then invokes norm_num to verify positivity.
why it matters
The result secures positivity of the lower edge of the RS-predicted Hubble ratio band, a prerequisite for the structural cert HubbleTensionCert recorded in the same module. It aligns with the phi-rational shift near $1 + 1/(2 phi^2)$ and supports the falsification criterion that a measured ratio falling outside the band at greater than $2 sigma$ would challenge the BIT-Z-aging account.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.