canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the RS astrophysics pulsar-period module is strictly positive. Anyone building domain-cost comparisons or the module certificate cites this fact. Proof is a one-line unfold of the threshold definition followed by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $T$ of the RS astrophysics module (a real scale built from the golden ratio $\varphi$) satisfies $0 < T$.
background
Astrophysics RS Module 10 packages structural facts about pulsar periods on the $\varphi$-ladder: typical periods near $\varphi^{-1},\mathrm{s}\approx 0.618,\mathrm{s}$ and millisecond periods near $\varphi^{-10},\mathrm{s}\approx 8.1,\mathrm{ms}$. The module is marked structural (zero sorry, zero axioms).
Recognition Science forces $\varphi=(1+\sqrt{5})/2$ as the self-similar fixed point (forcing chain T6). The present declaration concerns a canonical threshold defined from $\varphi$ inside this module; only its positivity is claimed here.
The sole upstream lemma is phi_gt_onePointFive: "$\varphi>1.5$ (since $\sqrt{5}>2$, so $(1+\sqrt{5})/2>1.5$)." That bound is enough for a linear-arithmetic finish once the threshold is unfolded.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi>1.5$ from phi_gt_onePointFive. No further case splits or algebraic identities are required.
why it matters
Minimal positivity gate for the Module 10 structural certificate (RSAstro010Cert / cert_inhabited) and for any later comparison that treats the canonical threshold as a positive scale against domain cost. The module itself sits on the $\varphi$-ladder used for periods and masses (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}}$), so the claim inherits the T6 forcing of $\varphi$ and the eight-tick / octave scaffolding only indirectly. The dependency graph currently lists no downstream users; the lemma is local hygiene for the astrophysics package rather than a cross-module bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.