canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2 (about 0.118). It is the reference cost cutoff used when comparing domain costs in the RS Moore-law module. Anyone working the Moore-law certificate or nonnegativity of domain cost would cite it. The body is a one-line arithmetic definition in the golden ratio.
Claim. Define the canonical threshold by $\mathrm{canonicalThreshold} := \varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the RS cost calculus).
background
The module recasts Moore's law in Recognition Science units. Classical Moore doubling (every 1.5–2 years) is replaced by a φ-law: transistor count grows as $\varphi^{2t}$ with $t$ in years, so annual growth is $\varphi^2 \approx 2.618$ rather than 2. The natural time unit is $1/\varphi$ φ-years.
The golden ratio $\varphi$ is the forced self-similar fixed point of the J-cost (forcing chain T6). Here it enters only as a numeric constant from Constants. The threshold $\varphi - 3/2$ sits just above zero and is the scale against which domain costs are compared when stating the structural Moore-law certificate.
Sibling facts in the same file establish that the domain cost is nonnegative and that this threshold is strictly positive, so the cutoff is a usable positive real in the certificate.
proof idea
Pure definition: the real is set equal to $\varphi - 3/2$ by abbreviation. No lemmas, tactics, or proof obligations.
why it matters
Gives the numeric cutoff that the RS Moore-law certificate and domain-cost comparisons hang on. The parent structural claim of the module is that transistor growth follows $\varphi^{2t}$ with doubling time $1/\varphi$, status STRUCTURAL THEOREM (0 sorry, 0 axiom). The constant is φ-native, so it sits downstream of T6 (φ forced as self-similar fixed point) without needing the full forcing chain T0–T8 or the RCL identity. It does not itself prove the growth law; it only names the threshold those later certificates use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.