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 comparing domain costs to a fixed positive scale in the proton–electron mass-ratio module cites this constant. It is a one-line definition, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
Module 9 of the RS physics layer treats the proton–electron mass ratio. The structural claim is that a pure $\varphi^{12}$ ladder step yields about 321.9, leaving a residual factor near 5.7 relative to the observed 1836 that must be absorbed by cost corrections.
The constant $\varphi$ is imported from IndisputableMonolith.Constants and is the unique positive solution of the self-similarity fixed-point equation forced at T6. The Cost import supplies the J-cost and related non-negative defect measures against which a numerical threshold is compared.
Sibling declarations introduce a domain cost functional and prove it is non-negative; the present definition simply names the comparison scale used by those statements and by the module certificate.
proof idea
Pure definitional abbreviation: the real constant is introduced by the single equation $\varphi - 3/2$. No lemmas are applied and no tactics run.
why it matters
Gives a named, reusable scale for the structural certificate of Module 9 (proton–electron mass ratio). Downstream siblings such as positivity of the threshold and the inhabited certificate package rely on this exact real so that cost-versus-threshold comparisons stay uniform across the module.
In the broader RS chain the number sits downstream of T6 ($\varphi$ forced) and is used only as a fixed positive cutoff; it does not itself encode the eight-tick octave, spatial dimension, or the fine-structure band. It keeps the residual mass-ratio gap discussion numerically concrete without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.