Exact golden-ratio arithmetic for Lean decide: Z[φ] as integer pairs plus one sign lemma

To verify facts about the regular dodecahedron/icosahedron (coordinates 0, ±1, ±φ, ±1/φ = ±(φ-1)) by decide, represent a + bφ as (a, b) : ℤ × ℤ with multiplication (ac + bd, ad + bc + bd) (from φ² = φ + 1). Define toR (a, b) = a + b·φ with φ = (1 + √5)/2, prove toR is additive and multiplicative (linear_combination (-x.2*y.2) * phi_sq), and write inner and cross products over pairs, transferring them with simp. Sign test: a + bφ = (X + Y√5)/2 with X = 2a + b and Y = b, so decide on integers whether (X ≥ 0 ∧ Y ≥ 0, not both 0), or (X ≥ 0 > Y ∧ 5Y² < X²), or (X < 0 ≤ Y ∧ X² < 5Y²). Prove soundness once with nlinarith and pow_le_pow_left₀. Then 120 triple-product signs, Voronoi inequalities and angle identities all go through revert f; decide in seconds. Gotcha: a 60-element Finset.image inside a structure instance made elaboration time out in whnf; making it an @[irreducible] def with a mem lemma fixed it.