canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Domain-cost comparisons and Count Law 7 cutoff arguments cite this fact. The proof is a one-line unfold of the definition closed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau$, where $\tau$ is the real threshold constant defined from the golden ratio $\varphi$.
background
The module records Count Law 7 Exact v2: the structural identity $2^D-1=7$ forced once spatial dimension is $D=3$ (forcing-chain step T8), matching the familiar sevens (crystal systems, electroweak modes, diatonic notes, and related lists). Status is a structural theorem with zero sorry and zero axioms.
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. An upstream lemma tightens the elementary lower bound to $\varphi>1.5$, via $\sqrt{5}>2$ so $(1+\sqrt{5})/2>1.5$.
The canonical threshold is a real constant defined from $\varphi$. Sibling facts in the same file treat domain cost and its nonnegativity; positivity of the threshold is the elementary gate those comparisons need.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then finish with linarith supplied the lemma $\varphi>1.5$. No case analysis and no rewriting beyond the unfold; positivity is pure linear arithmetic once the definition is exposed.
why it matters
Count Law 7 is the exact count $2^D-1=7$ after $D=3$ is forced (T8), and sits inside the broader forcing chain that also fixes $\varphi$ (T6) and the eight-tick octave (T7). Positivity of the canonical threshold is a small supporting lemma in that structural package: any domain-cost argument that treats the threshold as a strict cutoff needs $0<\tau$. The module claims a fully closed structural theorem. The dependency graph lists no downstream consumers yet; the natural users are the sibling domain-cost nonnegativity facts and the Count Law 7 certificate in the same file. The link to the rest of Recognition Science is only through shared $\varphi$ and the $D=3$ count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.