canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in RS cosmology calibration is strictly positive. Anyone citing the structural module for parameter-free predictions needs this sign fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the real constant built from the golden ratio $\varphi$ in this module) is strictly positive: $0 < T_{\mathrm{can}}$.
background
This file is Cosmology RS Structural Module 10. The module sets the coherence energy $E_{\mathrm{coh}}$ once from the electron mass and then treats all further predictions as parameter-free; the status line is structural theorem (zero sorry, zero axiom).
The only external constant needed here is the golden ratio $\varphi = (1+\sqrt{5})/2$ from Constants. The upstream lemma records the tight elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a local real defined from $\varphi$; positivity is the first arithmetic sanity check before it is used as a cut in domain-cost comparisons.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single hypothesis $\varphi > 1.5$ supplied by phi_gt_onePointFive. No further lemmas or case splits.
why it matters
Keeps the structural certificate of the module honest: every named real cut that later appears in domain-cost or calibration statements must be known positive before it can serve as a threshold. The module itself advertises parameter-free cosmology once $E_{\mathrm{coh}}$ is fixed by the electron mass; this lemma is the elementary positivity step for the canonical cut. No downstream consumers are wired yet in the graph, so the result is presently a local hygiene fact inside the structural certificate rather than a cited step in a larger forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.