canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the canonical comparison threshold in the RS forcing-chain calibration module. Anyone comparing domain cost against a fixed cutoff, or proving that cutoff is positive, cites this name. The body is a one-line abbreviation of that arithmetic expression in terms of the golden-ratio constant.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the Recognition cost (the golden ratio).
background
Module 10 of the RS forcing chain treats calibration: $E_{\mathrm{coh}}$ is the single free energy scale, fixed by placing the electron on rung 3 of the $\varphi$-ladder. The module is marked structural (zero sorry, zero axiom).
The constant $\varphi$ is imported from Constants and is the T6 fixed point of the Recognition Composition Law cost $J$. Sibling definitions introduce a domain cost functional and prove it is nonnegative; this threshold is the fixed real against which that cost is compared in the same file.
No separate doc-comment sits on the definition; its meaning is the arithmetic cut $\varphi - 3/2 \approx 0.118$ in RS-native units.
proof idea
Bare definition: the identifier is bound to the real expression $\varphi - 3/2$. There is no proof body, no tactic, and no lemma application. Downstream positivity is handled by the sibling canonicalThreshold_pos, not here.
why it matters
Gives a single named real for the cutoff used in domain-cost comparisons inside the forcing-chain calibration layer. The parent module ties $E_{\mathrm{coh}}$ to the electron at rung 3; this threshold is the structural constant that sits beside that calibration rather than a derived mass or coupling.
It sits downstream of T6 ($\varphi$ forced) and upstream of any certificate that asserts the threshold is positive or that a domain cost clears it (RSForcingChain010Cert and related cert inhabitants in the same file). It does not itself invoke T5–T8, RCL identities, or the eight-tick octave; it only packages the arithmetic cut those later arguments may need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.