For integers 4 ≤ k < l, some difference occurs three times in {0, ±1, ±k, ±l} iff l ∈ {k+1, k+2, 2k−1, 2k, 2k+1, 3k}
ProvedDiazModulus.power_pair_difference_count_iffcombinatoricsdiaz-modulus-leantranscendence
Let be integers and . Some has if and only if .
Proof. The six cases have explicit witnesses (for : , ). Conversely, is an involution of , so three elements contain two, and , with ; the pairs and then force a coincidence among the differences , and a case analysis closed by linear arithmetic leaves exactly the six values of .
Novelty. Elementary.
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem power_pair_difference_count_iff (k l : ℤ) (hk : 4 ≤ k) (hkl : k < l) :
(∃ d : ℤ, 0 < d ∧ 3 ≤ (({0, 1, -1, k, -k, l, -l} : Finset ℤ).filter
(fun s => s + d ∈ ({0, 1, -1, k, -k, l, -l} : Finset ℤ))).card) ↔
(l = k + 1 ∨ l = k + 2 ∨ l = 2 * k - 1 ∨ l = 2 * k ∨ l = 2 * k + 1 ∨ l = 3 * k) := by
sorry
end DiazModulus
Source
Elementary combinatorics; a step of R6 of the Diaz modulus mission (the polar-degree note). Formal proof: Diaz modulus mission, 8 October 2026 (C. Perassi).