canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold of RS Cosmology Module 4 is strictly positive. Anyone needing a positive φ-scale cutoff in this module cites it. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The module's canonical threshold $t$ (a scale defined from the golden ratio $\varphi$) satisfies $0 < t$.
background
RS Cosmology Module 4 is a structural block aimed at the scalar spectral index $n_s = 1 - 2/45 \approx 0.9556$, set against the Planck value $0.9649$ (reported $2.2\sigma$ tension). The module is marked structural: zero sorry, zero axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The only upstream fact used here is the tighter real bound $\varphi > 1.5$, which follows from $\sqrt{5} > 2$.
The canonical threshold is a named real constant in this module, defined by unfolding to a $\varphi$-expression. Sibling facts establish nonnegativity of the domain cost and package the module certificate; this lemma supplies the strict positivity half for the threshold itself.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold to expose its $\varphi$-expression, then discharge $0 < \cdots$ by linarith using the lemma $\varphi > 1.5$. No case split and no further lemmas.
why it matters
Gives the strict positivity fact for the module's canonical threshold, a prerequisite scale in the RS cosmology stack for Module 4. The module targets the structural $n_s = 1 - 2/45$ claim and its Planck comparison; this lemma is the elementary positivity gate on the threshold constant that such certificates rely on.
No downstream consumers are recorded yet in the graph. Framework landmarks in play are T6 ($\varphi$ forced) and the RS-native constants built from $\varphi$. The open item flagged by the module doc remains the $2.2\sigma$ $n_s$ tension with Planck; this lemma does not close that comparison, only the positivity of the local threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.