canonicalThreshold_pos
plain-language theorem explainer
The module's canonical threshold is strictly positive. Cosmology and ladder arguments that need a positive cutoff (gap-45 / minimum stable self-reference rung at D=3) can cite this. The proof is a one-line unfold plus linarith from the bound φ > 1.5.
Claim. The canonical threshold of this structural module is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the real constant obtained by unfolding the module definition of the canonical threshold (a quantity built from the golden ratio $\varphi$).
background
This file is Cosmology RS Structural Module 4. Its module doc fixes the local setting: RS gap-45, namely $D^2(D+2)=9\cdot 5=45$, identified as the minimum rung for stable self-reference at $D=3$. Status is a structural theorem block (no sorry, no axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the Recognition chain (T6). The only upstream fact used here is the tighter numerical bound $\varphi>1.5$, proved from $\sqrt{5}>2$. Sibling definitions in the module introduce a domain cost and the canonical threshold itself; this theorem only records positivity of that threshold.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the lemma $\varphi>1.5$. No further case splits or Recognition identities are needed; positivity is pure real arithmetic once the definition is expanded.
why it matters
Gap-45 is the structural minimum rung for stable self-reference in three spatial dimensions (T8 forces $D=3$; the eight-tick octave is T7). A positive canonical threshold is the elementary numerical gate that later cost and ladder comparisons in this module can rely on without re-proving $\varphi>3/2$ each time.
No downstream consumers are wired yet in the graph (used_by is empty), so the result presently closes a local positivity obligation inside RS_COS_Structural_004 rather than feeding a named parent theorem. It sits under the structural (not dynamical) half of the cosmology layer and does not itself derive masses, $\alpha$, or expansion history.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.