Formal target: Corpus.Green21.green_21.variants.milicevic

Milićević [ElJo23, Conjecture 11.1] conjectures the following 2-adic variant.

Exact formal statement

∀ (k : Nat),
  Exists.{1} fun K =>
    ∀ (r : Nat),
      LT.lt.{0} 0 r →
        ∀ (a : Fin k → ZMod (HPow.hPow.{0, 0, 0} 2 r)),
          Exists.{1} fun col =>
            ∀ (x : Fin k → ZMod (HPow.hPow.{0, 0, 0} 2 r)),
              (∀ (i j : Fin k), Eq.{1} (col (x i)) (col (x j))) →
                Eq.{1} (Finset.sum.{0, 0} Finset.univ.{0} fun i => HMul.hMul.{0, 0, 0} (a i) (x i)) 0 →
                  ∀ (i : Fin k),
                    Dvd.dvd.{0} (HPow.hPow.{0, 0, 0} 2 (HSub.hSub.{0, 0, 0} r (Corpus.Green21.maxDepth a))) (x i).val

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record