canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the canonical threshold in the RS rung-spacing module. Anyone working domain-cost comparisons or positivity lemmas on consecutive φ-rungs cites it. The body is a pure definitional abbreviation of that arithmetic combination of the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
Module 11 treats RS rung spacing: consecutive rungs on the φ-ladder differ by the multiplicative factor φ ≈ 1.618. The golden ratio φ is the unique positive fixed point forced at T6 of the unified forcing chain; costs and thresholds in this module are expressed in that native scale.
The Cost import supplies the J-cost and related nonnegativity infrastructure. Sibling declarations introduce a domain cost functional and prove it is nonnegative; the present constant is the numerical cut used against that cost. No external lemma is required to name the value: it is simply φ minus three halves.
proof idea
Definitional. The declaration binds the real identifier to the closed-form expression φ − 3/2; there is no proof body, tactic block, or lemma application.
why it matters
Gives a single named real for the threshold that later positivity and certificate lemmas in the same module (canonicalThreshold_pos, the RSForcingChain011Cert bundle) refer to. In the broader framework it sits inside the φ-ladder bookkeeping that supports mass rungs and spacing arguments after T6 (φ forced) and the eight-tick octave. It does not itself force a physical constant; it standardizes the cut used by the structural theorems of this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.