canonicalThreshold_pos
plain-language theorem explainer
The module's canonical threshold constant is strictly positive. Materials and Hall-resistance arguments that need a positive scale can cite this directly. The proof unfolds the definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold constant of the materials module satisfies $0 < \ thr$, where $\ thr$ is the real defined by unfolding that constant (an expression in the golden ratio $\varphi$).
background
Materials RS Module 8 is a structural package for Hall resistance $R_H = h/e^2$ obtained from the RS fine-structure derivation. It is marked structural: zero sorry, zero axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced in the Recognition chain (T6). The module imports Constants and Cost, and defines a real canonicalThreshold used as a positive scale in the materials layer.
Upstream, phi_gt_onePointFive records the tighter bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. That inequality is the only external fact needed for positivity of the threshold.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith with the single lemma phi_gt_onePointFive ($1.5 < \varphi$). No further case splits or cost identities are required.
why it matters
Gives a proved positivity fact for the materials threshold scale inside Module 8 (Hall resistance / fine-structure structural layer). Downstream use is not yet wired in the graph (used_by empty), but sibling certificate objects (RSMatl008Cert, cert, cert_inhabited) sit in the same module and are the natural consumers of a positive threshold.
In the broader RS picture this is bookkeeping under the forced $\varphi$ (T6) and the structural constants package, not a new forcing step. It closes a trivial but necessary positivity obligation so later materials identities can assume a positive scale without local arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.