Multiplicative 1D Orbit Strict 3-AP Rigidity
Provedmultiplicative_orbit_1d_ap_freecombinatoricserdos-problemsnumber-theory
In a 1D geometric orbit {1, r, r^2}, the 3-AP condition 1 + r^2 = 2r forces r = 1.
Formal statement
import Mathlib theorem multiplicative_orbit_1d_ap_free (r : ℝ) (h_ap : 1 + r ^ 2 = 2 * r) : r = 1 := by sorry