isPos_not_neg
plain-language theorem explainer
If a golden integer is constructively positive, its additive inverse is not. Anyone building the ordered ring structure on ℤ[φ] for the choice-free T6 spine cites this exclusivity. The proof rewrites IsPos(−x) into the negated PosPair data and discharges via the pair-level non-negation lemma.
Claim. Let $x = a + b\varphi$ be an element of the golden ring $\mathbb{Z}[\varphi]$. Write positivity of $x$ as the integer predicate $\mathrm{PosPair}(2a+b,\, b)$ encoding $s + t\sqrt{5} > 0$. If $x$ is positive, then $-x$ is not positive.
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)$ standing for $a + b\varphi$, with multiplication folded through $\varphi^2 = \varphi + 1$. The target axiom closure is sigma0 (no Classical.choice): only elementary integer arithmetic, ring, trichotomy, and atomic omega.
Constructive positivity IsPos x is defined as PosPair (2a+b) b. Here PosPair s t is a decidable three-disjunct predicate on $\mathbb{Z}$ that says exactly $s + t\sqrt{5} > 0$: both components nonnegative and not both zero; or $s < 0$ dominated by $t\sqrt{5}$; or $t < 0$ dominated by $s$. Negation on golden integers acts componentwise (neg_a, neg_b).
Upstream, posPair_not_neg already proves exclusivity at the pair level: PosPair s t and PosPair (-s) (-t) cannot both hold. All nine case combinations close by omega on atomic False.
proof idea
Tactic proof by contradiction. Assume IsPos (-x). Unfold that to a PosPair on the components of $-x$. Using neg_a and neg_b plus a one-line ring identity, rewrite $2(-x).a + (-x).b = -(2x.a + x.b)$ and $(-x).b = -x.b$, so the assumption becomes PosPair (-(2a+b)) (-b). The hypothesis IsPos x is already PosPair (2a+b) b. Apply posPair_not_neg to those two pair facts and obtain False.
why it matters
Exclusivity of positivity under negation is a basic ordered-ring fact needed before one can treat $\varphi$ as the unique positive root of $x^2 = x + 1$ inside $\mathbb{Z}[\varphi]$. That uniqueness is the content of the sigma0 re-derivation of T6 in the Delta Forcing Spectrum program: the continuum and Classical.choice are deferred to the display bridge in GoldenIntReal.
Downstream it is consumed in GoldenIntReal (cited use site posPair_real_pos), where the integer sign predicate is matched to ordinary real positivity $0 < s + t\sqrt{5}$. Without pair-level and element-level exclusivity, the sign trichotomy and the bridge IsPos x ↔ 0 < toReal x would not be coherent. Framework landmark: T6 $\varphi$-forcing, choice-free carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.