canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the precise Hubble-constant derivation is strictly positive. Anyone building nonnegativity or certificate arguments on that cutoff cites this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold used in the precise Hubble derivation is strictly positive: $0 < T_{\mathrm{can}}$.
background
The module derives a structural match of the Planck Hubble value $H_0 = 67.4,\mathrm{km/s/Mpc}$ from the Recognition Science phi-ladder: $H_0 = \varphi^k / \tau_{\mathrm{universe}}$ with $\tau_{\mathrm{universe}} = 13.8,\mathrm{Gyr}$, treated as a structural (zero-sorry) identity rather than a fit.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced by the Recognition Composition Law (T6). The upstream lemma supplies the elementary tightening $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is the module-local cutoff built from $\varphi$; positivity of that cutoff is the only claim here.
Sibling material in the same file defines a domain cost from the J-cost, records its nonnegativity, and packages a HubblePrecise2 certificate around these facts.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single upstream fact $\varphi > 1.5$. No further algebraic identities or cosmology lemmas are required; positivity is immediate once the definition is expanded in terms of $\varphi$.
why it matters
Positivity of the cutoff is a hygiene lemma for the structural Hubble certificate in this module (siblings HubblePrecise2Cert, cert, cert_inhabited). Without it, any later comparison that treats the threshold as a strict lower barrier would be ill-typed or vacuous.
In the broader Recognition chain the result sits under the phi-ladder mass and cosmology layer that uses T6 ($\varphi$ forced) and the eight-tick / rung bookkeeping. It does not itself force $H_0$ or $D=3$; it only clears the sign of the local threshold so the precise-$H_0$ packaging can proceed without sorry.
No downstream edges are recorded yet; the immediate consumers are the certificate constructors in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.