canonicalThreshold_pos
plain-language theorem explainer
The canonical cosmology threshold is strictly positive. Cosmology and RS-structural arguments that need a positive cutoff built from φ cite this fact. The proof unfolds the threshold definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \ thr_{\mathrm{can}}$, where $\ thr_{\mathrm{can}}$ is the real constant defined from the golden ratio $\varphi$ in this module.
background
This module is Cosmology RS Structural Module 9. It sits on the RS forcing chain T5 (J-uniqueness) through T6 (φ forced as the self-similar fixed point), T7 (eight-tick octave), and T8 (D = 3), and is marked as a structural theorem with no sorry and no axioms.
The golden ratio φ = (1 + √5)/2 is the unique positive fixed point forced by the Recognition Composition Law and J-cost uniqueness. Upstream, phi_gt_onePointFive records the tighter numerical bound φ > 1.5, obtained from √5 > 2. The canonical threshold is a module-local real constant built from φ; sibling facts also record nonnegativity of the domain cost and the certificate packaging for RS-COS-Structural-009.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the single upstream inequality φ > 1.5. No further case splits or RS identities are required once the definition is expanded.
why it matters
Positivity of the canonical threshold is a structural hygiene lemma for the cosmology side of Recognition Science: any later argument that treats the threshold as a strict cutoff (domain cost comparisons, certificate inhabitation for RS-COS-Structural-009) needs 0 < thr_can rather than a weak inequality. The module ties this to the forcing chain T5–T8 and φ uniqueness. No downstream dependents are recorded yet; the lemma is infrastructure for the structural certificate rather than a mass or α-band identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.