Implement 2x using the polynomial system

Question

Your job is to implement \2ドル^x\$ using polynomials, such that in a way that for all integers \$x\$ and \$y\$, $$\exists(v_0,v_1,\dots)[P_1(x,y,v_0,v_1,v_2,\cdots) = 0 \land P_2(x,y,v_0,v_1,v_2,\cdots)=0 \land \cdots ]\iff 2^x=y$$

I will explain simultaneously how the score is calculated and what you can do to construct an integer polynomial group.

You can construct using: \$x, y, z\$ which are variables and \$a,b,c\$ are integer constants of your choice (can be any natural number), and \$F_1, F_2, F_3\$ are mathematical expressions, \$E_1,E_2,E_n\$ are equations and \$G\$ is an equation group. The number bewteen parentheses is the score, \$d_{constant}\$ is the size of the constant in decimal (if the constant is \2ドル\$ and it's used for an exponent of a variable, then its number length score is \0ドル\$ because you can do \$xx=x^2\$).

\$ \begin{aligned} (1)\ & F_1 \Rightarrow x \\[4pt] (d_a)\ & F_1 \Rightarrow a \\[4pt] (1 + d_a)\ & F_1 \Rightarrow F_2 + a \\[4pt] (2 + d_a)\ & F_1 \Rightarrow x^a \\[4pt] (2 + d_a + d_b)\ & F_1 \Rightarrow a x^b \\[4pt] (1)\ & F_1 \Rightarrow x F_2 \\[4pt] (1 + d_a)\ & F_1 \Rightarrow -a \qquad\qquad\qquad \qquad\text{(useless, probably)} \\[4pt] (1 + d_a)\ & F_1 \Rightarrow F_2 - a \\[4pt] (2)\ & F_1 \Rightarrow F_2 - x \\[4pt] (3 + d_a)\ & F_1 \Rightarrow F_2 - x^a \\[4pt] (3 + d_a + d_b)\ & F_1 \Rightarrow F_2 - a x^b \\[4pt] (2n + d_a + d_b + d_c + \cdots)\ & F_1 \Rightarrow x_1^a x_2^b x_3^c \cdots x_n^\omega \\[4pt] (2n + d_a + d_b + d_c + \cdots)\ & F_1 \Rightarrow a x_1^b x_2^c x_3^d \cdots x_n^\omega \\[4pt] (2n + 1 + d_a + d_b + d_c + \cdots)\ & F_1 \Rightarrow F_2 - a x_1^b x_2^c x_3^d \cdots x_n^\omega \\[4pt] (2)\ & F_1 \Rightarrow F_2(F_3) \\[4pt] (1)\ & F_1 \Rightarrow F_2 + F_3 \\[4pt] (4 + d_a)\ & F_1 \Rightarrow (F_2)^a \\[4pt] (0)\ & G \Rightarrow F_1 \land F_2 \land (\cdots) \land F_n \end{aligned}\$

And that's the scoring system. Try making an equation group such that: \$\forall x \in \mathbb{N_0}((F_1 = 0, F_2 = 0, F_3 = 0, \cdots) \land (x_1, x_2, x_3, \cdots , x_n, y \in \mathbb{Z}) \implies 2^x=y)\$

Here's a simplified example: if you want to force to make \$x=\mathrm{abs}(y)\$ or equivalently \$x=|y|\$, you can do:

$$ a^2+b^2+c^2+d^2-x\\x^2-y^2 $$

This has the score of \$\mathrm{score}(G) = 18\$. Note that all the polynomials above must be equal to zero to work. This works because a integer can be only positive (or zero) if and only if it can be represented by the sum of four squares, and since \$y^2=(-y)^2, y \in \mathbb{Z}\$, you can make both the absolute value of the numbers equal: \$x^2=y^2\$, and by forcing \$x\$ to be positive, it becomes clear that \$x=|y|\$

Try to do the same but for \2ドル^x=y\$. The lowest number of instructions, \$\mathrm{score}(G)\$, wins.

Some clarifications I want to tell:

• Using \$\mathrm{constant}^\mathrm{variable}\$ is obviously disallowed, you have to implement exponentiation with polynomials.

• The scoring system is like how you would implement the polynomials in a basic programming language with some exceptions: that the multiplication between variables (with power or not) don't count towards the score, the power costs one score (the operation), the parentheses cost two (for both, in other words, one for each one), using something like \$(F_1)\hat{}(2)\$ is totally fine because it acts like a programming language and not a strict polynomial that you have to expand to a form.

• Fmbalbuena: @Dingus Yeah, in fact it is impossible if you do \$P(x)=2^x\,ドル but that's not the challenge. The challenge is to find \$P_1,P_2,\cdots\$ (named \$F_1,F_2,\cdots\$ in this challenge) such that if \$P_1(x,y,v_1,v_2,\cdots)=0 \land P_2(x,y,v_1,v_2,\cdots)=0 \land \cdots\$ then that makes \$y=2^x\$ true. In fact, the integer solutions of \$x^2-2y^2=1\$ (Pell's equation) grow exponentially.
• Jonathan Allan: It's worth noting that Matiyasevič’s theorem tells us that this challenge is, indeed, possible, although the score would be huge unless we find some clever trick(s). (I don't think I am fit to take up such a challenge.)
• xnor: @Fmbalbuena I think you should explain what you say in your comment there within the challenge, because I think that's not clear to readers now.
• Fmbalbuena: @xnor There's a sentence in the challenge that explains the same thing as the comment.
• Fmbalbuena: @Dingus I attempted to clarify by adding a sentence, is it clear now or is it missing something?

Answer 1

Score 162

$$ \begin{align} y^2 (a^2 - 1) + 1 - x^2 = 0 & \text{ } & (14) \\ v^2 (a^2 - 1) + 1 - u^2 = 0 && (14)\\ t^2 (b^2 - 1) + 1 - s^2 = 0 && (14)\\ r y^2 - v = 0 && (7)\\ py \cdot 4 - b + 1 = 0 && (7) \\ a + q u - b = 0 && (6)\\ x + cu - s = 0 && (6)\\ k + 4 y (d - 1) - t = 0 && (11) \\ k + e - 1 - y = 0 && (7) \\ (y (a - 2) + m - x)^2 + ((f - 1)(a \cdot 4 - 5))^2 (-1) = 0 && (36) \\ 4 a - m - g - 5 = 0 && (8) \\ 2 + h - w = 0 && (5)\\ k + l - w = 0 && (5) \\ z^2 (w - 1)^2 (w^2 - 1) + 1 - a^2 = 0 && (22) \end{align} $$

This solution is taken from Martin Davis's article Hilbert's Tenth Problem Is Unsolvable, using the sets of equations in theorems 3.1 and 3.5. The proof for why this works is approximately fifteen pages, so I won't be replicating it here - Matiyasevič’s theorem, which draws an equivalence between solutions to Diophantine equations and the values of sets that can be enumerated by a program, and is the reason this challenge is solvable, relies on the exponential function being Diophantine, which took multiple decades to prove.

I've replaced the base \$n\$ in the given equations with \2ドル\$, and reformatted the equations to be polynomials that fit the challenge's spec. The scoring system is a bit weird - in particular, there's no way to subtract two formulas directly, and the scoring around them is weird - e.g. a - b previously had to be scored as (a) - b^1, or a + b(-1), although this has now been changed. I think I've done a reasonably good job, but it's possible there's more to be saved.

• Fmbalbuena: The mathematical expression x - y is now scored 3 points. I will not add a way to subtract two formulas directly, because the distributive property can be used to subtract formulas.
• Lucenaposition: are you sure that the there are no additional solutions where some of the variables are 0 or negative integers?
• emanresu A: @Lucenaposition I didn't actually notice that the challenge allows negative variables - it's likely that some of the variables can't have negative solutions, but I'm not sure how to prove that - so I would have to do some fiddling to see how few I can get away with forcing to be 1 + sum of four squares.