canonicalThreshold_pos
plain-language theorem explainer
The module's canonical threshold (a real built from the golden ratio φ) is strictly positive. Cosmology proofs that need a positive scale or cutoff on the φ-ladder cite this. The argument is a one-line unfold-plus-linarith wrapper from the bound φ > 1.5.
Claim. The canonical threshold $\tau$ associated to the $\varphi$-ladder CMB construction satisfies $0 < \tau$.
background
The module derives the CMB temperature structurally from the Recognition Science $\varphi$-ladder: $T_{\mathrm{CMB}}/T_{\mathrm{vac}}=\varphi^{-k}$ with $T_{\mathrm{vac}}$ the Planck temperature scale and $k=196$, recovering $T_{\mathrm{CMB}}\approx 2.73,\mathrm{K}$ near the observed $2.725,\mathrm{K}$. Status is structural (no sorry, no axioms).
Constants come from IndisputableMonolith.Constants: $\varphi=(1+\sqrt{5})/2$. The upstream lemma records the tight elementary bound $\varphi>1.5$, proved from $\sqrt{5}>2$. Cost primitives are imported from the Cost module; the local canonical threshold is the positive real scale used by the domain-cost / CMB certificate siblings in this file.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0<\tau$ by linarith using the single fact $\varphi>1.5$. No further case splits or Recognition Composition Law identities are required.
why it matters
Keeps the CMB-from-$J$-cost development on a strictly positive scale so later certificate objects (CMBTemp3v2Cert, cert, cert_inhabited) can treat the threshold as a genuine cutoff rather than a formal symbol. In the broader RS chain this sits under the $\varphi$-ladder mass/temperature bookkeeping (T6 forces $\varphi$ as the self-similar fixed point); positivity is the minimal arithmetic hygiene before quoting $T_{\mathrm{CMB}}=T_{\mathrm{vac}},\varphi^{-196}$. No external used-by edges are recorded yet; the consumers are the sibling certificates in the same cosmology module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.