canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as the real number φ − 3/2, with φ the RS self-similar fixed point. Cited in the electron-mass-from-phi-ladder module as the comparison scale against which domain cost is measured. Pure definitional binding; no proof content.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of Recognition Science.
background
This module derives the electron rest mass from the RS phi-ladder. The stated structural claim is $m_e = E_{\mathrm{coh}},\varphi^3$, numerically $0.121\times 4.236 \approx 0.512,\mathrm{MeV}$ against the observed $0.511,\mathrm{MeV}$.
The constant $\varphi$ is the unique self-similar fixed point forced at T6 of the Unified Forcing Chain. Masses sit on the discrete phi-ladder with yardstick scaling $\mathrm{yardstick}\cdot\varphi^{rung-8+\mathrm{gap}(Z)}$. The threshold $\varphi-3/2$ is the local comparison value used when testing domain cost against a fixed positive cut.
Sibling definitions in the same file introduce a domain cost functional and prove it is nonnegative and equals a concrete expression at evaluation points; positivity of this threshold is recorded separately.
proof idea
Definitional abbreviation only: bind the real constant to $\varphi - 3/2$. No tactics, no lemmas, no proof term beyond the right-hand side.
why it matters
Supplies the numerical cut used inside the electron-mass certificate path of ElectronMass3_FromPhiLadder. The module aims at a structural (0-sorry, 0-axiom) match $m_e \approx E_{\mathrm{coh}},\varphi^3$ on the phi-ladder, consistent with the RS mass formula and the T6 forcing of $\varphi$. Downstream certificate inhabitants in the same file rely on a positive threshold when comparing domain cost; this definition is the named scale those comparisons use. It does not itself close the mass derivation; it only names the cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.