canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as the golden-ratio offset φ − 3/2 used in the pulsar-period astrophysics module. Anyone citing RS structural bounds on typical versus millisecond pulsar timescales will pull this constant. The body is a one-line definitional binding to φ from Constants; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (the self-similar fixed point of the Recognition forcing chain).
background
Module RS_Astro_Module_010 packages structural statements about pulsar periods in Recognition Science units. The module doc fixes the characteristic scales: a typical period near $\varphi^{-1},\mathrm{s}\approx 0.618,\mathrm{s}$ and a millisecond band near $\varphi^{-10},\mathrm{s}\approx 8.1,\mathrm{ms}$, treated as a RANGE claim with zero sorry and zero axioms.
The constant $\varphi$ is imported from IndisputableMonolith.Constants; it is the unique positive solution of $x=1+1/x$ forced at T6 of the unified forcing chain. The Cost import supplies the J-cost infrastructure used by sibling definitions such as domainCost, but this declaration itself only names a real threshold built from $\varphi$.
Sibling facts (domainCost_nonneg, canonicalThreshold_pos, RSAstro010Cert) turn the threshold into a nonnegative cost comparison and a certificate inhabitation check for the module.
proof idea
Pure definition: the real is bound to the closed-form expression $\varphi-3/2$. No tactics, no lemmas, no reduction steps. Downstream positivity or cost comparisons are separate declarations.
why it matters
Gives the module a single named real against which pulsar-period domain costs can be compared, keeping the structural certificate RSAstro010Cert free of magic numbers. In the broader RS framework it sits on the $\varphi$-ladder already fixed by T6 (self-similar fixed point) and is consistent with the eight-tick and dimensional forcing that set the units in which periods are measured. It does not itself close a forcing-chain step; it is scaffolding for the astrophysics RANGE claim that typical and millisecond pulsars sit at definite negative powers of $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.