canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the CMB sound-horizon certificate is strictly positive. Cosmologists checking the RS identity that recovers r_s ≈ 147 Mpc from a J-cost factor times a φ-ladder length would cite this fact. The proof is a one-line unfold of the threshold definition, closed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T$ (the positive scalar built from the golden ratio that enters the Recognition Science sound-horizon formula) satisfies $0 < T$.
background
The module derives the CMB sound horizon from J-cost. In RS units the observed scale $r_s \approx 147$ Mpc is recovered as a J-cost factor times a pure $\phi$-ladder length: $\phi^{14} \sim 843$ Mpc and $147/843 \sim J(\phi)$, so $r_s = J(\phi)\cdot\phi^{14}$ Mpc exactly at the structural level.
Here $\phi = (1+\sqrt{5})/2$ is the self-similar fixed point. The sole upstream input is the elementary bound $\phi > 1.5$ (from $\sqrt{5} > 2$). The canonical threshold is the local positive scalar, defined directly from $\phi$, that the sound-horizon certificate normalizes against.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then finish with linear arithmetic on the hypothesis $\phi > 1.5$ supplied by the constants lemma that records this tighter lower bound. No other lemmas are invoked.
why it matters
Positivity is a prerequisite for the local sound-horizon certificate (the inhabited certificate objects assembled in the same module). The construction sits in the cosmology layer that ties J-cost and the $\phi$-ladder length scales to the observed acoustic scale $r_s = 147$ Mpc. The module is marked structural (zero sorry, zero axioms). No external downstream edges are recorded; the lemma is consumed inside the certificate assembly that realizes the Plan-v7 sound-horizon claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.