canonicalThreshold
plain-language theorem explainer
Defines the canonical cost threshold as φ − 3/2 ≈ 0.118. Solar-constant and domain-cost arguments in the φ-ladder module cite this fixed real as the comparison level against which nonnegative domain costs are checked. The body is a one-line real arithmetic definition from the golden ratio constant.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio.
background
The module derives the solar constant $S_0 \approx 1361,\mathrm{W/m^2}$ from the φ-ladder. In RS units the observed value sits near rung 15: $\varphi^{15} \approx 1364$, matching $S_0$ to a few parts in $10^3$. The structural identity used is $S_0 = \sigma_{\mathrm{SB}} T_{\mathrm{sun}}^4 (R_{\mathrm{sun}}/\mathrm{AU})^2$.
Domain costs are nonnegative real-valued functionals built from the J-cost $J(x) = (x+x^{-1})/2-1$ (the unique cost forced by the Recognition Composition Law). A fixed numerical threshold is needed to certify that a domain cost lies below a recognition-scale cutoff. The golden ratio $\varphi$ is the self-similar fixed point of the forcing chain (T6); subtracting $3/2$ places the cutoff just above zero and below the Berry creation scale $\varphi^{-1}$.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression $\varphi - 3/2$. No lemmas or tactics are involved. Downstream positivity is handled by the sibling canonicalThreshold_pos.
why it matters
Supplies the numerical cutoff used by solar-constant certificates in this module (siblings SolarConstantCert, cert, cert_inhabited). It anchors domain-cost comparisons on the same φ-ladder that places $S_0$ at rung 15, tying the solar-constant claim to the T5–T6 forcing landmarks (J-uniqueness and φ as fixed point). Without a named threshold the nonnegativity and certification lemmas would hard-code a magic number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.