isPos_trichotomy
plain-language theorem explainer
Every element of the golden ring ℤ[φ] is positive, zero, or has positive negation under the constructive sign predicate. Workers on the choice-free T6 spine cite this as the discrete sign law before any continuum bridge. The proof applies integer-pair trichotomy to (2a+b, b) and kills the s²=5b² tie by the √5-descent lemma.
Claim. For every $x=a+b\varphi$ in the golden ring $\mathbb{Z}[\varphi]$, at least one of the following holds: $x$ is constructively positive (the integer pair $(2a+b,\,b)$ is a positive pair), $x=0$, or $-x$ is constructively positive.
background
The 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 folded through $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: only elementary integer arithmetic, with axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$.
Constructive positivity IsPos is the decidable predicate that the pair $(s,b)$ with $s=2a+b$ is a positive pair. This encodes the exact sign trichotomy of $s+b\sqrt{5}$ without naming reals. The upstream lemma int_sq_eq_five_sq states that $s^2=5b^2$ forces $b=0$, by strong-induction descent on $\mathbb{N}$ from the irrationality of $\sqrt{5}$.
posPair_trichotomy supplies the three-way split on integer pairs once that impossible tie is excluded.
proof idea
Instantiate posPair_trichotomy at $s=2a+b$ and $t=b$, feeding int_sq_eq_five_sq as the tie-breaker so $s^2=5b^2$ never survives. Case-split the resulting disjunction.
- Left:
IsPos xholds outright. - Middle: both coordinates vanish;
omegaforces $a=0$, thenextshows $x=0$. - Right: rewrite the positive-pair data for $-x$ using
neg_aandneg_b(so $2(-x).a+(-x).b=-(2a+b)$ and $(-x).b=-b$), and transport the negative-pair witness.
No continuum lemmas; only ring identities, omega on atomic goals, and the descent lemma.
why it matters
This is the sigma0 sign law for $\mathbb{Z}[\varphi]$. Downstream, isPos_iff_toReal_pos in GoldenIntReal quotes it as the key to the sign bridge: "Proved via the sigma0 trichotomy — the forward direction is posPair_real_pos; the reverse uses exclusivity so no real-side case analysis is ever needed." Continuum tax is paid once at the display boundary, not inside the derivation.
In the Recognition forcing chain this supports the T6 node (φ as the unique positive self-similar fixed point) in its delta-forced, choice-free form. The module target is sigma0 DELTA_FORCED; this trichotomy is a load-bearing step toward stating "φ is the unique positive root" with no real numbers at all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.