canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the RS cosmology baryon-density module is strictly positive. Cosmology arguments that gate domain cost or structural Omega_b comparisons on that threshold cite this fact. The proof unfolds the definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real constant obtained by unfolding its definition in terms of the golden ratio $\varphi$) satisfies $0 < \text{canonical threshold}$.
background
RS Cosmology Module 9 is a structural (zero-sorry) package for baryon density: it records that $J(\varphi)(1-J(\varphi))/2 \approx 0.052$ sits next to the observed $\Omega_b \approx 0.0493$. Here $J$ is the recognition cost $J(x)=(x+x^{-1})/2-1$, and $\varphi$ is the self-similar fixed point forced at T6.
The module imports Constants and Cost, so the golden-ratio lower bound and the J-cost API are in scope. The sibling definition canonicalThreshold is a real built from $\varphi$; positivity of that constant is the local claim.
Upstream, phi_gt_onePointFive states the tighter bound $\varphi > 1.5$, proved from $\sqrt{5}>2$ via the closed form $\varphi=(1+\sqrt{5})/2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ from phi_gt_onePointFive. No further lemmas or case splits.
why it matters
Positivity of the threshold is bookkeeping needed before any comparison that treats the threshold as a strict gate on domain cost or on the structural baryon-density identity in this module. The parent certificate objects in the same file (RSCosmo009Cert, cert, cert_inhabited) package the module as a structural theorem; this lemma supplies the elementary sign fact those certificates may rely on.
It sits downstream of the T6 forcing of $\varphi$ and the Constants bound $\varphi>1.5$, and upstream of any cosmology use that needs the threshold to be a positive scale. No external used_by edges are recorded yet. It does not itself derive the numerical $\Omega_b$ match; that match is the module-level structural claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.