canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the RS reionization-redshift module is strictly positive. Anyone citing the φ-ladder bracket for z_reion (φ^4 to φ^5) needs this gate before cost or certificate lemmas. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T$ of the RS reionization module satisfies $0 < T$. Positivity follows from the definition of $T$ in terms of the golden ratio $\varphi$ together with the bound $\varphi > 3/2$.
background
The module treats reionization redshift as a structural RS claim: observed $z_{\mathrm{reion}}\sim 7$–$10$ sits between $\varphi^4\approx 6.85$ and $\varphi^5\approx 11.09$, so the $\varphi$-ladder brackets the data. Status is a structural theorem (no sorry, no extra axioms).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. Upstream, the lemma $\varphi>1.5$ records the elementary tightening $\sqrt{5}>2\Rightarrow(1+\sqrt{5})/2>3/2$. The canonical threshold is the real scale defined from $\varphi$ in this file; sibling definitions (domain cost, reionization certificate) sit downstream of its positivity.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold to an explicit real expression in $\varphi$, then close $0<T$ by linarith using the upstream lemma $\varphi>1.5$. No case splits or further lemmas.
why it matters
Local positivity gate for the RS reionization-redshift development. The module’s structural claim is that $\varphi^4$ to $\varphi^5$ brackets $z_{\mathrm{reion}}\sim 7$–$11$, consistent with observation. This lemma ensures the threshold scale used in that comparison is positive, so later nonnegativity and certificate inhabitation (domain-cost nonnegativity, certificate inhabited) rest on a sound base. It does not yet appear in the used-by graph; it is infrastructure inside the cosmology reionization file rather than a cross-module forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.