canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in RS Cosmology Module 6 is strictly positive. Anyone citing the structural DM-mass certificate (M_W/45 ladder, XENONnT target) needs this to treat the cutoff as a genuine positive scale. Proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold constant of the module is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the real constant obtained by unfolding the module definition (a linear expression in the golden ratio $\varphi$).
background
RS Cosmology Module 6 packages a structural, zero-sorry claim about a dark-matter mass scale written as $M_W/45 = 1.787,\mathrm{GeV}$, flagged as a 2026 XENONnT falsifier. The module imports Constants (for $\varphi$) and Cost (for the J-cost infrastructure used elsewhere in the ladder).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the Recognition forcing chain. The upstream lemma used here records the elementary bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a named real constant in this module; positivity is the minimal well-formedness fact needed before it can serve as a cutoff or gap scale on the $\varphi$-ladder.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith using the single upstream fact $\varphi > 1.5$. No case splits, no Cost identities, no cosmology-specific lemmas.
why it matters
Module 6 is marked STRUCTURAL THEOREM and TESTABLE: the DM mass $M_W/45$ is a concrete experimental target. Positivity of the canonical threshold is the first arithmetic hygiene step inside that certificate stack (siblings include domainCost_nonneg, RSCosmo006Cert, and cert_inhabited).
No downstream edges are recorded yet, so this lemma is presently a leaf supporting the local cert rather than a widely reused bridge. In the broader RS picture it sits downstream of T6 ($\varphi$ forced) and beside the Cost import; it does not itself invoke RCL, the eight-tick octave, or the $\alpha$ band. It keeps the module's threshold from being a vacuous or sign-indefinite scale when the XENONnT comparison is written down.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.