posPair_trichotomy
plain-language theorem explainer
For integers s,t, if s²=5t² forces t=0, then either the pair is positive for s+t√5, both vanish, or the negated pair is positive. Cited by anyone building choice-free positivity on ℤ[φ]. Proof is exhaustive Int.lt_trichotomy on signs of s and t; mixed signs compare s² to 5t², with omega only on atomic goals.
Claim. Let $s,t\in\mathbb{Z}$. Assume $s^2=5t^2$ implies $t=0$. Then either $s+t\sqrt{5}>0$ in the integer encoding (both components nonnegative and not both zero; or $s<0$ dominated by $t\sqrt{5}$; or $t<0$ dominated by $s$), or $(s,t)=(0,0)$, or the same positivity holds for $(-s,-t)$.
background
The GoldenInt module re-derives the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]\cong\mathbb{Z}\times\mathbb{Z}$ with multiplication folded through $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) proof: axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$, with no continuum and no Classical.choice. Positivity of $a+b\varphi$ is reduced to a decidable integer predicate on the pair $(s,t)=(2a+b,b)$, which is the exact sign trichotomy of $s+t\sqrt{5}$.
PosPair is that predicate: three disjuncts covering both components nonnegative and not both zero; $s<0$ dominated by $t\sqrt{5}$ via $s^2<5t^2$; or $t<0$ dominated by $s$ via $5t^2<s^2$. The hypothesis $s^2=5t^2\Rightarrow t=0$ is the integer form of irrationality of $\sqrt{5}$, proved elsewhere in the module by strong-induction descent. Tactic hygiene bans full simp and omega on structured goals; only explicit Int.lt_trichotomy splits and atomic omega are allowed.
proof idea
Unfold PosPair. Record the ring identities $(-s)^2=s^2$ and $(-t)^2=t^2$. Split on Int.lt_trichotomy for $s$, then for $t$ in each branch (nine sign cells).
Both negative, or $s<0$ and $t=0$: the negated pair lands in the nonnegative non-zero disjunct (omega). Both zero: middle disjunct. $s=0$ and $t\neq 0$: one of the two directed PosPair forms. Same-sign positive: nonnegative non-zero disjunct.
Mixed signs ($s$ and $t$ opposite): split Int.lt_trichotomy on $s^2$ versus $5t^2$. Strict inequality picks the matching PosPair (or PosPair of the negation, rewriting squares). Equality is absurd: the tie hypothesis forces $t=0$, contradicting $t\neq 0$ (omega). No classical choice; omega only closes atoms.
why it matters
Feeds isPos_trichotomy on GoldenInt: exactly one of IsPos x, x=0, IsPos(-x), by instantiating this lemma at $s=2a+b$, $t=b$ and discharging the tie via int_sq_eq_five_sq. That is the positivity half of the choice-free T6 node: $\varphi$ is the unique positive root of $x^2=x+1$ stated entirely in $\mathbb{Z}[\varphi]$, with no Real.sqrt and no Classical.choice.
In the forcing chain this is the sigma0 re-derivation of T6 (phi as self-similar fixed point). The continuum bridge (toReal, agreement with PhiForcing.φ) is deferred to GoldenIntReal and pays the sigma1 tax once at the display boundary. Supports the Delta Forcing Spectrum program target: every theorem in this module audits to subset of {propext, Quot.sound}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.