isPos_ne_zero
plain-language theorem explainer
In the golden ring ℤ[φ], every constructively positive element is nonzero. Anyone proving uniqueness of the positive self-similar root (T6, delta-forced) cites this to separate the zero element from the positive cone. The proof is a one-step contradiction: equality to zero is rewritten away and discharged by the kernel fact that zero is not positive.
Claim. Let $x = a + b\varphi \in \mathbb{Z}[\varphi]$. If $x$ is positive in the decidable integer sense (the pair $(2a+b,\, b)$ lies in the constructive positive cone for $(s + b\sqrt{5})/2$), then $x \neq 0$.
background
This module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. Elements are pairs $(a,b)$ standing for $a + b\varphi$, with multiplication reduced by $\varphi^2 = \varphi + 1$. The goal is a choice-free (sigma0) derivation whose axiom footprint stays inside ${propext, Quot.sound}$.
Positivity is not the real order. IsPos is the decidable predicate PosPair (2a+b) b, encoding the exact sign trichotomy of $(s + b\sqrt{5})/2$ with $s = 2a+b$. Zero is the pair $(0,0)$. The continuum bridge (toReal, comparison with PhiForcing.φ) is deferred to a separate sigma1 module; everything here is elementary integer arithmetic.
The classical continuum statement that $\varphi$ is the unique positive self-similar ratio appears upstream as phi_unique_self_similar. This file strips the carrier tax and re-proves the same content inside $\mathbb{Z}[\varphi]$.
proof idea
Term-style contradiction. Assume $x = 0$ via rintro rfl. The hypothesis IsPos x becomes IsPos 0, which is false by the sibling lemma zero_not_isPos. That single fact closes the goal. No ring laws or norm computations are needed.
why it matters
T6 in the forcing chain asserts that $\varphi$ is the unique positive solution of $x^2 = x + 1$. In the delta-forced golden ring that uniqueness is stated entirely with integer predicates: $\varphi$ is positive, $\psi = 1-\varphi$ is not, and no other ring element satisfies the golden equation. Separating the positive cone from zero is a trivial but mandatory hygiene step before uniqueness arguments and before the kernel computation that $\varphi$ itself is positive.
The module doc frames the whole development as the sigma0 re-derivation of PhiForcing.phi_unique_self_similar, with irrationality of $\sqrt{5}$ carried by strong induction (sq_ne_five_sq) rather than real analysis. This lemma sits in that supporting layer. No downstream uses are recorded yet; it is infrastructure for the T6 block that follows in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.