canonicalThreshold_pos
plain-language theorem explainer
The canonical J-cost recombination threshold is strictly positive. Cosmology arguments that need a positive cutoff before comparing z_rec to the φ-ladder cite this fact. Proof is a one-line unfold of the threshold definition followed by linear arithmetic from φ > 1.5.
Claim. The canonical threshold constant appearing in the J-cost recombination-redshift construction is strictly positive: $0 < \tau_{\mathrm{can}}$.
background
This module treats recombination redshift as a structural consequence of the Recognition Science J-cost. Observationally $z_{\mathrm{rec}} \approx 1100$; in RS units one asks for the nearest φ-powers, since $\log 1100 / \log \varphi \approx 14.7$, so $z_{\mathrm{rec}}$ lies between $\varphi^{14}$ and $\varphi^{15}$.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The upstream lemma records the elementary bound $\varphi > 1.5$ (from $\sqrt{5} > 2$). The canonical threshold is the module-local real cutoff built from $\varphi$; positivity of that cutoff is the first arithmetic hygiene step before any comparison with the φ-ladder or the domain cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith using the lemma $\varphi > 1.5$. No further J-cost identities are required.
why it matters
Keeps the recombination-redshift certificate (Recombin3Cert / cert in the same module) on a strictly positive cutoff, so later comparisons with $\varphi^{14}$–$\varphi^{15}$ and the domain cost stay well-defined. The module is marked structural (0 sorry, 0 axiom) and records consistency of $z_{\mathrm{rec}} = 1100$ with the φ-ladder. No external downstream consumers are wired yet; the lemma is local scaffolding for the cosmology certificate chain rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.