canonicalThreshold_pos
plain-language theorem explainer
The canonical cosmology threshold built from the golden ratio is strictly positive. Cosmology and ladder-cost arguments cite it whenever a domain-cost comparison needs a positive cutoff. The proof unfolds the definition and applies the elementary bound φ > 1.5 via linear arithmetic.
Claim. The canonical threshold constant (defined from the golden ratio $\varphi$) satisfies $0 < \mathrm{canonical\,threshold}$.
background
The ambient module is Cosmology RS Structural Module 3, whose stated content is the RS count law $2^D-1=7$ independent channels forced by the $D=3$ configuration dimension. Status is structural: zero sorry, zero axiom.
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point of the Recognition forcing chain (T6). The upstream lemma records the tight elementary lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is the local real constant built from $\varphi$ that serves as the positive cutoff for domain-cost comparisons in this module (siblings include the domain-cost functional and its nonnegativity).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge positivity by linarith using the upstream lemma $\varphi>1.5$. No further case splits or Recognition identities are required.
why it matters
Positivity of the canonical threshold is the elementary gate that lets later domain-cost inequalities in the structural cosmology module fire without side conditions. The module itself packages the RS count law $2^D-1=7$ forced by $D=3$ (forcing landmark T8). No downstream consumers are recorded yet in the dependency graph; the lemma sits as a local positivity fact supporting the structural certificate RSCOSStructural003Cert. It does not itself encode the count law, only the sign of the $\varphi$-built cutoff used beside it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.