canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used by the reionization-end certificate is strictly positive. Anyone checking the RS prediction that reionization completes near a small power of φ (around Planck’s z_end ∼ 5.5–6) needs this positivity fact. The proof is a one-line wrapper: unfold the threshold and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $\tau$ appearing in the reionization-end certificate satisfies $0 < \tau$. Here $\tau$ is the real constant obtained by unfolding the module’s threshold definition in terms of the golden ratio $\varphi = (1+\sqrt{5})/2$.
background
The module derives the end of cosmic reionization from the Recognition Science J-cost, as a structural theorem (no sorry, no axioms). Observationally, reionization completes near $z_{\mathrm{end}}\sim 5.5$–$6$ (Planck). RS matches this with a short power of the golden ratio: $\varphi^3\approx 4.24$, $\varphi^4\approx 6.85$, so the natural candidates are $z_{\mathrm{end}}=\varphi^3$ or $\varphi^4$ (module doc).
The golden ratio $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain. The only upstream fact used here is the elementary bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The sibling canonicalThreshold is the named real constant that the certificate treats as the positivity gate for the endpoint comparison; this lemma records that gate.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (an arithmetic expression in $\varphi$), then apply linarith to the imported lemma $\varphi>1.5$. No further lemmas or case splits are required.
why it matters
Positivity of the canonical threshold is the elementary gate that lets the reionization-end certificate (ReionEnd3Cert, cert, cert_inhabited) treat the RS endpoint as a well-defined positive scale. It sits in the cosmology layer that reads redshifts off the $\varphi$-ladder after the J-cost has been fixed (T5 J-uniqueness, RCL). The module’s structural claim is that the same cost that forces $\varphi$ also places $z_{\mathrm{end}}$ near $\varphi^3$ or $\varphi^4$, consistent with Planck. No downstream edges are recorded yet; the immediate consumers are the sibling certificate constructions in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.