canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, with φ the self-similar fixed point of Recognition Science. Cosmology and structural-certificate authors cite it as the numeric cut used beside domain-cost comparisons in this module. The body is a one-line constant assignment from the Constants import; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the unique self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$.
background
Module RS_COS_Structural_006 packages structural facts around RS φ-uniqueness: φ is forced as the continued-fraction fixed point φ = 1 + 1/(1+1/(1+⋯)), matching forcing-chain step T6. The module imports Constants (for φ) and Cost (for the J-cost and related domain-cost machinery used by sibling declarations).
Sibling names indicate the local pattern: a nonnegative domain cost, equality lemmas for that cost, this threshold, a positivity lemma for the threshold, and a structural certificate bundle. The threshold is the bare numeric cut those comparisons will use; it is not itself a cost functional.
proof idea
Pure definition: the real constant is assigned by the closed form φ − 3/2. No tactics, no lemmas, no reduction. Downstream positivity or comparison proofs (e.g. the sibling that asserts the threshold is positive) discharge any arithmetic obligations separately.
why it matters
Gives a single named cut, built from the forced φ of T6, for structural cosmology certificates in this module. The certificate siblings (RSCOSStructural006Cert, cert, cert_inhabited) and domain-cost comparisons are the natural consumers. Numerically φ − 3/2 ≈ 0.118 lies well below the Berry creation scale φ⁻¹ and the dream fraction φ⁻³ from the RS primer, so it functions as a mild positive gate rather than a dynamical threshold. No open sorry is closed here; the declaration is scaffolding-free infrastructure for the zero-sorry structural theorem status claimed by the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.