canonicalThreshold_pos
plain-language theorem explainer
The canonical CMB optical-depth threshold is strictly positive. In RS units that threshold is J(φ)=φ−3/2, the value that seeds the reionization depth match to Planck τ≈0.054. Anyone citing the structural τ certificate in this module needs the positivity fact. Proof is a one-line unfold plus linarith from the bound φ>1.5.
Claim. The canonical threshold is strictly positive: $0 < \varphi - 3/2$. Equivalently $0 < J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the Recognition cost and $\varphi=(1+\sqrt{5})/2$.
background
This module derives a structural expression for the CMB reionization optical depth from the Recognition cost $J$. Status is a finished structural theorem (zero sorry, zero axioms). The working comparison is $\tau=J(\varphi)/2\approx0.059$, within about 10% of the Planck 2018 value $\tau=0.054$.
$J$ is the unique cost forced by the Recognition Composition Law and T5 uniqueness: $J(x)=(x+x^{-1})/2-1$. On the golden ratio $\varphi$ forced at T6 one has the elementary identity $J(\varphi)=\varphi-3/2$. The local definition canonicalThreshold is exactly that quantity.
The sole upstream fact used here is the tighter numerical bound $\varphi>1.5$, obtained from $\sqrt{5}>2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (which is $\varphi-3/2$), then discharge $0<\varphi-3/2$ by linarith using the imported lemma $\varphi>1.5$.
why it matters
Positivity is the first arithmetic gate for the CMB optical-depth certificate constructed in the same module (CMBOptDepth3Cert, cert, cert_inhabited). Without it the threshold cannot serve as a physical scale for reionization depth.
In the broader RS chain the identity $J(\varphi)=\varphi-3/2$ sits on T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point). The module treats the resulting $\tau\approx J(\varphi)/2$ as a structural prediction, not a fit. No downstream edges are recorded yet; the immediate consumers are the sibling certificate declarations that package the numerical match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.