canonicalThreshold_pos
plain-language theorem explainer
The canonical metallicity threshold is strictly positive. Cosmology certificates and the solar-metallicity structural match cite this to guarantee a valid positive scale. The proof is a one-line wrapper: unfold the definition and close by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the module's canonical metallicity threshold (built from the golden ratio $\varphi$).
background
Module 10 of the RS cosmology stack records the solar-metallicity match $J(\varphi)^2 \approx 0.01393 \sim Z_\odot = 0.014$ as a structural theorem (no sorry, no axioms). Here $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$, and $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6.
The only upstream fact used is the tighter lower bound $\varphi>1.5$, proved from $\sqrt{5}>2$. Because $J(\varphi)=\varphi-3/2$, that bound is exactly the statement that the cost at $\varphi$ is positive, which feeds any threshold built from $J(\varphi)$ or its square.
Local siblings package domain cost, the threshold definition itself, and the inhabited cosmology certificate for this module.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the single lemma $\varphi>1.5$. No further rewriting or case splits are required; positivity is pure linear arithmetic once the definition is expanded.
why it matters
Keeps the solar-metallicity structural claim on a positive scale: without $0<\tau_{\mathrm{can}}$ the numerical match $J(\varphi)^2\sim Z_\odot$ would sit on a non-physical threshold. The module status line marks the whole file as a structural theorem; this lemma is the positivity gate for that certificate.
It sits downstream of T5 (J-uniqueness) and T6 ($\varphi$ forced), and upstream of the module certificate (RSCosmo010Cert / cert_inhabited). No further used-by edges are recorded yet, so its present role is local to the Module-10 certificate rather than a global forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.