posPair_real_pos
plain-language theorem explainer
If an integer pair (s, t) satisfies the constructive positivity predicate PosPair, then the real number s + t√5 is strictly positive. Anyone citing the sign bridge between the sigma0 golden integers and classical real order needs this forward direction. The proof is a three-case analysis on PosPair, with nlinarith closing each real inequality after casting.
Claim. Let $s, t \in \mathbb{Z}$. If $(s, t)$ satisfies the integer positivity predicate (both nonnegative and not both zero; or $s < 0 < t$ with $s^2 < 5 t^2$; or $t < 0 < s$ with $5 t^2 < s^2$), then $0 < s + t\sqrt{5}$ in $\mathbb{R}$.
background
This module is the display bridge from the golden integers $\mathbb{Z}[\varphi]$ into $\mathbb{R}$. The sigma0 development in GoldenInt forces $\varphi$ as the unique positive golden root entirely inside $\mathbb{Z}[\varphi]$; here one pays the continuum tax once by evaluating $a + b\varphi \mapsto a + b\varphi_{\mathbb{R}}$ and matching the classical order.
The predicate PosPair s t is the integer-only stand-in for $s + t\sqrt{5} > 0$. Its three disjuncts are: both components nonnegative with at least one strictly positive; $s < 0 < t$ dominated by $t\sqrt{5}$ via $s^2 < 5t^2$; or $t < 0 < s$ dominated by $s$ via $5t^2 < s^2$. Constructive positivity of a golden integer $x = a + b\varphi$ is then IsPos x := PosPair (2a+b) b, since $a + b\varphi = (s + b\sqrt{5})/2$ with $s = 2a+b$.
The theorem is the forward half of the sign bridge: integer positivity implies real positivity of the evaluation. The reverse half uses exclusivity (isPos_not_neg) rather than a real-side case split.
proof idea
Cast the integer hypotheses to $\mathbb{R}$ and case-split on the three disjuncts of PosPair.
Case 1 (both nonnegative, one strictly positive): cast the nonnegativity bounds, then on the strict disjunct apply nlinarith with $0 < \sqrt{5}$.
Case 2 ($s < 0 < t$ and $s^2 < 5t^2$): assume for contradiction $s + t\sqrt{5} \le 0$, rearrange to $t\sqrt{5} \le -s$, and feed the squared domination inequality plus positivity of $t\sqrt{5}$ into nlinarith.
Case 3 ($t < 0 < s$ and $5t^2 < s^2$) is symmetric: contradiction yields $s \le -t\sqrt{5}$, and nlinarith closes with the squared bound.
Auxiliary facts used: $(\sqrt{5})^2 = 5$ and $0 < \sqrt{5}$.
why it matters
This is the forward direction of the sign bridge isPos_iff_toReal_pos, which equates the decidable sigma0 predicate IsPos with classical real positivity of toReal. Downstream, that equivalence lets every sigma0 trichotomy and uniqueness theorem about golden-integer order speak about the real order, not a private surrogate.
In the module architecture this is the continuum tax paid once: the T6 derivation ($\varphi$ forced as the unique positive golden root) stays delta-forced inside $\mathbb{Z}[\varphi]$; only the display into $\mathbb{R}$ uses Real.sqrt and real arithmetic. The bridge also underwrites t6_bridge, identifying the sigma0 $\varphi$ with $(1+\sqrt{5})/2$.
Framework landmark: T6 in the forcing chain (phi as self-similar fixed point). Without this lemma the integer sign calculus would remain formally disconnected from the classical PhiForcing presentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.