canonicalThreshold_pos
plain-language theorem explainer
The canonical cosmology threshold is strictly positive. Anyone comparing domain costs to that cutoff in the Li-7 Spite-plateau module needs this fact. The proof is a one-line wrapper: unfold the threshold and close by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T$, where $T$ is the $\varphi$-dependent canonical threshold of the module.
background
Cosmology RS Module 12 treats the lithium-7 Spite plateau. The RS prediction band is $(4.69,4.86)\times 10^{-10}$; the observed window is $(4.0,5.2)\times 10^{-10}$, recorded as RS_PASS. The module is marked structural (zero sorry, zero axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the forcing chain. A tighter elementary bound is available: $\varphi>1.5$, proved from $\sqrt{5}>2$. The canonical threshold is a $\varphi$-dependent cutoff used alongside domain costs (nonnegative cost functionals imported from the Cost layer) when the module certifies the Spite-plateau comparison.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then finish by linarith using the upstream lemma $\varphi>1.5$ (from $\sqrt{5}>2$). No further case splits or cost identities are required.
why it matters
Structural positivity fact for Cosmology RS Module 12 (Li-7 Spite plateau). It keeps the threshold side of any domain-cost comparison well-defined and strictly above zero, which the module certificate (RSCosmo012Cert / cert_inhabited) relies on as ambient arithmetic. No direct downstream edges are recorded yet; the lemma is local scaffolding-closure for the module rather than a cross-module bridge. It sits downstream of the T6 forcing of $\varphi$ only through the elementary bound $\varphi>1.5$, not through the full Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.