canonicalThreshold_pos

This module is the Plan v7 Recognition Science complete summary certificate: a structural theorem package (0 sorry, 0 axiom) that packages the claim that one cost equation $J(x)=(x+x^{-1})/2-1$ is uniquely forced and yields $\varphi$, gap-45, $D=3$, and the derived constants.

The golden ratio $\varphi=(1+\sqrt{5})/2$ lives in Constants. The upstream lemma used here is the tighter lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The sibling definition canonicalThreshold is the named cutoff unfolded in the proof; positivity is the elementary gate before any cost or certificate inequality that divides by or compares against that cutoff.

Imports pull Mathlib, Constants, and Cost, so the local setting is foundation-level constant hygiene rather than a deep forcing step (T5–T8).

One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0<$ that expression by linarith using the lemma $\varphi>1.5$. No case split and no cost-functional identities are required; the arithmetic is pure comparison against the golden-ratio lower bound.

Inside the RS summary certificate stack, several nonnegativity and threshold lemmas need a strictly positive canonical cutoff. This theorem closes that gate so certificate inhabitants and domain-cost facts can quote a proved positivity fact rather than an ad-hoc norm_num.

It sits downstream of the Constants bound $\varphi>1.5$ and beside siblings such as domain-cost nonnegativity and the summary cert structure. It is not itself a forcing-chain step (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$); it is infrastructure that keeps the summary module free of sorry when thresholds appear. No downstream consumers are recorded on the graph yet; the value is local certificate completeness.