The Kalai-Sahai-Sudan collision bound for the group (Lemma 4.8)
DisprovedAKS.group_upperLemma 4.8 of the paper, whose proof is attributed to Kalai, Sahai, and Sudan: if n is not a power of p, then the group G-cal is small - at most n^(sqrt t). The proof: the bounded subset I-hat = {(n/p)^i p^j : i, j at most floor(sqrt t)} of I has (floor(sqrt t) + 1)^2 > t distinct numbers (distinct because a collision would force a power of p to equal a power of n, making n a power of p), so two of them, m1 > m2, are equal modulo r; then X^m1 = X^m2 modulo X^r - 1, and introspection turns the collision into the equation y^m1 = y^m2 satisfied by every image y in F of a polynomial of P, with m1 at most n^(floor(sqrt t)). So G-cal lies inside the root set of the polynomial Y^m1 - Y^m2, whose degree m1 is at most n^(sqrt t).
Formalization Note The statement is the collision: two numbers m2 < m1 at most n^(Nat.sqrt t), with every image of P in the field F_p[X]/(h) satisfying y^m1 = y^m2. The coprimality of n/p and p to r and the equality t = the size of the residue group G are hypotheses (they place the residues of I-hat inside G, by the order-divides-phi(r) window argument); the cardinality consequence - the root bound of Y^m1 - Y^m2 over a field gives at most m1 elements - is part of the goal's proposed work.
import Mathlib import Definitions.Def_AKS_poly import Definitions.Def_AKS_alg
namespace AKS
/-! Lemma 4.8 of the paper (Kalai, Sahai, and Sudan): if n is not a power
of p, the group G-cal lies in the roots of Y^(m_1) - Y^(m_2) for two
colliding elements m_2 < m_1 of the bounded set I-hat. -/
theorem group_upper (n p r t ℓ : ℕ) [Fact (Nat.Prime p)]
(h : Polynomial (ZMod p)) [Fact (Irreducible h)]
(hdiv : h ∣ (Polynomial.X ^ r - 1 : Polynomial (ZMod p)))
(hintros : ∀ m, inI n p m → ∀ f, inP p ℓ f → introspective p r f m)
(hnpow : ¬ ∃ k, 0 < k ∧ n = p ^ k)
(ht : t = (Gfin n p r).card)
(hcop : Nat.gcd (n / p) r = 1 ∧ Nat.gcd p r = 1) :
∃ m₁ m₂ : ℕ, m₂ < m₁ ∧ m₁ ≤ n ^ (Nat.sqrt t) ∧
∀ f, inP p ℓ f →
Polynomial.aeval (AdjoinRoot.root h) f ^ m₁
= Polynomial.aeval (AdjoinRoot.root h) f ^ m₂ := by sorry
end AKS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: fix n, p, r, t, ell with p prime, and an irreducible h over F_p dividing X^r - 1; assume every m of I is introspective for every f of P; assume n is not p^k for any k > 0, t equals the number of residues modulo r of I inside the window, and n/p and p are coprime to r. Then there are natural numbers m2 < m1 with m1 at most n^(floor(sqrt t)) such that for every polynomial f of P, the image of f in F_p[X]/(h) satisfies y^m1 = y^m2.
False as stated because p | n is not assumed: with n = 3, p = 2, r = 7, ell = 0 and h = X^3 + X + 1 over F_2 all hypotheses hold (n / p = 1, Gfin 3 2 7 = {1, 2, 4}, t = 3, P = {X^e} is introspective for every m by the identity X^(em) = X^(em)) but no m2 < m1 <= 3 satisfies root^(m1) = root^(m2), since the root of h has order 7; the statement also fails at n = 0, where hcop forces r = 1 and n ^ Nat.sqrt t = 0. The paper's Lemma 4.8 takes p a prime factor of n. The corrected theorem AKS.group_upper_of_dvd adds the hypotheses p | n and 0 < n and is otherwise identical; the milestone of mission 5b2088ab-bbea-4f55-a196-d5ad6ff9f847 is relinked to it.
Confirmed by the mission captain (proposal self-audit).