canonicalThreshold
plain-language theorem explainer
The canonical materials threshold is the real number φ − 3/2, with φ the golden-ratio fixed point of Recognition Science. Materials certificates cite it as the reference scale for domain-cost comparisons in the water c_p module. The declaration is a one-line real definition, not an inequality or existence proof.
Claim. Define the canonical threshold by $T_{\mathrm{can}} := \varphi - 3/2$, where $\varphi=(1+\sqrt{5})/2$ is the golden ratio.
background
Recognition Science forces $\varphi$ as the unique self-similar fixed point of the cost functional (forcing chain T6). Dimensionless RS quantities routinely sit on the $\varphi$-ladder; constants such as $\hbar=\varphi^{-5}$ and the mass rungs are built from the same base.
This file is Materials RS Module 6. Its module claim is structural: water specific heat $c_p=\varphi^{19}\cdot 0.447,\mathrm{J/kg/K}$ equals $4179$ against the experimental $4179.6$ (relative error $0.01%$), with zero sorry and zero axioms. The threshold $\varphi-3/2\approx 0.118$ is the numeric cutoff against which domain costs in the module are compared.
Sibling declarations include a nonnegativity lemma for the domain cost and a positivity lemma for this same threshold; the certificate RSMatl006Cert packages the module-level claim.
proof idea
Definitional only. The real constant is set equal to phi - 3/2 by a one-line abbreviation; there is no tactic proof and no lemma application.
why it matters
Gives the materials layer a single named real that later positivity and certificate lemmas can invoke without re-expanding $\varphi-3/2$. It ties the water $c_p$ structural theorem to the same $\varphi$ that appears in the mass ladder, the eight-tick octave (T7), and the $\alpha$ band. Downstream siblings such as the positivity fact for this threshold and the inhabited materials certificate rely on the name existing as a first-class constant. The definition itself does not prove the heat-capacity match; that match is the surrounding module theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.