canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the matter-perturbation / CMB module is strictly positive. Cosmology arguments that need a positive cutoff or scale cite this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the positive real scale built from the golden ratio $\varphi$ in this module) satisfies $0 < t_{\mathrm{can}}$.
background
This module develops a structural account of CMB temperature anisotropy from the Recognition Science J-cost. The module header records the target scale $\Delta T/T \sim 10^{-5}$ and the RS estimate $J(\varphi)^{D+1} = J(\varphi)^4 \approx 1.94\times 10^{-4}$, which is the same order of magnitude.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point of the forcing chain (T6). The only upstream fact used here is the elementary bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a named real constant in this file, defined from $\varphi$; positivity is the first arithmetic check before it is fed into domain-cost and certificate constructions.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the lemma $\varphi > 1.5$. No further Recognition identities are required; the inequality is pure real arithmetic once the definition is expanded.
why it matters
Local hygiene for the MatterPert4 certificate stack: a positive threshold is a prerequisite for any comparison of domain cost against a cutoff in the CMB anisotropy argument. Downstream use edges are not yet wired in the graph, but sibling names (domainCost_nonneg, MatterPert4Cert, cert_inhabited) show the intended landing zone inside the structural (0-sorry) CMB certificate.
In the broader framework this sits under cosmology rather than the T0–T8 forcing core. It does not itself derive $\Delta T/T$; it only clears the positivity obligation so that later comparisons to $J(\varphi)^4$ can be stated cleanly. The module’s order-of-magnitude claim ($J(\varphi)^4 \sim 2\times 10^{-4}$ vs observed $10^{-5}$) remains interpretive context, not a consequence of this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.