canonicalThreshold
plain-language theorem explainer
Defines the real number φ − 3/2 as the canonical threshold used in the RS golden-angle development. Anyone checking domain-cost bounds or the GoldenAngleCert certificate cites this constant. The body is a one-line arithmetic definition in terms of the forced golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio.
background
The module treats the golden angle $\theta_G = 2\pi(1 - 1/\varphi) = 2\pi,\varphi^{-2}$ as an RS structural object (phyllotaxis angle, about 137.508°). Recognition Science forces $\varphi$ as the unique self-similar fixed point (T6) of the cost geometry built from the J-cost $J(x) = (x + x^{-1})/2 - 1$.
Sibling definitions introduce a domain cost on the relevant interval and a positivity lemma for this threshold. The constant $\varphi - 3/2$ sits just above zero ($\varphi \approx 1.618$), so it is a natural positive cutoff against which domain-cost values can be compared when certifying the golden-angle identity.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression $\varphi - 3/2$. No proof obligations; downstream lemmas (e.g. positivity) discharge properties of this value.
why it matters
Supplies the numerical cutoff that the golden-angle certificate and domain-cost comparisons rely on inside Foundation.GoldenAngle_RS. The module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and ties the classical golden angle $\theta_G = 2\pi\varphi^{-2}$ to the RS-forced $\varphi$ from the T0–T8 forcing chain. Without a named positive threshold, the cost-side inequalities that underwrite the certificate would be ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.