canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS gravity module is strictly positive. Anyone building positivity or scale arguments for tidal deformability or domain-cost comparisons would cite it. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $\tau$ of the RS gravity module satisfies $0 < \tau$. Here $\tau$ is the fixed real expression in the golden ratio $\varphi$ used as the module's reference scale.
background
This module develops structural RS gravity facts (session 3), with status STRUCTURAL THEOREM (0 sorry, 0 axiom). The local physics target is neutron-star tidal deformability: nuclear-structure values sit near $\Lambda_T \sim 500$–$1000$, while RS predicts a pure $\varphi$-power $\Lambda_T = \varphi^k$ with $\varphi^{13} \approx 521$, hence consistency at the $\varphi^{13}$ rung.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The only upstream lemma used here is the tight lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is the module-level real scale built from $\varphi$; sibling facts also record nonnegativity of the domain cost and the tidal-deformability certificate package.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ supplied by phi_gt_onePointFive. No case split or further algebraic identity is required: positivity is immediate from that lower bound once the definition is expanded.
why it matters
Gives a proved positivity anchor for the RS gravity scale before any tidal or domain-cost comparison is run. The module frames NS tidal deformability as $\Lambda_T = \varphi^k$ with $\varphi^{13} \approx 521$ matching the empirical $500$–$1000$ band; a positive canonical threshold is the elementary positivity fact those comparisons rest on. It sits next to the domain-cost nonnegativity and the inhabited tidal-deformability certificate, and is forced ultimately by T6 ($\varphi$ as the unique self-similar fixed point). No downstream users are recorded yet; the lemma is infrastructure for later gravity certificates rather than a terminal claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.