canonicalThreshold_pos
plain-language theorem explainer
The canonical astrophysical threshold used in RS Module 3 is strictly positive. Anyone citing the neutron-star radius match (φ⁵ km ≈ 11.09 km) needs this positivity fact before comparing to the 10–13 km observational window. The proof is a one-line unfold-and-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold constant of the module satisfies $0 < \mathrm{canonical\,threshold}$. After unfolding its definition in terms of the golden ratio $\varphi$, positivity follows from the elementary bound $\varphi > 1.5$.
background
RS Astrophysics Module 3 packages the neutron-star radius claim: the RS-native length $\varphi^5$ km evaluates to about 11.09 km and therefore sits inside the observed 10–13 km band. 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 Recognition forcing chain. A tighter elementary lower bound $\varphi > 1.5$ is already proved in the Constants library (from $\sqrt{5} > 2$). The module defines a canonical threshold expression in $\varphi$; the present lemma only records that this expression is positive.
Sibling facts in the same file establish non-negativity of the domain cost and package the whole module into a certificate RSAstro003Cert.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the imported lemma phi_gt_onePointFive (which states $(1.5:\mathbb{R}) < \varphi$). No further case splits or Recognition-specific identities are required; ordinary real arithmetic closes the goal.
why it matters
Positivity of the threshold is the first arithmetic hygiene fact needed before the module can claim a numerical match of $\varphi^5$ km against neutron-star radii. In the broader RS framework this sits next to the landmark $Z_{\mathrm{cf}} = \varphi^5 \in (11,12)$ and the mass/length ladder built from powers of $\varphi$. The module itself is already a closed structural theorem; this lemma is a tiny supporting brick inside that certificate. No downstream consumers are recorded yet, so its immediate role is local to the Module-3 certificate construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.