ratWitness
plain-language theorem explainer
Builds the golden-integer witness q·x − p whose sign decides whether the rational p/q sits strictly below x ∈ ℤ[φ]. Anyone certifying rational brackets on the φ-ladder (φ, φ⁵, φ⁸, …) cites this constructor. It is a one-line structure map on the integer coefficients of x.
Claim. For $p,q\in\mathbb{Z}$ and $x=a+b\varphi\in\mathbb{Z}[\varphi]$, define the witness $q\cdot x-p:=(qa-p)+(qb)\varphi\in\mathbb{Z}[\varphi]$. Its positivity (via the sigma0 sign predicate on $\mathbb{Z}[\varphi]$) decides $p/q\lessgtr x$ when $q>0$.
background
The module LadderRatioBounds certifies dimensionless φ-ladder ratios at sigma0: every rung gap k gives the exact ratio φ^k, and concrete rational brackets on those powers must close by decide with no Real.sqrt, Float, or native_decide.
GoldenInt is the ring ℤ[φ] of pairs (a,b) standing for a+b·φ, with multiplication folded through φ²=φ+1. Ordering questions p/q ⋚ x on this ring reduce to a sign question about an element of ℤ[φ], which in turn is decided by comparing integer squares against 5t² (√5-irrationality already proved in DeltaSpine.GoldenInt).
The witness constructed here is exactly that difference q·x−p, kept entirely inside ℤ[φ] so the existing decidable positivity predicate IsPos applies directly.
proof idea
Pure definition: unpack x = ⟨a,b⟩ and return the GoldenInt pair ⟨q·a − p, q·b⟩. No lemmas, no tactics; the arithmetic identity q·(a+bφ)−p = (qa−p)+(qb)φ is the constructor itself.
why it matters
This is the shared substrate for the decidable bracket predicates RatLt and RatGt: RatLt p q x := IsPos(ratWitness p q x) and RatGt reuses the same witness on negated data. Downstream, GoldenIntReal.toReal_ratWitness lifts the construction to ℝ, proving toReal(ratWitness p q x) = q·toReal(x) − p, so the sigma0 integer brackets are genuine bounds on the real φ-ladder.
In the RS forcing chain, φ is the T6 self-similar fixed point and the mass law places spectrum rungs on the φ-ladder; certified rational brackets (e.g. 1618033/1000000 < φ < 1618034/1000000, and the φ⁵, φ⁸ octave bounds) are the computable end of that story at sigma0 DELTA_FORCED. Without this witness there is no choice-free integer predicate for p/q ⋚ x.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.