canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold (the φ-dependent cost cutoff in the solar-radius astrophysics module) is strictly positive. Anyone wiring domain-cost inequalities or the RSAstro008 certificate cites this fact. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The module's canonical threshold $\tau$ (the $\varphi$-dependent cost cutoff) satisfies $0 < \tau$.
background
Module 8 of the RS astrophysics layer records the solar-radius match $\varphi^{43},\mathrm{m} \approx R_\odot$ (about 0.6% relative error) and packages it as a structural theorem with no sorry and no extra axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified chain. The only upstream fact used here is the tighter numerical bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. Sibling definitions supply a domain cost functional and the threshold itself; positivity of that threshold is the elementary gate before any cost comparison can be stated.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau$ by linarith using the lemma $\varphi > 1.5$. No further case splits or RS identities are required.
why it matters
Positivity is the minimal arithmetic fact needed before the domain-cost nonnegativity and certificate inhabitants in this module can be used as cutoffs. The parent packaging is the RSAstro008 structural certificate for the solar-radius rung $\varphi^{43}$. In the broader framework this sits on the $\varphi$-ladder mass/length formulas and on T6 ($\varphi$ forced); it does not itself invoke RCL, the eight-tick octave, or $D=3$. No downstream theorems are recorded yet; the lemma is infrastructure for the module certificate rather than a cited step in a longer forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.