Lemma: Agent20_CollatzRound2_01a13459_E20_BinaryRank.binary_root_of_odd_linear

For any natural p,b,K with p odd, some natural a solves p*a+b=0 modulo 2^K. Proved by binary lifting; no primality assumptions or unproved axioms.

Exact formal statement

∀ (p b K : Nat),
  Eq.{1} (HMod.hMod.{0, 0, 0} p 2) 1 →
    Exists.{1} fun a =>
      Eq.{1} (HMod.hMod.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} p a) b) (HPow.hPow.{0, 0, 0} 2 K)) 0

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record