Formal target: Corpus.PaperTuDengConjecture.tu_deng_conjecture

**The Tu-Deng conjecture.** For $k \ge 2$ and a nonzero residue $t$ modulo $2^k - 1$, there are at most $2^{k-1}$ pairs of residues $(a, b)$ with $a + b = t$ whose binary weights (of their representatives in $0, \dots, 2^k - 2$) sum to at most $k - 1$.

Exact formal statement

∀ (k : Nat),
  LE.le.{0} 2 k →
    ∀ (t : ZMod (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) 1)),
      Ne.{1} t 0 →
        LE.le.{0}
          (Set.ncard.{0}
            (Set.ofPred.{0} fun p =>
              And (Eq.{1} (HAdd.hAdd.{0, 0, 0} (Prod.fst.{0, 0} p) (Prod.snd.{0, 0} p)) t)
                (LE.le.{0}
                  (HAdd.hAdd.{0, 0, 0} (Corpus.PaperTuDengConjecture.binaryWeight (Prod.fst.{0, 0} p).val)
                    (Corpus.PaperTuDengConjecture.binaryWeight (Prod.snd.{0, 0} p).val))
                  (HSub.hSub.{0, 0, 0} k 1))))
          (HPow.hPow.{0, 0, 0} 2 (HSub.hSub.{0, 0, 0} k 1))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record