canonicalThreshold
plain-language theorem explainer
Canonical threshold is the real number φ − 3/2, with φ the RS golden ratio. Neutron-star work in this module uses it as a fixed structural cutoff beside the domain cost. The declaration is a one-line arithmetic definition in the RS constant φ; no proof is required.
Claim. Define the canonical threshold by $T := \varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of Recognition Science.
background
Recognition Science forces a unique dimensionless scale φ via self-similarity (forcing step T6): φ = (1+√5)/2 satisfies φ = 1 + 1/φ. Constants and the J-cost live in the imported Constants and Cost modules; J is the unique cost with J(x)=(x+x^{-1})/2−1.
This file is Astrophysics RS Module 3. Its stated target is the neutron-star radius φ^5 km ≈ 11.09 km, inside the observed 10–13 km window, recorded as a structural match with no sorry and no axioms. The threshold φ − 3/2 ≈ 0.118 is the module’s named real cutoff used with the local domain cost.
proof idea
Definition only. The real is introduced by the closed-form expression φ − 3/2; there is no tactic proof and no lemma application.
why it matters
Gives the module a single named real against which domain-cost comparisons and positivity facts are stated. Sibling results include positivity of this threshold and the certificate RSAstro003Cert that packages the module’s structural claims. In the broader RS ladder, neutron-star scales sit near Z_cf = φ^5 ∈ (11,12); the threshold is a local arithmetic anchor for that astrophysics layer, not a replacement for the mass or radius formulas themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.