isPos_iff_toReal_pos
plain-language theorem explainer
The decidable positivity predicate on golden integers ℤ[φ] is equivalent to strict positivity of the real evaluation map. Anyone citing the T6 display bridge or the rational comparison lemmas on the phi-ladder needs this sign bridge. The proof is a short trichotomy argument: forward via the PosPair-to-real lemma, reverse by excluding zero and the negative case using evaluation of negation.
Claim. For every golden integer $x=a+b\varphi\in\mathbb{Z}[\varphi]$, the constructive positivity predicate on $x$ holds if and only if $0<a+b\varphi_{\mathbb{R}}$, where evaluation uses the classical golden ratio $\varphi_{\mathbb{R}}=(1+\sqrt{5})/2$.
background
The module is the sigma1 display boundary: it evaluates the golden ring ℤ[φ] into ℝ once, so sigma0 (delta-forced) structure about φ can be read classically. GoldenInt is pairs $(a,b)$ representing $a+b\varphi$, with multiplication folded through $\varphi^2=\varphi+1$. The map toReal sends $a+b\varphi$ to $a+b\varphi_{\mathbb{R}}$ with $\varphi_{\mathbb{R}}$ the classical root from PhiForcing.
Constructive positivity IsPos is the decidable predicate PosPair(2a+b,b) on the rewritten form $(s+t\sqrt{5})/2$. Upstream, isPos_trichotomy asserts that exactly one of positivity, zero, or positivity of the negative holds (the tie $s^2=5b^2$ is excluded by integer descent). The lemma posPair_real_pos already shows that PosPair s t implies $0<s+t\sqrt{5}$ over the reals, which is the forward half of the bridge.
proof idea
A key lemma first shows the forward direction for every $y$: positivity implies $0<\mathrm{toReal}(y)$, by applying posPair_real_pos, unfolding evaluation with $\varphi=(1+\sqrt{5})/2$, and finishing with linarith after push_cast.
The biconditional is then a constructor. Left-to-right is the key lemma at $x$. Right-to-left assumes $0<\mathrm{toReal}(x)$ and cases on isPos_trichotomy. The positive branch is immediate. The zero branch rewrites via toReal_zero and contradicts lt_irrefl. The negative branch applies the key lemma to $-x$, rewrites with toReal_neg, and obtains $0<-\mathrm{toReal}(x)$, contradicting the hypothesis by linarith.
why it matters
This is the sign bridge that makes the sigma0 order on ℤ[φ] identical to the real order under evaluation. Downstream, ratLt_toReal and ratGt_toReal invoke it to turn discrete rational comparisons into real inequalities. The T6 display bridge t6_bridge relies on the same positivity transfer: the unique positive golden root from the sigma0 derivation evaluates to $(1+\sqrt{5})/2$ with classical positivity.
In the Recognition Science forcing chain, T6 forces φ as the self-similar fixed point entirely inside ℤ[φ] at sigma0. This lemma ensures those positivity and uniqueness statements are about the real order, not a private surrogate. The continuum tax (Classical.choice via Real.sqrt) is paid only at this display boundary; the derivation itself stays delta-forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.