canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold built from the golden ratio is strictly positive. Physicists citing cutoffs for domain cost or the top-Yukawa structural package in RS Module 7 need this sign fact. The proof is a one-line wrapper: unfold the definition, then linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau$, where $\tau$ is the real threshold constructed from the golden ratio $\varphi = (1 + \sqrt{5})/2$.
background
Physics RS Module 7 treats the top Yukawa as the unit coupling $y_t = 1$ at unification, identified with the $\varphi^0 = 1$ rung on the phi-ladder. The module is marked structural (zero sorry, zero axioms).
The golden ratio $\varphi$ is the self-similar fixed point of the Recognition forcing chain (T6). A standard real bound records $\varphi > 1.5$, obtained from $\sqrt{5} > 2$ via $(1+\sqrt{5})/2 > 3/2$.
The canonical threshold is a real built from $\varphi$ (its definition is unfolded in the proof). Sibling lemmas in the module compare domain cost against this threshold and record nonnegativity of that cost.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linear arithmetic (linarith) to the hypothesis $\varphi > 1.5$. Once the definition is expanded into an elementary expression in $\varphi$, the lower bound forces the expression above zero; no further identities are needed.
why it matters
Positivity of the canonical threshold is the basic sign check inside the top-Yukawa structural package. It keeps $\varphi$-ladder cutoffs well-defined and underwrites sibling comparisons of domain cost against the threshold. The module claims structural status (zero sorry). The dependency graph currently lists no downstream users, so the result stands as the positivity companion to the threshold definition itself. Framework landmarks: T6 forces $\varphi$; the top coupling sits at rung zero with $y_t = 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.