canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in eight-tick domain-cost applications is strictly positive. Anyone bounding costs or certifying eight-tick structure against that cutoff would cite this. The proof is a one-line unfold-plus-linarith wrapper on 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 collects structural eight-tick applications of Recognition Science: the period $2^D = 8$ forced by the forcing chain (T7 eight-tick octave, T8 spatial $D = 3$). The same $8$ reappears as musical octave notes, color-flavor quark counting, SU(3) gluons, the eightfold way, and related discrete structures. Status is structural theorem (no sorry, no axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The sibling definition canonicalThreshold is the real cutoff used with domain cost in this file; positivity is the elementary gate before any comparison or certificate.
Upstream, Constants supplies the tighter lower bound $\varphi > 1.5$ (from $\sqrt{5} > 2$), which is already stronger than the classical $\varphi > 1$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \cdots$ by linarith using the lemma $\varphi > 1.5$. No case split and no further Recognition identities are required; linear arithmetic on that single strict inequality closes the goal.
why it matters
Positivity of the canonical threshold is the first numeric hygiene fact for eight-tick application certificates in this module (siblings include domain-cost nonnegativity and the EightTickAppsV2Cert bundle). It sits under the forcing-chain landmarks T6 ($\varphi$ forced) and T7 (eight-tick octave from $2^3$). No downstream edges are recorded yet, so the lemma is presently a local gate rather than a widely reused bridge. It does not itself derive the eight-tick period or any particle multiplet; it only guarantees the cutoff used in those structural comparisons is a positive real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.