canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio φ is strictly positive. Cosmology structural certificates that need a positive cutoff cite this fact. The proof is a one-line wrapper: unfold the definition, then finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T$ (the real constant defined from the golden ratio $\varphi$ in this module) satisfies $0 < T$.
background
This module records structural facts for Recognition Science cosmology tied to φ-uniqueness: φ is the self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$, forced in the T6 step of the unified forcing chain.
The golden ratio is the constant $\varphi = (1+\sqrt{5})/2$. The upstream lemma phi_gt_onePointFive supplies the tighter real bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is a real expression in φ (unfolded in the proof); positivity of that expression is the local claim.
Sibling material in the same file defines a domain cost and packages the structural certificate RSCOSStructural006Cert. Imports are Mathlib, Constants, and Cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold so the goal is an explicit inequality in φ, then apply linarith with the single fact phi_gt_onePointFive ($1.5 < \varphi$). No further lemmas or case splits.
why it matters
Keeps the structural cosmology layer free of sorries and axioms by discharging the elementary positivity obligation on the φ-derived cutoff. Sits in the φ-uniqueness / T6 neighborhood of the forcing chain (self-similar fixed point), which underpins later RS constants and ladder constructions. Downstream use edges are empty in the graph snapshot; the natural consumer is the module certificate RSCOSStructural006Cert / cert_inhabited among the siblings. Does not itself force φ or derive cosmological observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.