canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS gravity structural package is strictly positive. Gravity and gap-45 arguments that compare domain costs against this cutoff cite it. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the real constant obtained by unfolding the module's canonical-threshold definition in terms of the golden ratio $\varphi$.
background
This module is Gravity RS Structural Module 4. Its local setting is the RS gap-45 identity $D^2(D+2)=9\cdot 5=45$ at spatial dimension $D=3$, read as the minimum rung for stable self-reference. Status is structural: zero sorry, zero axiom.
The only external numeric input is the golden ratio $\varphi=(1+\sqrt{5})/2$ from the Constants layer. The upstream lemma records the tight elementary 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 constant is the claim here. Sibling facts in the same file treat a domain cost and its nonnegativity, so the threshold is the comparison scale those costs are measured against.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi>1.5$ supplied by phi_gt_onePointFive. No case split and no further lemmas.
why it matters
Gap-45 is the structural marker that $D=3$ forces a minimum self-reference rung of 45 on the $\varphi$-ladder (primer T6–T8: $\varphi$ fixed, eight-tick octave, $D=3$). A positive canonical threshold is the elementary positivity gate any later comparison of domain cost against that cutoff needs.
No downstream edges are recorded yet; in-module siblings (RSGRVStructural004Cert, cert, cert_inhabited) are the natural consumers that package this fact into the structural certificate for the module. The declaration closes a tiny but mandatory arithmetic obligation so the rest of the gap-45 story does not re-prove $\varphi>3/2$ inline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.