canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the RS economics layer is strictly positive. Firm-growth and domain-cost arguments that compare against this cutoff cite it. The proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real constant defined from $\varphi$ in the RS economics module) satisfies $0 < \tau_{\mathrm{can}}$.
background
The ambient module is the Recognition Science economics layer (session 3). It is marked as a structural theorem block with no sorry and no extra axioms. The motivating picture is Gibrat's law (firm growth rate independent of size), specialized in RS to a recognition-optimal trajectory whose growth rate is $J(\varphi)$ times revenue growth, numerically about 11.8% per year.
The only external fact used is the tighter lower bound on the golden ratio: $\varphi = (1+\sqrt{5})/2 > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a named real constant in this module whose definition, once unfolded, is an elementary expression in $\varphi$; positivity is then immediate from that bound. Sibling material includes a domain cost functional and a four-step firm-growth certificate that sit alongside this positivity lemma.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting elementary inequality by linarith using the upstream lemma phi_gt_onePointFive ($1.5 < \varphi$). No case splits and no further Recognition-cost identities are required.
why it matters
Keeps the economics layer's threshold comparisons on a proved footing inside a zero-sorry structural block. Downstream use sites are not yet wired in the dependency graph (no used_by edges), but the sibling firm-growth certificate and domain-cost nonnegativity results are the natural consumers: any comparison of the form "cost or growth increment exceeds the canonical cutoff" needs $0 < \tau_{\mathrm{can}}$ first.
In the broader forcing chain this rests only on $\varphi$ itself (T6: $\varphi$ forced as the self-similar fixed point) and on the elementary arithmetic bound $\varphi > 1.5$. It does not invoke the Recognition Composition Law, the eight-tick octave, or the mass ladder; it is pure constant hygiene for the economics session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.