canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of RS gravity structural module 9 is strictly positive. Gravity and certificate authors cite it when they need a positive cutoff built from φ. The proof is a one-line wrapper: unfold the definition, then linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $\tau$ of the RS gravity structural module is strictly positive: $0 < \tau$. Here $\tau$ is the real constant obtained by unfolding the module's canonical-threshold definition, and positivity follows from $\varphi > 1.5$.
background
This lives in Gravity RS Structural Module 9, a zero-sorry structural layer on the RS forcing chain (T5 J-uniqueness and φ uniqueness, T6 φ forced as self-similar fixed point, T7 eight-tick octave, T8 D = 3). The module packages domain-cost and threshold facts used by the structural certificate.
The only external arithmetic input is the golden ratio $\varphi = (1+\sqrt{5})/2$ from Constants. The upstream lemma records a tight lower bound: "$\varphi > 1.5$ (since $\sqrt{5} > 2$, so $(1+\sqrt{5})/2 > 1.5$)." After the threshold definition is unfolded, that inequality is exactly what linear arithmetic needs for strict positivity.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then run linarith on the single hypothesis phi_gt_onePointFive (i.e. $1.5 < \varphi$). No case split, no induction, no cost-functional identities.
why it matters
Keeps the structural certificate's cutoff strictly positive without axioms or sorry. The module status line is "STRUCTURAL THEOREM (0 sorry, 0 axiom)"; this lemma is the positivity half of that package, sitting beside nonnegativity of domain cost and the inhabited certificate record.
In the broader RS chain it sits under T5–T8: once φ is forced and bounded below by 1.5, every threshold written as a simple φ-offset inherits positivity for free. No downstream edges are recorded yet; the immediate consumers are the sibling certificate constructors in the same file (the structural-009 cert and its inhabited instance).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.