canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the magnetar-field module is strictly positive. Anyone discharging nonnegativity side-conditions for the RS magnetar scaling (φ^{72} Gauss) cites this lemma. Proof is a one-line unfold-plus-linarith wrapper on the bound φ > 1.5.
Claim. The canonical threshold of the magnetar module is strictly positive: $0 < T_{\mathrm{can}}$.
background
RS Astrophysics Module 11 is a structural certificate for the magnetar surface field, stated as $\varphi^{72}$ Gauss $\sim 10^{14}$ Gauss, with zero sorry and zero axioms. The module introduces a domain cost (built from the RS $J$-cost) and a canonical threshold constant expressed in terms of the golden ratio $\varphi=(1+\sqrt{5})/2$.
The only upstream fact required is the tight lower bound $\varphi>1.5$, proved from $\sqrt{5}>2$ so that $(1+\sqrt{5})/2>3/2$. That bound is enough, after unfolding the threshold definition, to obtain strict positivity by linear arithmetic.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single lemma $\varphi>1.5$. No further case splits or cost identities are needed.
why it matters
Positivity of the canonical threshold is a side-condition lemma inside the structural magnetar certificate (Module 11). It sits on the $\varphi$-ladder forced at T6 of the unified forcing chain and keeps the module in the zero-sorry structural layer. No downstream theorems currently depend on it; it is available for any later nonnegativity or comparison argument that mentions the same threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.