canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Neutron-lifetime and domain-cost arguments in the RS physics stack cite this positivity before comparing measured lifetimes to the φ-ladder prediction. The proof unfolds the threshold definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $\tau_{\mathrm{can}}$ (the real constant defined from the golden ratio $\varphi$ in this module) satisfies $0 < \tau_{\mathrm{can}}$.
background
This file is Physics RS Module 3, whose structural claim is the neutron-lifetime match $\varphi^{17}\cdot 0.246,\mathrm{s}=878.5,\mathrm{s}$ against the PDG value $878.4,\mathrm{s}$. The module imports the global constants (including $\varphi$) and the cost layer, and exposes a small cluster of domain-cost and threshold lemmas used by the certificate RSPhysics003Cert.
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. Upstream, phi_gt_onePointFive records the elementary bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is the local real constant (unfolded in the proof) against which domain costs and lifetime ratios are compared; positivity is the first arithmetic fact needed before any inequality with measured data.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi>1.5$ supplied by phi_gt_onePointFive. No further lemmas or case splits are required; the positivity is pure real arithmetic once the definition is expanded.
why it matters
Positivity of the canonical threshold is a tiny but mandatory gate for the neutron-lifetime certificate in this module (status: structural theorem, zero sorry). Downstream certificate constructors and domain-cost non-negativity arguments rely on a strictly positive comparison scale before they can assert the $\varphi^{17}$ lifetime match. In the broader Recognition stack the same $\varphi$ appears as the T6 fixed point, the mass-ladder base, and the source of the Berry threshold $\varphi^{-1}$; keeping every derived threshold positive is part of the zero-axiom hygiene of the physics modules. No open scaffold remains here: the claim is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.