canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold of RS Cosmology Module 5 is a strictly positive real. Anyone assembling or citing the module certificate (r-tensor vs Planck bound) needs this positivity fact. Proof is a one-line unfold plus linear arithmetic from φ > 1.5.
Claim. The module's canonical threshold $T$ (an explicit real built from the golden ratio $\varphi$) satisfies $0 < T$.
background
RS Cosmology Module 5 is a structural certificate: the r-tensor value $2/(44\varphi^2)\approx 0.0174$ lies below the Planck bound $0.036$, marked CONSISTENT with zero sorry and zero axioms.
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the Recognition forcing chain. The only upstream lemma used here is the elementary tightening $\varphi>1.5$ (from $\sqrt{5}>2$).
The canonical threshold is a named real constant in this module, defined by unfolding to an arithmetic expression in $\varphi$. Sibling facts establish nonnegativity of the domain cost and package the certificate (RSCosmo005Cert).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold to an explicit expression in $\varphi$, then apply linarith with the lemma $\varphi>1.5$. No further case splits or Recognition-cost identities are required.
why it matters
Positivity of the threshold is a structural hygiene fact for the Module 5 certificate: the comparison quantities that sit under the r-tensor / Planck consistency claim are well-defined and oriented correctly. It sits among the module's certificate inhabitants (cert, cert_inhabited, RSCosmo005Cert) even though no named downstream edge is recorded yet.
Framework landmark: $\varphi$ from T6, used only through the elementary bound $\varphi>1.5$. No appeal to RCL, eight-tick structure, or the mass ladder is needed. Closes a tiny positivity obligation inside an already sorry-free cosmology module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.