canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden ratio fixed by φ² = φ + 1. It lives in the Foundation phi-square identity module as a named scale for cost and certificate comparisons. Anyone bounding domain costs or positivity against an RS-native cutoff would cite it. The declaration is a one-line definitional assignment, not a theorem.
Claim. Define the canonical threshold as the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (unique positive solution of $x^2 = x + 1$).
background
The module RS Phi Square Identity records the structural fact $\varphi^2 = \varphi + 1$, the defining algebraic property of the golden ratio in Recognition Science. From it one gets the Fibonacci recurrence $\varphi^n = \varphi^{n-1} + \varphi^{n-2}$ for all $n$, read as the recognition recursion identity. Status is structural: zero sorry, zero axiom.
$\varphi$ itself is the self-similar fixed point forced at T6 in the unified forcing chain. The file imports Mathlib together with RS Constants and Cost, so $\varphi$ and the J-cost infrastructure are already in scope. Sibling names in the module include domainCost, a nonnegativity lemma for that cost, a positivity lemma for this threshold, and a certificate bundle PhiSqIdentCert.
proof idea
Definitional one-liner: the real constant is set equal to phi - 3/2. No tactics, no lemmas, no proof obligations.
why it matters
Names a concrete RS scale built from $\varphi$ so later positivity and certificate statements can refer to a single symbol rather than an inline expression. The module's main content is the phi-square identity and its Fibonacci consequences; this constant sits beside domainCost and the certificate constructors that package those facts. Framework landmark: T6 (phi forced as self-similar fixed point). It does not itself close an open question; it is scaffolding-free infrastructure for the structural theorem package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.