canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant is strictly positive. Researchers citing domain-cost or recognition-threshold inequalities in the 2026 state certificate need this elementary sign fact. The proof unfolds the definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real constant built from $\varphi$ in this module) is strictly positive: $0 < t_{\mathrm{can}}$.
background
This module is the Recognition Science 2026 state-of-the-art certificate: a structural bundle with zero sorry and zero axioms, recording that the forcing chain T0–T8 is complete and that the derived constants sit in their claimed bands.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The upstream lemma phi_gt_onePointFive strengthens the usual $\varphi > 1$ to $\varphi > 1.5$, via $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ (its body is unfolded in the proof); positivity is the sign check required before treating it as a cost or creation cutoff beside the sibling domain-cost definitions.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then close $0 < \cdots$ by linarith using the lemma $\varphi > 1.5$. No further case splits or cost identities are required.
why it matters
Sits in Foundation.RecognitionScience2026State as local hygiene for the structural certificate (siblings include the domain-cost lemmas and the inhabited cert bundle). Guarantees the threshold scale used next to domain cost is a positive real, so later nonnegativity and comparison facts are well-typed as strict inequalities.
No recorded downstream consumers yet; the lemma is certificate-local. It rests only on the T6 constant $\varphi$ and the tighter numerical bound $\varphi > 1.5$, consistent with threshold language elsewhere in RS (e.g. Berry creation near $\varphi^{-1}$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.