canonicalThreshold
plain-language theorem explainer
The canonical cosmic-string threshold is the real number φ − 3/2, identical to the J-cost evaluated at the golden ratio. Cosmologists bounding RS string tension cite it as the dimensionless prefactor in Gμ = J(φ)(v/M_Pl)². The declaration is a one-line arithmetic definition in the RS constant φ.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point forced by Recognition self-similarity.
background
The module derives a structural bound on cosmic-string tension from the Recognition J-cost. In RS-native units the string-tension parameter takes the form $G\mu = J(\varphi),(v/M_{\mathrm{Pl}})^2$, and the numerical prefactor is quoted as about 0.118.
The cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The constant $\varphi$ is the unique self-similar fixed point of the forcing chain (T6). Because $\varphi$ satisfies $\varphi=1+1/\varphi$, a short algebra yields $J(\varphi)=\varphi-3/2$.
Thus the present definition simply names that value as the canonical threshold used throughout the cosmic-string certificate.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression $\varphi-3/2$. No lemma application or tactic proof is required. Downstream positivity and certificate lemmas consume the name directly.
why it matters
Inside the CosmicStrings4 development this constant is the RS-native prefactor that converts a symmetry-breaking scale $v$ into a predicted $G\mu$. The module status note records $G\mu\approx 8\times 10^{-6}$ at $v=10^{16},\mathrm{GeV}$, marginally excluded by present limits $G\mu<10^{-7}$.
The identification $J(\varphi)=\varphi-3/2$ ties the cosmology bound to the T5/T6 forcing landmarks (J-uniqueness and $\varphi$ as self-similar fixed point) and to the Recognition Composition Law that forces the shape of $J$. Sibling lemmas (positivity of the threshold, the inhabited CosmicStrings4 certificate) build on this single real.
It therefore sits at the junction of the abstract cost calculus and a concrete observational window on high-scale string networks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.