canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS gravity structural layer is strictly positive. Gravity and domain-cost arguments that need a positive cutoff cite this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold built from the golden ratio $\varphi$ is strictly positive: $0 < \tau_{\mathrm{can}}$.
background
This module is Gravity RS Structural Module 6. Its local setting is the structural uniqueness of the golden ratio as the self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$, recorded as a zero-sorry structural theorem package.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the RS fixed point forced at T6 of the forcing chain. The upstream lemma phi_gt_onePointFive supplies the tighter real bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ (unfolded in the proof); sibling declarations package domain cost and the RS-GRV structural certificate around the same constant.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ from phi_gt_onePointFive. No further case splits or algebraic identities are required once the definition is expanded.
why it matters
Positivity of the canonical threshold is a structural hygiene fact for the RS gravity layer: domain-cost and certificate objects in the same module (domain cost nonnegativity, the RS-GRV structural 006 certificate) sit on a positive cutoff built from $\varphi$. It anchors the T6 landmark that $\varphi$ is the forced self-similar fixed point, so thresholds derived from $\varphi$ inherit a strict lower bound rather than a formal placeholder. No downstream edges are recorded yet; the result is local scaffolding closure inside the structural 006 package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.