canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant appearing in the structural physics certificate at recognition rung 66 is strictly positive. Certificate and domain-cost positivity arguments cite this bound. The proof is a one-line wrapper: unfold the threshold and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$.
background
This module packages a structural Recognition Science certificate for the Physics domain at recognition rung 66 (Plan v7, 120th pass). Status is a pure structural theorem: zero sorry, zero axioms. Sibling definitions introduce a domain cost, its nonnegativity, and the canonical threshold constant used by the certificate.
The only upstream fact needed here is the tighter lower bound on the golden ratio: $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ so that $(1+\sqrt{5})/2 > 3/2$. In RS units $\varphi$ is the self-similar fixed point forced by the J-cost uniqueness chain (T5–T6).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single lemma $\varphi > 1.5$. No case splits or further Recognition lemmas are required; positivity is pure real arithmetic once the threshold is expanded in terms of $\varphi$.
why it matters
Positivity of the canonical threshold is a local hygiene lemma inside the structural Physics certificate at rung 66. It sits beside domain-cost nonnegativity and the inhabited certificate record, ensuring the numeric gate used by that certificate is well-defined and strictly above zero. In the broader forcing chain it rests only on T6 ($\varphi$ as the self-similar fixed point) via the elementary bound $\varphi > 1.5$. No downstream consumers are recorded yet; the lemma is infrastructure for the module's own certificate assembly rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.