canonicalThreshold
plain-language theorem explainer
The real constant φ − 3/2 is fixed as the canonical cost threshold for the hydrogen-spectrum-from-J module. Anyone matching Balmer-line ratios to the φ-ladder against a J-cost floor cites this value. It is a one-line arithmetic definition in terms of 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 hydrogen Balmer emission structure from the Recognition Science φ-ladder and the J-cost. Module status is a structural theorem with no sorry and no axioms. The classical Balmer lines (Hα 656 nm, Hβ 486 nm, Hγ 434 nm) enter via the observed ratio Hα/Hβ = 656/486 ≈ 1.35, which RS identifies with a φ^0.8 spacing of adjacent Balmer wavelengths.
J-cost is the unique cost functional forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$. The golden ratio φ is the self-similar fixed point of the forcing chain (T6). Sibling definitions in the file introduce a domain cost on the relevant interval and prove it is nonnegative; the present constant supplies the numerical floor those comparisons use.
proof idea
Pure definition: the real is bound to the closed term phi - 3/2 from the Constants import. No proof obligations, tactics, or lemmas.
why it matters
Gives a single named real that later certificates in the same module (nonnegativity of domain cost, the HydrogenSpect3Cert bundle) can compare against when linking Balmer ratios to J-cost on the φ-ladder. It sits in the Foundation layer that turns the forcing-chain landmarks (J-uniqueness, φ fixed point) into concrete spectroscopic numerics. The module frames the Balmer φ^0.8 spacing as the physical readout; this threshold is the cost-side cut those comparisons need. No downstream edges are recorded on the page, so its role is local to the hydrogen-spectrum certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.