canonicalThreshold
plain-language theorem explainer
Defines the canonical numerical threshold as φ − 3/2 in RS-native units. Gravity and structural-certificate authors cite it when a fixed positive cutoff built from the self-similar fixed point is needed. The body is a one-line real definition, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the continued fraction $1+1/(1+1/\cdots)$ (the golden ratio forced by Recognition Science).
background
Module 6 of the RS gravity structural series records facts tied to φ-uniqueness: φ is the self-similar fixed point φ = 1 + 1/φ, equivalently the infinite continued fraction 1+1/(1+1/⋯). The module is marked structural (zero sorry, zero axiom) and imports the global Constants and Cost layers.
In Recognition Science the same φ appears as the T6 forced fixed point of the forcing chain and as the base of the mass ladder. A simple affine shift φ − 3/2 yields a small positive real (≈ 0.118) that the sibling lemmas treat as a canonical cutoff for domain-cost comparisons in this gravity certificate.
proof idea
Pure definition: the identifier is bound to the real expression φ − 3/2. No tactic proof, no lemma application. Downstream positivity or comparison facts (e.g. the sibling that the threshold is positive) unfold this abbreviation and reason about φ > 3/2.
why it matters
Supplies the named real cutoff used by the RS gravity structural certificate in this module (siblings such as the positivity lemma and the inhabited certificate package). It ties the gravity side to the T6 landmark that forces φ as the unique self-similar fixed point, so every later comparison is expressed in the same RS-native scale rather than an ad-hoc constant. No open scaffold: the definition is closed; only its uses in larger GRV certificates remain to be assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.