canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant is strictly positive. Structural arguments that need a positive cutoff on the cost or domain side of RS_MTH_Structural_001 cite this fact. 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 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the real constant defined in this module from the golden ratio $\varphi$.
background
This module records structural predictions of Recognition Science: the J-cost $J(x) = \tfrac12(x + 1/x) - 1$, the golden ratio $\varphi$ as the self-similar fixed point, and the forcing of $D = 3$. Status is a structural theorem block with no sorry and no extra axioms.
The canonical threshold is a real constant built from $\varphi$ (in the RS framework the natural scale is the Berry creation threshold $\varphi^{-1}$). Positivity is the minimal arithmetic fact needed before any comparison or certificate that treats the threshold as a strict lower cutoff.
The only upstream lemma used is phi_gt_onePointFive: $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ and the closed form $\varphi = (1+\sqrt{5})/2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the inequality $\varphi > 1.5$. No case split and no further RS lemmas are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Sits in Mathematics RS Structural Module 1, which packages the structural core (J-form, $\varphi$, $D = 3$) as a zero-sorry block. The positivity fact is the arithmetic gate for any certificate or domain-cost comparison that assumes a strictly positive threshold (siblings include domainCost_nonneg and the module certificate RSMTHStructural001Cert).
In the forcing chain this supports the T5/T6 layer: J-uniqueness and $\varphi$ as the self-similar fixed point. No downstream used_by edges are recorded yet; the lemma is local scaffolding for the structural certificate rather than a deep dependency of later physics modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.