canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the canonical threshold used in the RS physics module on the EM fine-structure band. Anyone citing domain-cost comparisons or the structural alpha certificate in this file will pull this value. The body is a one-line abbreviation of that arithmetic expression in RS-native units.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point forced by self-similarity.
background
This module packages the Recognition Science structural claim that the inverse fine-structure constant lies in the open interval $(137.030, 137.039)$, with the CODATA value $137.036$ inside, and records an RS_PASS structural theorem (no sorry, no axioms).
The constant $\varphi$ is the unique self-similar fixed point forced at step T6 of the unified forcing chain; in RS-native units it is the base of the mass ladder and the scale that organizes dimensionless thresholds. Sibling definitions in the same file introduce a nonnegative domain cost and prove that this threshold is strictly positive, so the present abbreviation is the numeric cut those lemmas compare against.
No external lemmas are required: the definition only names the combination $\varphi - 3/2$ once, for reuse by the certificate and positivity facts in the module.
proof idea
Pure definitional abbreviation. The right-hand side is the real arithmetic expression $\varphi - 3/2$ drawn from the Constants import; there is no proof body, no tactic, and no lemma application.
why it matters
Gives a single named cut for domain-cost comparisons inside the EM fine-structure module. The module doc frames the whole file as the structural theorem that $\alpha^{-1}$ sits in $(137.030, 137.039)$ with CODATA inside; this threshold is the local numeric anchor those cost and certificate declarations use. It sits downstream of T6 ($\varphi$ forced) and upstream of the inhabited certificate RSPhysics002Cert / cert siblings. It does not itself prove the alpha band; it only standardizes the cut those proofs reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.