canonicalThreshold_pos
plain-language theorem explainer
The canonical Mott threshold used in this materials module is strictly positive. Anyone citing the RS structural match U/t = φ³ ≈ 4.24 (experimental band 3–5) needs this positivity fact as a basic side condition. The proof is a one-line unfold of the threshold definition followed by linarith from the constant bound φ > 1.5.
Claim. The canonical Mott threshold is strictly positive: $0 < \mathrm{canonicalThreshold}$. In this module the threshold is the RS scale $\varphi^3$ for the Mott ratio $U/t$, so the claim is equivalent to $0 < \varphi^3$.
background
Materials RS Module 10 treats the Mott metal–insulator transition. Recognition Science forces the dimensionless ratio $U/t$ onto the golden-ratio ladder at $\varphi^3 \approx 4.236$, which lies inside the accepted experimental window $3$–$5$; the module records this as a structural match (zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the unique self-similar fixed point of the Recognition forcing chain (T6). The upstream lemma phi_gt_onePointFive supplies the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The local definition canonicalThreshold packages the Mott scale (unfolded in the proof to an expression in $\varphi$), and the present theorem records that this scale is positive.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \ldots$ by linarith using the single upstream fact $\varphi > 1.5$. No further Recognition identities are required; positivity follows from the elementary lower bound on $\varphi$ alone.
why it matters
Positivity of the Mott threshold is a trivial but mandatory side condition for the module certificate (RSMatl010Cert / cert_inhabited) that packages the structural $U/t = \varphi^3$ match. It sits inside the materials layer of Recognition Science, downstream of the forcing-chain landmarks that fix $\varphi$ (T5–T6) and upstream of any quantitative comparison of the RS Mott scale against condensed-matter data. No further theorems currently depend on it (empty used-by list); it is infrastructure for the module’s inhabited certificate rather than a deep physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.