Zumkeller’s Binary Gaussian Evaluation
Abstract
A vanishing binary digit polynomial at the Gaussian unit has an argument divisible by five.
Definition 1.1 (The binary Gaussian evaluation).
Formalization. D5/S1/Digit/ZumkellerBinaryGaussianEvaluationZeroMultipleOfFive.z (✓ std3).
Citation. Reinhard Zumkeller (2007). OEIS A131853, Numbers m such that z(m)=(0,0) with z as defined in A131851. URL: https://oeis.org/A131853.
Commentary.
The definition is Nat.binaryRec 0 (fun b _ w => (if b then 1 else 0) + ⟨0, 1⟩ * w). Here bit b n = 2n + (if b then 1 else 0), so the equations are exactly the OEIS A131851 recursion for the binary digit polynomial evaluated at the Gaussian imaginary unit.
Theorem 1.2 (Zumkeller’s divisibility conjecture).
Proof. Machine-checked in Lean as D5/S1/Digit/ZumkellerBinaryGaussianEvaluationZeroMultipleOfFive.zumkeller_a131853 (✓ std3). ∎
Resolves. Problems/oeis-a131853-binary-gaussian-evaluation-zero-multiple-of-five (proved) by D5/S1/Digit/ZumkellerBinaryGaussianEvaluationZeroMultipleOfFive.zumkeller_a131853.
Source. Repository-derived.
Commentary.
Binary induction proves m ≡ Re z(m) + 2·Im z(m) (mod 5). The identity uses the fact that the Gaussian unit behaves as 2 modulo 5 because 2 squared is congruent to minus one. Therefore z(m) = 0 forces m to be divisible by five, including the case m = 0.