canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the RS cosmology module is strictly positive. Anyone citing the structural Hubble-tension certificate (Module 3) needs this positivity fact. The proof is a one-line unfold of the threshold definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the module's canonical threshold (an explicit real expression in the golden ratio $\varphi$).
background
RS Cosmology Module 3 packages a structural theorem on the Hubble tension: the ratio $H_{0,\mathrm{local}}/H_{0,\mathrm{CMB}}$ lies in $(1.075, 1.091)$, with the SH0ES value $1.0837$ inside the band (status RS_PASS, zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The upstream lemma phi_gt_onePointFive records the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a derived real scale in this module (sibling of the domain-cost functionals), built from $\varphi$ so that positivity is immediate from that bound.
Imports are Mathlib, Constants, and Cost; the local setting is pure real arithmetic on RS constants, not a full FLRW derivation.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau_{\mathrm{can}}$ by linarith using the single upstream fact $\varphi > 1.5$. No case split, no induction, no cost-functional identities.
why it matters
Positivity of the canonical threshold is a tiny but necessary arithmetic hinge inside the Module-3 structural package on Hubble tension. Downstream siblings include the certificate RSCosmo003Cert and its inhabited proof; this lemma keeps every comparison that mentions the threshold well-defined and oriented.
In the broader Recognition framework it sits on T6 ($\varphi$ forced) and the RS-native constant layer ($c=1$, $\hbar=\varphi^{-5}$, etc.). It does not itself produce the $(1.075,1.091)$ band; it only clears the sign of the scale those comparisons use. With used_by empty at the graph edge, its role is local hygiene inside the cosmology certificate rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.