IsPos
plain-language theorem explainer
Constructive positivity on the golden ring ℤ[φ]: an element a + b·φ is positive exactly when the integer pair (2a+b, b) satisfies the three-case sign law for s + t√5 > 0. Anyone proving the choice-free T6 node (unique positive root of x² = x + 1) cites this predicate. The body is a one-line abbreviation of that pair predicate; decidability is inherited.
Claim. For $x = a + b\varphi$ in the golden ring $\mathbb{Z}[\varphi]$, declare $x$ positive when the integer pair $(s,t) = (2a+b,\, b)$ satisfies the constructive sign law for $s + t\sqrt{5} > 0$: both nonnegative and not both zero, or $s < 0$ dominated by $t\sqrt{5}$, or $t < 0$ dominated by $s$.
background
The module re-derives the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi] = \mathbb{Z}\times\mathbb{Z}$ with $(a,b)\mapsto a + b\varphi$ and 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.
Elements are pairs of integers. The companion predicate on pairs encodes the exact sign trichotomy of $s + t\sqrt{5}$ entirely in $\mathbb{Z}$: both components nonnegative and not both zero; or $s < 0$ dominated by $t\sqrt{5}$ via $s^2 < 5t^2$; or $t < 0$ dominated by $s$ via $5t^2 < s^2$. Because $a + b\varphi = (s + b\sqrt{5})/2$ with $s = 2a + b$, positivity of a ring element is exactly that pair law on $(2a+b,, b)$.
This is the carrier for all later positivity lemmas (nonzero, exclusivity with negation, trichotomy) used to force $\varphi$ as the unique positive root without real numbers.
proof idea
One-line definitional abbreviation: unfold positivity of $x$ as the pair sign predicate applied to $(2x.a + x.b,, x.b)$. Decidability is inferred from the pair predicate's existing Decidable instance (itself unfolded from a finite disjunction of integer comparisons). No algebraic work occurs at this site.
why it matters
This predicate is the positivity language of the delta-forced T6 node. Downstream it feeds: $\varphi$ is positive (kernel decide); $\psi$ is not; a positive element is nonzero; positivity excludes negativity; and the full trichotomy (positive / zero / negative) that, with the two-root factorization of $x^2 = x + 1$, yields the unique positive root theorem t6_delta_forced.
In the Recognition forcing chain this is the choice-free carrier for T6 ($\varphi$ as the self-similar fixed point). The continuum bridge (toReal, agreement with the real $\varphi$, and equivalence of this predicate with $0 < \mathrm{toReal}, x$) is deferred to the display module, so the derivation itself stays sigma0. Without a decidable integer positivity law, the unique-positive-root claim would fall back to the sigma1 real proof in PhiForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.