canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. Anyone citing the Logo5 cost curve (J on (0,∞) with the golden-ratio mark) needs this positivity fact. The proof unfolds the threshold definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $\tau$ (the positive real attached to the Logo5 cost curve at the golden ratio) satisfies $0 < \tau$.
background
The module fixes the Recognition Science logo cost $J(x) = (x + 1/x)/2 - 1$ on $(0,\infty)$. This is the unique J-cost from the forcing chain (T5): nonnegative, zero only at $x=1$, and self-similar under the golden ratio $\varphi$. The curve rises from the minimum $J(1)=0$ to the value at $x=\varphi$, which the module treats as the canonical threshold mark on the logo.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is imported from Constants. The only upstream fact used here is the tighter lower bound $\varphi > 1.5$ (from $\sqrt{5}>2$). The threshold itself is a named real built from $\varphi$; positivity is the first structural sanity check before nonnegativity and evaluation lemmas for the domain cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the lemma $\varphi > 1.5$. No further cost-function identities are required; linear arithmetic closes once the definition is exposed.
why it matters
Logo5 presents the single curve $J$ as the visual and structural core of Recognition Science ("one curve, all of physics"). Positivity of the canonical threshold is a zero-sorry structural fact that keeps the $\varphi$-mark strictly above the zero minimum at $x=1$, consistent with T5 J-uniqueness and T6 ($\varphi$ as self-similar fixed point). No downstream consumers are wired yet in the graph; the lemma sits beside domainCost_nonneg and the RSLogo5Cert bundle as part of the absolute final Logo5 certificate. It does not itself force dimension, the eight-tick octave, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.