canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the ISM dust-fraction cosmology module is strictly positive. Anyone citing the Module 11 structural match (J(φ)² ≈ 1.39%) needs this positivity fact for the certificate. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold of the module is strictly positive: $0 < T_{\mathrm{can}}$.
background
Cosmology RS Module 11 records the ISM dust-fraction identity $J(\varphi)^2 \approx 1.39%$, presented as a structural match to the empirical $\sim 1%$ dust fraction, with zero sorry and zero axioms.
Here $\varphi = (1+\sqrt{5})/2$ is the golden ratio forced as the self-similar fixed point (T6). The J-cost is the unique cost functional $J(x) = (x+x^{-1})/2-1$ from T5; on $\varphi$ one has $J(\varphi)^2 \approx 0.0139$. The module also names a domain cost and a canonical threshold used by the certificate RSCosmo011Cert.
The sole upstream fact is the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting inequality by linarith using the lemma $\varphi > 1.5$. No further algebraic identities are required.
why it matters
Keeps the Module 11 certificate (ISM dust fraction MATCH) on a fully proved footing: the threshold that domain costs are compared against is known to be positive. Sits beside the nonnegativity of the domain cost and the inhabitation of the module certificate. Framework landmarks in play are T5 (J-uniqueness) and T6 ($\varphi$ forced), since the headline claim is $J(\varphi)^2 \approx 1.39%$. No downstream dependents are recorded yet; the lemma is local scaffolding for the cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.