canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, with φ the golden-ratio fixed point of the RS self-similarity equation. Structural and cost lemmas in this module cite it as the cut separating admissible domain costs from the rest of the line. The body is a one-line constant abbreviation; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the unique positive self-similar fixed point of the Recognition Science recurrence (the golden ratio).
background
Module RS_MTH_Structural_006 packages the structural uniqueness of φ as the continued-fraction fixed point φ = 1 + 1/(1 + 1/(1 + ⋯)). Status is a closed structural theorem block (zero sorry, zero axioms).
The constant φ is imported from IndisputableMonolith.Constants; cost primitives come from IndisputableMonolith.Cost. Sibling definitions introduce a domain cost functional on the reals and record its non-negativity and evaluation identities. The present abbreviation supplies the numerical cut those cost statements compare against.
In the broader forcing chain, φ is forced at T6 as the unique self-similar scale; thresholds built from φ therefore inherit that uniqueness rather than being free parameters.
proof idea
Pure definitional abbreviation: the real constant is set equal to phi - 3/2. No tactics, no lemmas, no unfolding obligations beyond the imported value of φ.
why it matters
Gives a single named real that later positivity and certification lemmas (canonicalThreshold_pos, RSMTHStructural006Cert) can quote without repeating the arithmetic. Ties the cost cut directly to the T6 fixed point rather than to an ad-hoc decimal. Downstream certificates in the same module use the name to assert that the structural package is inhabited and that the threshold lies strictly above zero, keeping the φ-ladder and domain-cost comparisons inside the closed structural layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.