canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as φ − 3/2 in RS-native units. Anyone deriving the fine-structure interval α⁻¹ ∈ (137.030, 137.039) from Recognition Science cites this constant as the cutoff against which domain cost is compared. The body is a one-line real arithmetic definition from the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique positive self-similar fixed point forced by the Recognition Composition Law.
background
The module derives a tight open interval for the inverse fine-structure constant α⁻¹ from Recognition Science alone, targeting the band (137.030, 137.039) already certified elsewhere in the monolith. All quantities sit in RS-native units (c = 1, ħ = φ⁻⁵, G = φ⁵/π).
φ itself is the unique positive solution of the self-similarity fixed-point equation forced at step T6 of the unified forcing chain; numerically φ = (1+√5)/2. The cost functional J(x) = (x + x⁻¹)/2 − 1 (equivalently cosh(log x) − 1) is the unique continuous solution of the Recognition Composition Law, and domain cost is built from it. The present constant is the numerical gate that separates admissible from inadmissible cost values in that derivation.
proof idea
Pure definition: the real is introduced by the arithmetic expression φ − 3/2. No lemmas, no tactics, no proof obligations.
why it matters
Supplies the numerical cutoff used by the fine-structure certification path in this module (siblings such as domainCost, canonicalThreshold_pos, and FineStructure2Cert). The parent goal is the structural theorem that α⁻¹ lies in (137.030, 137.039) with zero sorry and zero axioms. The value φ − 3/2 is the natural scale that appears once the eight-tick octave and the φ-ladder mass formula are fixed; it therefore sits downstream of T5–T7 in the forcing chain and upstream of the electromagnetic α certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.