canonicalThreshold_pos
plain-language theorem explainer
The canonical materials threshold is strictly positive. Materials and thermophysics arguments that normalize domain cost against this threshold cite the fact. The proof is a one-line unfold-plus-linarith wrapper from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the module's canonical threshold (an explicit real expression in the golden ratio $\varphi$).
background
Module 11 of the RS materials layer records the exact water specific-heat match $\varphi^{19}\cdot 0.447 = 4179,\mathrm{J/kg/K}$ as a structural theorem (no sorry, no axioms). The module imports the global constants and the J-cost layer, and defines a domain cost together with a canonical threshold used to normalize or gate that cost.
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The only upstream fact used here is the tighter numerical bound $\varphi>1.5$, proved from $\sqrt{5}>2$. That bound is enough to force positivity once the threshold definition is unfolded.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then close by linarith using the lemma $\varphi>1.5$. No further algebraic identities or cost lemmas are required.
why it matters
Positivity of the canonical threshold is the elementary gate that keeps domain-cost comparisons and the module certificate well-defined on the positive reals. The module status line marks the water specific-heat identity as a structural theorem; this lemma is the local positivity support for that certificate stack (siblings include domainCost_nonneg, RSMatl011Cert, and cert_inhabited). It sits downstream of the T6 forcing of $\varphi$ and the constants layer, and does not itself touch the mass ladder, RCL, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.