canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as φ − 3/2 in RS-native units. Structural cost lemmas in the J-symmetry module cite this constant when comparing domain cost against a fixed positive cutoff. The body is a one-line real constant built from the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
Module RS_FDN_Structural_007 records the ratio symmetry of Recognition cost: $J(x)=J(1/x)$. The cost $J$ is the unique continuous solution forced by the Recognition Composition Law, written $J(x)=(x+x^{-1})/2-1$.
The golden ratio $\varphi$ enters as the T6 fixed point of self-similar scaling. Constants live in the RS-native system imported from Constants and Cost. Sibling definitions introduce a domain cost functional and prove it is nonnegative; the present constant supplies the numerical cutoff those comparisons use.
proof idea
Pure definition: the real is set equal to $\varphi - 3/2$. No tactics, no lemmas. Downstream positivity is handled by the sibling canonicalThreshold_pos.
why it matters
Gives a single named cutoff for structural inequalities in the J-cost symmetry package (Foundation structural module 7, zero sorry). Ties the cost side of the framework to the forced scale $\varphi$ (T6). Parent certificates in the same module package domain-cost nonnegativity against this threshold; it does not itself advance the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.