Let be the least number of binary additions, subtractions and multiplications required to construct from and , with reuse of intermediate values. We show that, for every sufficiently large integer , some positive integer satisfies The proof combines unconditional results of Lenstra, Pila and Pomerance on smooth numbers in short intervals and on orders of genus-two Jacobians with a five-parameter family carrying a rational divisor class of infinite order. We encode rational divisor arithmetic, including the tests determining its branches, by a nonzero division-free integer circuit. A common finite sampling space yields circuits whose outputs collectively contain every prime at most , and repeated squaring supplies the required factorial valuations. The circuit bound includes the cost of constructing all integer parameters. This work was carried out with assistance from the UniMath model, developed by UniDT (Shanghai) Co., Ltd., and GPT-6.1 Sol.

生成讲解博客的中文版本

生成AI智能校验的中文版本