canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as the real number φ − 3/2, with φ the golden-ratio fixed point of Recognition Science. Anyone citing the RS GUT-scale structural package (M_GUT ∼ M_Z φ^{74.5}) uses this constant as the comparison level for domain cost. The body is a one-line definitional abbreviation, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio self-similar fixed point.
background
The module treats the grand-unification scale in Recognition Science units. Experimentally $M_{\mathrm{GUT}}\sim 2\times 10^{16},\mathrm{GeV}$; relative to $M_Z\approx 91.2,\mathrm{GeV}$ the RS mass ladder gives a rung $\log(2.2\times 10^{14})/\log\varphi\approx 74.5$, so $M_{\mathrm{GUT}}=M_Z,\varphi^{74.5}$. The module is marked structural (zero sorry, zero axiom).
The constant $\varphi$ is imported from Constants and is the unique self-similar fixed point forced by the T6 step of the unified forcing chain. Domain cost (a non-negative functional built from the J-cost) is compared against a fixed real threshold; that threshold is named here.
proof idea
Bare definitional abbreviation: the identifier is bound to the real expression $\varphi-3/2$. No lemmas, tactics, or proof obligations.
why it matters
Supplies the numeric cut used by the GUT-scale certificate in the same module (siblings canonicalThreshold_pos, domainCost_nonneg, GUT_Scale_RS_v3Cert). In the RS ladder picture the threshold sits just below the Berry creation scale $\varphi^{-1}$ and well below the eight-tick and $D=3$ structural layers; it is the comparison value against which domain cost is judged when certifying the structural GUT claim $M_{\mathrm{GUT}}=M_Z,\varphi^{74.5}$. It does not itself force the rung 74.5; that comes from the logarithmic conversion of the experimental ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.