canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the RS gravity structural layer is strictly positive. Gravity and ladder analysts cite it whenever a positive φ-built cutoff is required in domain-cost or certificate arguments. The proof is a one-line wrapper: unfold the definition, then finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T_{\mathrm{can}}$ (the real constant defined from the golden ratio $\varphi$ in this gravity module) satisfies $0 < T_{\mathrm{can}}$.
background
This module records structural facts for Recognition Science gravity tied to the eight-tick octave: one full traversal of the binary recognition lattice has period $2^D = 8$ with $D = 3$. The status line is structural theorem, zero sorry and zero axiom.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the chain (T6). An upstream lemma supplies the tighter real bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a named real built from $\varphi$ in this file; sibling declarations also introduce a domain cost and nonnegativity facts used by the module certificate.
Positivity of that threshold is the elementary gate before any comparison or certificate packing that treats the threshold as a strict lower cut.
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 open.
why it matters
Keeps the structural gravity certificate free of ad-hoc positivity assumptions: every later comparison against the canonical threshold can quote a proved strict inequality rather than a numeric guess. The module sits in the gravity domain of the RS forcing picture, where the eight-tick octave (T7) and $D = 3$ (T8) fix the lattice period that gravity structural claims must respect.
No downstream theorem edges are recorded for this declaration itself; it is consumed locally by the module certificate (RSGRVStructural005Cert / cert) that packages the structural claims of this file. It does not touch open mass-ladder or $\alpha$-band questions; it only clears a positivity obligation on a $\varphi$-native cutoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.