canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as φ − 3/2, with φ the golden ratio fixed by recognition recursion. Foundation work on the RS forcing chain and domain-cost comparisons cites this constant as the reference scale separating admissible from inadmissible cost regimes. The body is a one-line real abbreviation; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi = (1+\sqrt{5})/2$ is the unique self-similar fixed point of recognition recursion.
background
Module 8 of the RS forcing chain records structural facts about φ-uniqueness: φ = (1+√5)/2 is the unique fixed point of the recognition recursion, with status STRUCTURAL THEOREM (0 sorry, 0 axiom). The module imports the global Constants and Cost layers, so φ is the same constant forced earlier in the chain (T6) and used by the J-cost.
Sibling definitions introduce a domain cost and prove it is nonnegative and agrees with evaluation at a point. The canonical threshold sits beside those facts as the numerical cutoff against which domain costs are compared. In RS units the same φ appears in the mass ladder, the eight-tick octave, and the fine-structure band; here it only supplies the offset 3/2 that yields a small positive scale (~0.118).
proof idea
Pure definitional abbreviation: the real constant is declared equal to φ minus three-halves. No tactics, no lemmas, no unfolding obligations beyond the imported name φ from Constants.
why it matters
Supplies the reference scale used by the surrounding Module-8 certificate (RSForcingChain008Cert and the inhabited cert). Downstream positivity facts such as canonicalThreshold_pos rest on this value being strictly positive, which follows at once from φ > 3/2. In the broader forcing chain the same φ is the T6 self-similar fixed point; the offset 3/2 converts that fixed point into a concrete cost threshold for domain comparisons, keeping the structural layer free of free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.