canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the RS gap-45 structural module is strictly positive. Cite this when a later inequality needs a positive scale built from φ. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T$, where $T$ is the real constant obtained by unfolding the module's canonical-threshold definition (an expression in the golden ratio $\varphi$).
background
This module records RS structural facts around gap-45: at spatial dimension $D=3$ one has $D^2(D+2)=9\cdot 5=45$, identified as the minimum rung for stable self-reference. The file is marked a structural theorem block (no sorry, no axioms).
The only external numeric input is the golden ratio $\varphi=(1+\sqrt{5})/2$. Upstream, phi_gt_onePointFive supplies the tight lower bound $\varphi>1.5$, proved from $\sqrt{5}>2$. The canonical threshold is a named real built from $\varphi$ (unfolded in the proof); positivity of that scale is the local claim.
Sibling facts in the same file treat a domain cost functional and a structural certificate packing these inequalities.
proof idea
Wrapper proof. Unfold the definition of the canonical threshold, exposing an explicit real expression in $\varphi$. Discharge the resulting strict inequality by linarith against the single lemma $\varphi>1.5$. No case split and no further RS structure is used.
why it matters
Gap-45 is the structural landmark tying $D=3$ (forcing step T8) to the minimum self-reference rung on the $\varphi$-ladder (T6). A positive canonical threshold is the elementary scale fact any later comparison against that rung needs. The module packages the claim into a structural certificate (RSMTHStructural004Cert); this lemma is the positivity half of that certificate. No downstream consumers are wired yet in the graph, so the immediate role is local certification rather than a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.