canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the inflaton-mass phi-ladder module is strictly positive. Cosmology arguments that keep domain costs and ladder scales well-defined cite this positivity lemma. The proof is a one-line wrapper: unfold the threshold and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the real constant defined from the golden ratio $\varphi$ in this module) is strictly positive: $0 < T_{\mathrm{can}}$.
background
This module builds a structural account of the inflaton mass on the Recognition Science phi-ladder: $m_{\mathrm{inflaton}} = \varphi^k E_{\mathrm{coh}}$, with the target scale near $10^{13},\mathrm{GeV}$ at rung $k \approx 57$ when $E_{\mathrm{coh}} \approx 0.121,\mathrm{MeV}$. The module is marked structural (zero sorry, zero axiom).
The golden ratio is $\varphi = (1+\sqrt{5})/2$. The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. Sibling definitions introduce a domain cost (nonnegative, with an evaluation identity) and the canonical threshold itself; this lemma only records that the threshold is positive so later certificates can treat it as a genuine scale.
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 are needed: after unfolding, positivity is a linear-arithmetic consequence of that bound on $\varphi$.
why it matters
Keeps the threshold scale in the inflaton-mass construction strictly above zero, so domain-cost and ladder comparisons in this cosmology module are not vacuous. The module doc frames the whole development as a structural theorem for $m_{\mathrm{inflaton}} \sim 10^{13},\mathrm{GeV}$ via $\varphi^k E_{\mathrm{coh}}$ on the phi-ladder (primer mass formula: yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). No downstream uses are recorded in the graph yet; the lemma sits with the local certificate bundle (InflatonMass3Cert, cert, cert_inhabited) that packages the structural claim. It does not itself fix the rung or the GeV conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.