canonicalThreshold_pos
plain-language theorem explainer
The canonical baryon threshold built from the golden ratio is strictly positive. Anyone citing the RS structural match Omega_b ~ J(phi)/2 needs this positivity lemma. Proof is a one-line unfold of the threshold definition followed by linarith from the bound phi > 1.5.
Claim. The canonical threshold (the RS-native baryon density scale constructed from $\varphi$) satisfies $0 < t$, where $t$ is that threshold constant.
background
Module Cosmology.OmegaBaryon4 packages a structural theorem for the baryon density parameter: observationally $\Omega_b \approx 0.049$, while Recognition Science supplies the nearby scale $J(\varphi)/2 \approx 0.059$. Here $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law, and $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point (forcing chain T5–T6).
Because $\varphi$ obeys $\varphi^2=\varphi+1$, one has $J(\varphi)=\varphi-3/2$. The canonical threshold in this file is the corresponding positive scale (unfolded in the proof), so positivity is equivalent to $\varphi>1.5$.
Upstream, phi_gt_onePointFive records the elementary bound $\varphi>1.5$, obtained from $\sqrt{5}>2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith using the lemma that $\varphi>1.5$. No further algebraic identities are required.
why it matters
This is a tiny positivity brick inside the OmegaBaryon4 structural package (module status: 0 sorry, 0 axiom). The parent narrative is the RS claim that the baryon fraction sits near $J(\varphi)/2$, consistent with the observed $\Omega_b\approx 0.049$. The lemma guarantees the threshold used by the certificate siblings (OmegaBaryon4Cert, cert, cert_inhabited) is a genuine positive scale rather than a formal symbol.
It sits downstream of the forcing-chain constants ($\varphi$ from T6, $J$ from T5) and does not itself close the observational match; it only keeps the inequality side of the certificate well-formed. No used_by edges are recorded yet, so its immediate consumers are the in-module cert constructors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.