phi_isPos
plain-language theorem explainer
In the golden ring ℤ[φ], the ring element φ is constructively positive under the decidable integer sign predicate. Anyone citing the sigma0 T6 uniqueness package needs this fact as one of the four conjuncts. The proof is a one-line kernel decision: positivity reduces to a finite integer check on the pair (2a+b, b).
Claim. In the ring $\mathbb{Z}[\varphi]=\mathbb{Z}\times\mathbb{Z}$ with $(a,b)\mapsto a+b\varphi$, the element $\varphi=(0,1)$ is positive in the constructive sense: the integer pair $(s,b)=(2a+b,b)$ satisfies the decidable positivity predicate $\mathrm{PosPair}$ that encodes the sign of $(s+b\sqrt{5})/2$.
background
The module re-derives the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. Elements are pairs $(a,b)\in\mathbb{Z}\times\mathbb{Z}$ standing for $a+b\varphi$, with multiplication folded through $\varphi^2=\varphi+1$. The design goal is a sigma0 (choice-free) axiom closure: only ${propext, Quot.sound}$, no Classical.choice.
Constructive positivity is not the real inequality $0<x$. It is the decidable predicate $\mathrm{IsPos},x := \mathrm{PosPair}(2a+b,,b)$, which is the exact integer sign trichotomy of $s+b\sqrt{5}$ with $s=2a+b$. The instance DecidablePred IsPos makes the predicate available to decide.
The classical continuum statement lives only at the display bridge in GoldenIntReal. Inside this module, every positivity claim is pure integer arithmetic.
proof idea
One-line tactic proof: by decide. Unfolding IsPos phi yields a concrete PosPair goal on the integer coefficients of $\varphi=(0,1)$, namely the pair $(s,b)=(1,1)$. That atomic integer predicate is decidable, so the kernel closes it by computation. No lemmas are invoked; no case splits are needed.
why it matters
This is conjunct (2) of t6_delta_forced, the sigma0 packaging of T6: $\varphi$ satisfies $x^2=x+1$, is positive, the only roots are $\varphi$ and $\psi=1-\varphi$, and $\varphi$ is the unique positive root. Downstream, t6_bridge lifts the same positivity to the display continuum as $0<\mathrm{toReal},\varphi$ with $\mathrm{toReal},\varphi=(1+\sqrt{5})/2$.
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point. The classical spine node PhiForcing already proves uniqueness over $\mathbb{R}$ but pays Classical.choice as carrier tax. This lemma is the choice-free positivity atom that lets the delta-spine re-derivation stay inside ${propext, Quot.sound}$. Without it, the unique-positive-root clause of T6 cannot be stated constructively.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.