canonicalThreshold_pos
plain-language theorem explainer
The canonical cosmic-string threshold built from the golden ratio is strictly positive. Cosmologists citing the RS string-tension formula Gμ = J(φ)(v/M_Pl)² need this to know the prefactor cannot vanish or flip sign. Proof is a one-line unfold of the threshold definition followed by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the RS-native string-tension prefactor obtained by evaluating the J-cost at $\varphi$) is strictly positive: $0 < T_{\mathrm{can}}$.
background
The module derives a cosmic-string network bound from the Recognition Science J-cost. The cost is $J(x) = (x + x^{-1})/2 - 1$; at the golden ratio it collapses to $J(\varphi) = \varphi - 3/2 \approx 0.118$, which multiplies $(v/M_{\mathrm{Pl}})^2$ to give the dimensionless string tension $G\mu$.
The canonical threshold is that prefactor (or an equivalent expression in $\varphi$) used as the structural constant in the $G\mu$ estimate. Module status is a structural theorem with zero sorry and zero axioms; the numerical story is that at $v = 10^{16},\mathrm{GeV}$ one obtains $G\mu \sim 8\times 10^{-6}$, marginally excluded by the observational ceiling $G\mu < 10^{-7}$.
Upstream, the lemma $\varphi > 1.5$ records the elementary bound $(1+\sqrt{5})/2 > 3/2$, which is exactly the inequality needed once the threshold is unfolded into an affine expression in $\varphi$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (exposing an expression linear in $\varphi$, typically $\varphi - 3/2$ or an equivalent form of $J(\varphi)$). Discharge the resulting strict inequality by linarith against the imported lemma $\varphi > 1.5$.
why it matters
Positivity of the threshold is the first arithmetic fact the CosmicStrings4 certificate needs before it can treat $G\mu = J(\varphi),(v/M_{\mathrm{Pl}})^2$ as a genuine positive scale. It sits in the cosmology layer that connects the forcing-chain cost $J$ (T5 J-uniqueness) and the self-similar fixed point $\varphi$ (T6) to an observational string-tension bound.
No external used-by edges are recorded; within the module it underwrites the certificate bundle (CosmicStrings4Cert, cert, cert_inhabited) and the nonnegativity story already present for the domain cost. The numerical comparison with $G\mu < 10^{-7}$ remains a consistency check, not a derived theorem here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.