canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS inflation-parameter suite is strictly positive. Anyone assembling or citing the InflationParam5 certificate (n_s, r bounds) needs this positivity fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the threshold constant defined from the golden ratio $\varphi$ in the RS inflation-parameter module.
background
The module fixes RS inflation observables against Planck-scale targets: observed $n_s \approx 0.9649$ and $r < 0.036$, with RS predictions $n_s = 1 - 2/45 = 0.9556$ (about 2.1σ) and $r = 2/(45\varphi^2) \approx 0.0169$. Status is structural (zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the Recognition forcing chain. The upstream lemma supplies the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a nonnegative real built from $\varphi$ (sibling of the domain-cost functionals in the same file); positivity is the first arithmetic gate before the certificate is inhabited.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single hypothesis $\varphi > 1.5$ (lemma phi_gt_onePointFive). No further case splits or Recognition-cost identities are required; the inequality is pure real arithmetic once the definition is expanded.
why it matters
Positivity of the canonical threshold is a leaf arithmetic fact inside the Inflation_Parameters5 certificate stack. It underwrites the structural claim that the RS predictions for the scalar spectral index and tensor-to-scalar ratio sit inside the observational window ($r$ passes cleanly; $n_s$ at 2.1σ, inside 3σ). Downstream siblings (InflationParam5Cert, cert, cert_inhabited) package the full parameter set; this lemma clears the sign obligation on the threshold constant so those certificates can be inhabited without extra hypotheses. It sits downstream of the T6 forcing of $\varphi$ and does not itself touch the eight-tick or $D=3$ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.