canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the stellar-metallicity module is strictly positive. Anyone building on the RS solar-metallicity match J(φ)² ≈ Z_⊙ needs this sign fact as a basic positivity lemma. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold used in the stellar-metallicity comparison is strictly positive: $0 < T_{\mathrm{can}}$.
background
RS Astrophysics Module 7 records the structural match between the squared J-cost at the golden ratio and solar metallicity: $J(\varphi)^2 \approx 0.0139 \sim Z_\odot = 0.014$. Here $J(x) = (x + x^{-1})/2 - 1$ is the unique cost forced by the Recognition Composition Law (T5), and $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point (T6).
The module imports the global constants and cost layers. The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a named real constant in this module whose positivity is needed for later sign and comparison arguments in the metallicity certificate.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ (lemma phi_gt_onePointFive). No further algebraic identities are required once the definition is expanded.
why it matters
Module 7 is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and claims the solar-metallicity match $J(\varphi)^2 \sim Z_\odot$. Positivity of the canonical threshold is a small supporting lemma in that certificate stack (siblings include domainCost_nonneg, RSAstro007Cert, and cert_inhabited). It does not yet feed named downstream theorems, but it closes the sign obligation any later comparison against $Z_\odot$ or domain-cost bounds will need. Framework landmarks in play: T5 (J-uniqueness) and T6 ($\varphi$ forced).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.