zero_not_isPos
plain-language theorem explainer
Zero in the golden ring ℤ[φ] is not positive under the constructive integer positivity predicate. Anyone proving that positive golden integers are nonzero cites this fact. The proof is a one-line kernel decision on the decidable PosPair predicate at (0,0).
Claim. The zero element $0 = 0 + 0\cdot\varphi$ of the golden ring $\mathbb{Z}[\varphi]$ is not positive: $\neg\mathrm{IsPos}(0)$. Equivalently, the integer sign predicate $\mathrm{PosPair}(s,t)$ fails at $(s,t)=(0,0)$.
background
This module re-derives the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]=\mathbb{Z}\times\mathbb{Z}$, with pairs $(a,b)$ standing for $a+b\varphi$ and multiplication folded through $\varphi^2=\varphi+1$. The goal is a choice-free (sigma0) development: only elementary integer arithmetic, no continuum carrier.
Positivity is not imported from $\mathbb{R}$. The predicate $\mathrm{IsPos}$ on a golden integer $x=(a,b)$ is defined by $\mathrm{PosPair}(2a+b,,b)$, where $\mathrm{PosPair}(s,t)$ is a decidable three-way integer condition encoding the sign of $s+t\sqrt{5}$: both components nonnegative and not both zero; or $s<0$ dominated by $t\sqrt{5}$; or $t<0$ dominated by $s$. Zero is the pair $(0,0)$.
The surrounding program is the Delta Forcing Spectrum: every theorem in this file must close in ${\mathrm{propext},,\mathrm{Quot.sound}}$, with the continuum bridge deferred to a separate display module.
proof idea
One-line wrapper: by decide. Unfolding $\mathrm{IsPos},0$ yields $\mathrm{PosPair}(0,0)$. Each of the three disjuncts of $\mathrm{PosPair}$ is false at $(0,0)$ by atomic integer arithmetic (nonnegativity-and-not-both-zero fails; the two strict-dominance clauses need a strictly positive component). The decidable instance on $\mathrm{PosPair}$ discharges the negation in the kernel.
why it matters
Feeds the immediate parent isPos_ne_zero: a positive golden integer is nonzero, proved by contradiction via this lemma. That nonzero fact is part of the choice-free T6 package in this module (unique positive root of $x^2=x+1$ stated entirely in $\mathbb{Z}[\varphi]$).
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point. The classical spine node does this over $\mathbb{R}$ and pays Classical.choice; this delta-spine module removes that tax. Establishing that zero is not positive is the base case of the positivity trichotomy that lets the unique-positive-root theorem stay inside sigma0.
No open scaffold: the claim is fully proved by decision procedure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.