canonicalThreshold_pos

Physics RS Module 4 records the tree-level Weinberg angle $\sin^2\theta_W = J(\varphi)/(1+J(\varphi)) \approx 0.1054$, with a loop-corrected target near $0.231$. Here $J(x) = (x + x^{-1})/2 - 1$ is the Recognition cost (T5), and $\varphi$ is the self-similar fixed point forced at T6.

The only upstream fact used is the tighter bound $\varphi > 1.5$, which follows from $\sqrt{5} > 2$ and the closed form $\varphi = (1+\sqrt{5})/2$. Because $J(\varphi) = \varphi - 3/2$, that bound is exactly the statement that the cost at $\varphi$ is positive; the canonical threshold in this module is the named real built from $\varphi$ whose positivity is discharged the same way.

Sibling facts in the module include nonnegativity of the domain cost and the zero-sorry module certificate.

One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the upstream lemma $\varphi > 1.5$. No further case splits or algebraic identities are required once the definition is expanded.

Keeps Module 4 at structural-theorem status (zero sorry, zero axiom) for the Weinberg angle claim. No downstream dependents are recorded yet; the lemma sits next to domain-cost nonnegativity and the inhabited module certificate. In the forcing chain it is pure bookkeeping under T5–T6: once $\varphi$ is forced and bounded below by $3/2$, every threshold built as a positive combination of $\varphi$ (including quantities that reduce to $J(\varphi)$) is positive by linear arithmetic. It does not touch T7 (eight-tick) or T8 ($D=3$), nor the $\alpha^{-1}$ band.