Finite Field Multiplicative Character Shift Rigidity for 3-AP Obstruction

Proved

char_weil_ap_rigid

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraerdos-problemsnumber-theory

For any prime $p$ and subgroup $H \le (\mathbb{Z}/p\mathbb{Z})^\times$ , if $H$ contains a 3-term arithmetic progression $x + z = 2y$ , then there exist elements $u, v \in H$ such that $u + v = 2$ , reducing 3-AP obstruction to a fixed level-set equation.

Formal statement

import Mathlib.Algebra.Group.Subgroup.Basic
import Mathlib.Algebra.Field.Basic
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring

theorem char_weil_ap_rigid {p : ℕ} [Fact (Nat.Prime p)] (H : Subgroup (ZMod p)ˣ)
    (x y z : (ZMod p)ˣ) (hx : x ∈ H) (hy : y ∈ H) (hz : z ∈ H)
    (hap : (x : ZMod p) + (z : ZMod p) = 2 * (y : ZMod p)) :
    ∃ u v : (ZMod p)ˣ, u ∈ H ∧ v ∈ H ∧ (u : ZMod p) + (v : ZMod p) = 2 := by sorry

View graph