canonicalThreshold_pos
plain-language theorem explainer
The canonical chemistry threshold is a strictly positive real. Structural chemistry arguments that gate domain costs or Debye-scale comparisons against this threshold cite the fact. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold constant of the module is strictly positive: $0 < \tau$, where $\tau$ is defined from the golden ratio $\varphi$.
background
Chemistry RS Module 8 records structural identities linking copper's Debye temperature to a pure power of the golden ratio ($\varphi^{12} \approx 321.9,\mathrm{K}$ versus the experimental $343,\mathrm{K}$). The module is marked structural: zero sorry, zero axioms.
The constant $\varphi = (1+\sqrt{5})/2$ is the unique self-similar fixed point forced by the Recognition Composition Law (T6). A tighter elementary bound already available in Constants is $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is the real gate used by the module's domain-cost predicates; its positivity is the minimal arithmetic fact needed before any comparison or certificate can fire.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (an expression built from $\varphi$), then invoke linarith on the single upstream lemma $\varphi > 1.5$. No case splits or further Recognition identities are required.
why it matters
Supplies the positivity gate for every subsequent inequality in RS_Chem_Module_008 (domain-cost non-negativity, the module certificate RSChem008Cert). The module itself is a structural check that Debye scales sit on the $\varphi$-ladder, consistent with the mass/energy yardstick of Recognition Science. No downstream theorems yet list this lemma, but the inhabited certificate in the same file is the natural consumer. It does not touch the forcing chain T0–T8 directly; it only re-uses the elementary lower bound on $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.