canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold is a strictly positive real constant. Structural proofs that need a positive cutoff built from φ (domain-cost bounds, certificate packing in this module) cite it. The argument is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the real constant obtained by unfolding its definition in terms of $\varphi$) is strictly positive: $0 < \tau_{\mathrm{can}}$.
background
Module RS_MTH_Structural_009 sits in the mathematics layer of the Recognition Science forcing chain (T5 J-uniqueness through T8, D = 3). It is marked structural: zero sorry, zero axioms. Imports pull in Mathlib, the RS constants (including $\varphi$), and the cost primitives.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The upstream lemma phi_gt_onePointFive records the elementary bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a named real built from $\varphi$; its positivity is the local fact needed by sibling domain-cost nonnegativity and the module certificate.
Sibling declarations in the same file introduce domainCost, its evaluation identity, nonnegativity, the threshold itself, and the packing certificate RSMTHStructural009Cert.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold so the goal becomes an explicit linear inequality in $\varphi$. Discharge that inequality by linarith using the single upstream fact $\varphi > 1.5$ (phi_gt_onePointFive). No further case splits or cost identities are required.
why it matters
Gives a clean positivity anchor for the structural package in RS_MTH_Structural_009. Downstream certificate inhabitants and domain-cost nonnegativity in the same module can quote it without re-proving the arithmetic. In the broader framework it supports the T5–T8 forcing spine (J-uniqueness, $\varphi$ forced, eight-tick octave, D = 3) by keeping threshold constants strictly positive in RS-native units. No external used-by edges are recorded yet; the immediate consumers are the local certificate and cost lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.