canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the carbon-oxygen stellar module is strictly positive. Anyone citing the RS C/O structural ratio φ^{-1.5} ≈ 0.504 needs this sign gate before cost or certificate work. Proof is a one-line unfold closed by linear arithmetic from the bound φ > 1.5.
Claim. The module's canonical threshold (a real built from the golden ratio $\varphi$) is strictly positive: $0 < T_{\mathrm{can}}$.
background
Astrophysics RS Module 12 is a structural package for the carbon-oxygen stellar abundance ratio. The module doc states C/O = $\varphi^{-1.5} \approx 0.504$, compared with the empirical value $\sim 0.55$ (about 10% off), and marks the file as a structural theorem with zero sorry and zero axioms.
Recognition Science forces $\varphi = (1+\sqrt{5})/2$ as the self-similar fixed point (T6). The Constants library supplies the elementary tightening $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a real constant in this module defined from $\varphi$; sibling declarations (domain cost, nonnegativity, and the RSAstro012 certificate) sit beside it and presuppose a well-defined positive scale.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting inequality by linarith using the upstream lemma $\varphi > 1.5$. No Recognition-cost identities, case splits, or further arithmetic are required.
why it matters
Local hygiene for the C/O structural layer: positivity of the threshold removes a hidden sign assumption before domain-cost and certificate constructions (domainCost, RSAstro012Cert, cert_inhabited) can treat $\varphi^{-1.5}$ as a positive scale. The module is already marked structural (0 sorry, 0 axiom); this lemma is one of the elementary gates that keep that status honest.
It lives in the astrophysics stack rather than the T0–T8 forcing chain, but it inherits $\varphi$ from Constants, which is forced at T6. No downstream used_by edges are recorded yet, so the result is presently a module-internal positivity fact rather than a cited lemma in a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.