canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the canonical threshold in RS physics units. Anyone citing Module 5 thresholds, domain-cost comparisons, or the QCD count-law package would reference it. The body is a one-line arithmetic definition from the golden fixed point.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the self-similar fixed point of the Recognition forcing chain.
background
Module 5 packages the structural claim that the one-loop QCD coefficient satisfies $b_0 = 7 = 2^D - 1$, forced by the count law once spatial dimension is fixed at $D = 3$ (forcing step T8). Status is a structural theorem with no sorry and no axioms.
The constant $\varphi$ is imported from Constants and is the unique self-similar fixed point forced at T6. Cost primitives from the Cost import supply the J-cost and related nonnegativity facts used by sibling lemmas that compare domain costs against thresholds.
This declaration simply names the particular real $\varphi - 3/2$ so later positivity and certificate statements can cite a single symbol rather than an inline expression.
proof idea
No proof obligation: the declaration is a bare definition equating the symbol to the real expression $\varphi - 3/2$. Downstream lemmas (for example positivity of the threshold) discharge any analytic content.
why it matters
Gives a stable name to the numerical gate used inside the Module 5 QCD structural package. The module ties $b_0 = 7$ to the count law $2^D - 1$ at $D = 3$, so a fixed threshold expressed in $\varphi$ keeps later domain-cost and certificate statements aligned with the T6–T8 forcing landmarks. Sibling positivity and the RSPhysics005 certificate inhabit the same file; this definition is the shared numeric anchor they quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.