PosPair
plain-language theorem explainer
Integer sign predicate deciding when s + t√5 is strictly positive, without mentioning reals. Three mutually exclusive cases cover both components nonnegative (not both zero), negative s dominated by t√5, and negative t dominated by s. Downstream positivity, trichotomy, and the choice-free T6 re-derivation on ℤ[φ] all route through it. The body is a pure Prop definition plus a decidability instance.
Claim. For integers $s,t\in\mathbb{Z}$, write $\mathrm{PosPair}(s,t)$ when $s+t\sqrt{5}>0$, encoded by the disjunction: both $s,t\ge 0$ and not both zero; or $s<0$, $t>0$ and $s^2<5t^2$; or $s>0$, $t<0$ and $5t^2<s^2$. The predicate is decidable.
background
Module GoldenInt rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]\cong\mathbb{Z}\times\mathbb{Z}$ with $(a,b)\mapsto a+b\varphi$ and multiplication folded by $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: only {propext, Quot.sound}, no continuum and no Classical.choice.
Positivity of a golden integer $a+b\varphi$ is not taken from $\mathbb{R}$. Instead one passes to the conjugate form $(s+b\sqrt{5})/2$ with $s=2a+b$, and asks whether $s+t\sqrt{5}>0$ for $t=b$. That comparison is exactly what this predicate packages, using only integer inequalities and the comparison of $s^2$ with $5t^2$ (the rational shadow of $|s|$ vs $|t|\sqrt{5}$).
The same module proves irrationality of $\sqrt{5}$ by strong-induction descent on $\mathbb{N}$ (norm $N(a+b\varphi)=a^2+ab-b^2$), which later discharges the tie case $s^2=5t^2$ in trichotomy lemmas.
proof idea
Definitional: the body is the three-way disjunction of integer inequalities that characterize $s+t\sqrt{5}>0$. No lemmas are applied. A Decidable instance is obtained by unfolding the definition and letting Lean synthesize decidability of the atomic comparisons and boolean combinations.
why it matters
This is the kernel of constructive positivity on the delta-forced golden ring. IsPos on GoldenInt is literally PosPair (2a+b) b. Pair-level exclusivity (posPair_not_neg) and trichotomy (posPair_trichotomy, using the no-tie hypothesis from $\sqrt{5}$ irrationality) lift to isPos_not_neg and isPos_trichotomy, and zero_not_isPos is a kernel computation on the same predicate.
In the continuum bridge module, posPair_real_pos and injectivity of toReal rely on it to match integer positivity with $0<\mathrm{toReal},x$. Framework-wise it supports the sigma0 re-derivation of T6 (unique positive root of $x^2=x+1$ is $\varphi$) inside the Delta Forcing Spectrum program, keeping choice tax off the derivation spine and paying it only at the display boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.