toReal_ratWitness
plain-language theorem explainer
The bracket witness q·x − p in ℤ[φ] evaluates under the real embedding to the affine form q·toReal(x) − p. Anyone bridging sigma0 rational comparisons on golden integers to classical real inequalities cites this identity. The proof is a short algebraic expansion: unfold the evaluation map, push integer casts, and finish by ring.
Claim. For all integers $p,q$ and every golden integer $x\in\mathbb{Z}[\varphi]$, the real evaluation of the witness element $q\cdot x-p$ equals $q\cdot\mathrm{ev}(x)-p$, where $\mathrm{ev}$ sends $a+b\varphi$ to $a+b\varphi_{\mathbb{R}}$.
background
This module is the sigma1 display bridge from the golden ring ℤ[φ] into ℝ. Golden integers are pairs ⟨a,b⟩ standing for a + b·φ, with multiplication folded through the relation φ² = φ + 1. The evaluation map sends ⟨a,b⟩ to a + b·φ_ℝ using the classical positive golden root from PhiForcing.
On the sigma0 side, rational comparisons against a golden integer are decided by an integer witness: ratWitness p q x is the element q·x − p = ⟨q a − p, q b⟩ in ℤ[φ]. The predicate RatLt p q x asserts that this witness is positive in the decidable integer sense (IsPos). The module's job is to show that these integer predicates match the classical order once displayed in ℝ.
The local setting is deliberately sigma1 CHOICE only at the continuum boundary: the T6 derivation that forces φ lives entirely inside ℤ[φ]; only the display into ℝ pays Classical.choice (via Real.sqrt and real arithmetic).
proof idea
Expand the left-hand side by the definition of the evaluation map on the witness pair ⟨q·x.a − p, q·x.b⟩. That produces the real expression (q a − p) + (q b)·φ. Rewrite the goal as that form equal to q·(a + b·φ) − p, push integer-to-real casts, and close by ring. No external lemmas beyond the definitions of toReal and ratWitness are required.
why it matters
This identity is the algebraic hinge that turns sigma0 sign predicates into classical rational inequalities. Downstream, ratLt_toReal and ratGt_toReal rewrite through it (together with isPos_iff_toReal_pos) to obtain p/q < toReal x and toReal x < p/q whenever q > 0. Those bridges make the integer trichotomy and uniqueness theorems of DeltaSpine speak about the real order, not a private surrogate.
In the Recognition forcing chain this sits at the T6 display boundary: φ is forced inside ℤ[φ], and the continuum tax is paid once so that the sigma0 golden root evaluates to (1+√5)/2. Without the witness evaluation identity, ladder-ratio bounds and positivity comparisons could not be exported to the classical PhiForcing presentation used elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.