canonicalThreshold
plain-language theorem explainer
The canonical threshold is the fixed real number φ − 3/2 used as a cost cut in the RS structural account of MSSM/SUSY breaking. Anyone working the M_SUSY ∼ φ^k M_Z ladder (k ≈ 10.7, M_SUSY ∼ 11 TeV) cites it as the named scale offset. It is a one-line definition in terms of the golden-ratio constant, not a derived inequality.
Claim. Define the canonical threshold as the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of Recognition self-similarity.
background
This module packages a structural (0-sorry) RS treatment of MSSM/SUSY breaking. The physical claim is that the SUSY-breaking scale sits on the φ-ladder relative to the Z mass: M_SUSY = M_Z · φ^k with φ^k ≈ 110 (near φ^10), hence M_SUSY ∼ 11 TeV in the 1–10 TeV window.
φ itself is the unique self-similar fixed point forced by the Recognition Composition Law and the J-cost uniqueness step (T5–T6 in the forcing chain). The module imports the global Constants and Cost layers, so φ and the J-cost are already available; the local objects are domain costs and a named threshold against which those costs are compared.
Sibling facts establish nonnegativity of the domain cost and positivity of this threshold; the present declaration only names the cut.
proof idea
Pure definition: the identifier is bound to the real expression φ − 3/2. No tactics, no lemmas, no proof obligations.
why it matters
Gives a single named real cut for the RS MSSM-breaking certificate (siblings cert / MSSM_Breaking_RS_v3Cert). Downstream positivity and cost comparisons need a concrete offset rather than an ad-hoc numeral; φ − 3/2 is that offset, sitting just below the Berry-scale neighborhood of φ^−1 while remaining positive.
It does not itself force the rung k ≈ 10.7 or the TeV window; those come from matching M_SUSY/M_Z to the φ-ladder in the module narrative. Within the forcing chain it is scaffolding for the structural SUSY-scale claim, not a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.