canonicalThreshold_pos
plain-language theorem explainer
The module's canonical threshold (a real constant built from the golden ratio φ) is strictly positive. Anyone packaging the RS fine-structure certificate α^{-1} ∈ (137.030, 137.039) needs this elementary positivity fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold constant of this module (a real defined from the golden ratio $\varphi$) satisfies $0 < t$, where $t$ denotes that threshold.
background
Physics RS Module 2 packages the EM fine-structure claim: the RS prediction places $\alpha^{-1}$ in the open interval $(137.030, 137.039)$, which contains the CODATA value $137.036$. The module is marked structural (zero sorry, zero axioms) and RS_PASS.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the Recognition forcing chain. A tighter elementary bound is available upstream: $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a φ-derived real constant defined in this module (sibling of the domain-cost helpers); its positivity is the present claim and is the natural gate before any comparison that treats the threshold as a positive scale.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the single upstream fact $\varphi > 1.5$ (phi_gt_onePointFive). No further lemmas or case splits are required: after unfolding, the goal is a linear inequality in $\varphi$ discharged by that bound.
why it matters
Positivity of the canonical threshold is bookkeeping inside the fine-structure structural package: the module asserts the RS $\alpha^{-1}$ band and exposes a certificate (RSPhysics002Cert / cert_inhabited). Without $t > 0$, any later comparison that scales costs or windows by the threshold would be ill-typed as a strict bound.
Framework landmarks in play are T6 (φ forced) and the RS-native $\alpha^{-1}$ window $(137.030, 137.039)$. The declaration does not itself prove the band; it clears the elementary positivity obligation so the certificate can treat the threshold as a positive real scale. No downstream edges are recorded yet in the graph, so its immediate consumers are the sibling certificate constructions in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.