canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the RS Chandrasekhar package is strictly positive. Anyone citing the structural identity φ^{-1}·2.33 M_☉ = 1.440 M_☉, or any inequality that treats that threshold as a cutoff, needs this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $\tau$ of this module satisfies $0 < \tau$. (Here $\tau$ is the real constant obtained by unfolding the module's threshold definition in terms of the golden ratio $\varphi$.)
background
This file is Astrophysics RS Module 2. Its stated target is the structural Chandrasekhar identity $\varphi^{-1}\cdot 2.33,M_\odot = 1.440,M_\odot$, recorded as a zero-sorry, zero-axiom theorem package. Sibling declarations introduce a domain cost (built from the RS cost functional) and a canonical threshold constant used as a positive cutoff in that package.
The only external arithmetic input is the golden-ratio lower bound from Constants: $\varphi > 1.5$, which follows from $\sqrt{5} > 2$ and the closed form $\varphi = (1+\sqrt{5})/2$. In RS units $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain; positivity facts about expressions in $\varphi$ are the routine substrate for mass-ladder and threshold inequalities.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold so the goal becomes an explicit inequality in $\varphi$. Discharge that inequality by linarith using the upstream lemma $\varphi > 1.5$. No further case splits or cost-functional identities are required.
why it matters
Positivity of the canonical threshold is the elementary gate that lets later inequalities in the Chandrasekhar structural package treat the cutoff as a genuine positive scale. The module presents the Chandrasekhar relation as an exact RS identity ($\varphi^{-1}$ times the classical 2.33 solar-mass prefactor yields 1.440 solar masses). This lemma does not itself prove that mass formula; it only secures the sign of the threshold constant that the package exposes (via the local certificate RSAstro002Cert and related inhabitants).
In the broader framework it sits downstream of T6 ($\varphi$ forced) and of the elementary bound $\varphi > 1.5$. No forcing-chain step T0–T8 is closed here; the contribution is local arithmetic hygiene for the astrophysics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.