canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2. It supplies a fixed comparison scale inside the RS Euler–phi module for domain-cost bounds. Anyone comparing golden-ratio ladder quantities to classical Euler growth cites it. The declaration is a bare real definition, not a proved inequality.
Claim. Define the canonical threshold by $\varphi - 3/2$, where $\varphi$ is the golden ratio (the self-similar fixed point of the RS forcing chain).
background
The module studies structural links between Euler's number $e$ and the golden ratio $\varphi$ in Recognition Science units. Status is structural (zero sorry, zero axiom). The module imports Mathlib, RS constants, and the J-cost layer.
Here $\varphi$ is the unique positive fixed point forced at T6 of the unified forcing chain; numerically $\varphi \approx 1.618$, so $\varphi - 3/2 \approx 0.118$. Sibling definitions introduce a domain cost and certify that this threshold is positive.
The surrounding narrative treats $e$ and $\varphi$ as transcendentally independent yet related by ladder exponents (e.g. rough comparisons $e \sim \varphi^{2.39}$). The threshold is the simple real cut used when those comparisons are made quantitative.
proof idea
Pure definition: the real is assigned by the closed-form expression $\varphi - 3/2$. No tactics, no lemmas, no proof obligations.
why it matters
Gives a named, reusable cut-point for the Euler–phi certificate stack in this module (siblings include domain-cost nonnegativity and the inhabited Euler–phi certificate). In the broader RS picture it sits next to T6 ($\varphi$ forced) and the J-cost calculus imported from Cost, without itself claiming a forcing-chain step.
It does not encode the RCL identity, the eight-tick octave, or the mass ladder; it is only the scalar threshold those later comparisons can quote. No downstream edges are recorded yet, so its role is local scaffolding for the module's structural theorem claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.