canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the J-cost heat-capacity anomaly is strictly positive. Anyone assembling the RS certificate for the specific-heat exponent α = J(φ)/2 needs this sign fact. The proof is a one-line unfold followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold used for the J-cost heat-capacity anomaly is strictly positive: $0 < t_{\mathrm{can}}$.
background
The module treats the critical specific-heat anomaly $C_p \propto |T-T_c|^{-\alpha}$ in Recognition Science. RS places the exponent between mean-field ($\alpha=0$) and 3D Ising ($\alpha\approx 0.110$) by taking $\alpha=J(\varphi)/2\approx 0.059$, where $J$ is the unique cost functional forced by the Recognition Composition Law and $\varphi$ is the golden ratio.
The golden ratio satisfies the tighter numerical bound $\varphi>1.5$ (lemma phi_gt_onePointFive), which follows at once from $\sqrt{5}>2$. Because $J(\varphi)=(\varphi+\varphi^{-1})/2-1$ collapses algebraically to $\varphi-3/2$, positivity of any threshold built from that difference is immediate once the bound is in hand.
Local setting: a structural (zero-sorry) certificate module that packages the RS prediction for the heat-capacity exponent without external axioms.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith using the upstream lemma that $\varphi>1.5$. No further rewriting or case splits are required.
why it matters
Positivity of the canonical threshold is the elementary sign fact needed before any certificate can assert that the RS heat-capacity exponent is a well-defined positive real. It sits inside the structural theorem package for the specific-heat anomaly (Plan v7, eighty-sixth pass) and underwrites the comparison of RS ($\alpha=J(\varphi)/2$) against mean-field and 3D Ising values. The same $J$-uniqueness that forces the cost functional (forcing-chain T5) and the self-similar fixed point $\varphi$ (T6) therefore reappear as the source of a concrete thermodynamic exponent. No downstream theorems currently cite it in the graph, but the sibling certificate constructors (HeatCapAnomalyCert, cert) are the natural consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.