canonicalThreshold
plain-language theorem explainer
Canonical threshold is the real constant φ − 3/2, with φ the golden-ratio fixed point of Recognition self-similarity. It is the cutoff against which domain J-cost is compared when the electron Compton length is read from the φ-ladder. Anyone working the structural Compton certificate in this module cites it. The declaration is a one-line real definition, not a theorem.
Claim. Define the canonical threshold by $T := \varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the Recognition forcing chain (the golden ratio).
background
This module derives the electron Compton wavelength as a structural φ-ladder identity: $\lambda_C/\ell_{\mathrm{Pl}}=\varphi^{97.5}$, matching the empirical $\lambda_C\approx 2426,\mathrm{fm}$ once Planck units are restored. Status is a structural theorem (no sorry, no axioms).
The cost side of the argument uses the unique J-cost $J(x)=(x+x^{-1})/2-1$ forced by T5 and the Recognition Composition Law. Domain cost is the restriction of that functional to the positive reals relevant for the ladder step. The constant $\varphi$ itself is imported from the Constants layer (T6 fixed point).
The threshold $\varphi-3/2$ sits between 0 and 1 and is the comparison value used when deciding whether a ladder defect clears the creation or identification cut for the electron rung.
proof idea
One-line definition: the name is bound to the real expression $\varphi-3/2$. No tactics, no lemmas, no proof obligations. Positivity and downstream comparisons are separate sibling declarations.
why it matters
Gives the numerical cut that the electron-Compton certificate compares against when it reads $\lambda_C$ off the φ-ladder via J-cost. Siblings such as the positivity lemma and the inhabited ElectronCompton3Cert package sit on top of this constant. In the broader framework it is a local specialization of T5–T6 data (unique J, forced φ) to the Compton rung $k=97.5$, not a new forcing step. It does not itself close the mass or α bands; it only supplies the threshold those structural certificates need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.