canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the module’s canonical numerical threshold. Physicists working the tree-level Weinberg angle in RS Module 4 cite it when comparing domain costs or positivity bounds against a fixed RS scale. The body is a one-line abbreviation in terms of the golden ratio from Constants.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of the Recognition self-similarity relation.
background
RS Physics Module 4 treats the tree-level Weinberg angle via the closed form $\sin^2\theta_W = J(\varphi)/(1+J(\varphi)) \approx 0.1054$, with a loop-corrected target near $0.231$. The module is marked structural (zero sorry, zero axiom).
Here $\varphi$ is the unique self-similar fixed point forced at T6 of the unified forcing chain, and $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$ from T5 / the Recognition Composition Law. Sibling definitions in the file introduce a nonnegative domain cost and a positivity lemma for this same threshold, so the constant is the comparison scale those lemmas use.
proof idea
Pure definition: the real is bound to the arithmetic expression $\varphi - 3/2$. No proof obligations, tactics, or upstream lemmas are involved.
why it matters
Gives Module 4 a single named RS-native cutoff built from $\varphi$ rather than an ad-hoc float. Downstream siblings (positivity of the threshold, the module certificate RSPhysics004Cert) hang off this value when they assert that domain costs sit above or below the cutoff. It sits in the same constants layer as $c=1$, $\hbar=\varphi^{-5}$, and the $\varphi$-ladder mass formula, and supports the structural claim that the tree-level Weinberg angle is forced rather than fitted. No open scaffold is attached; the declaration is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.