canonicalThreshold_pos
plain-language theorem explainer
The canonical materials threshold is a strictly positive real. Materials certificates and domain-cost lemmas cite it to keep φ-ladder comparisons on the positive side. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical materials threshold $\tau$ (the real constant named in this module and built from the golden ratio $\varphi$) satisfies $0 < \tau$.
background
This module is Materials RS Module 1. It records a structural match for steel Young's modulus: $\varphi^{25}$ MPa equals $196000$ MPa ($196$ GPa), near the experimental $\sim 200$ GPa band, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced in the Recognition chain (T6). Upstream, phi_gt_onePointFive gives the tight numerical bound $1.5 < \varphi$, proved from $\sqrt{5} > 2$. The canonical threshold is the module's named real constant built from $\varphi$; sibling lemmas treat domain cost nonnegativity and equality-at-evaluation for the same materials setting.
Imports are Mathlib, Constants, and Cost, so the local language is ordinary real arithmetic on RS constants rather than a new cost calculus.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $1.5 < \varphi$ from phi_gt_onePointFive. No case split and no further Recognition lemmas: positivity is pure real arithmetic once the definition is expanded.
why it matters
Keeps the materials module's threshold on the positive side of the $\varphi$-ladder so domain-cost and certificate constructions (siblings such as domain-cost nonnegativity and the RSMatl001 certificate) can quote a proved positivity fact rather than an ad-hoc inequality. The module itself targets the steel Young's modulus match $\varphi^{25},\mathrm{MPa}\approx 196,\mathrm{GPa}$. No downstream used_by edges are recorded yet; the lemma is local scaffolding closure for Module 1's structural certificate. Framework landmarks in play are T6 ($\varphi$ forced) and the $\varphi$-ladder mass/yardstick arithmetic used across materials claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.