claimroutine

Circuit normalization into quadratic equations

Turns ff into quadratics qiq_i with a common rational zero iff ff has one
normal form step toward quartic and sum of squares
Claim·§7 Turing degree and a quartic normal form·inside corDegree 0' for rational solvability and quartic forms

Statement (paper)

Given f∈Z[X1,…,Xn]f\in\Z[X_1,\ldots,X_n], one can effectively construct a nonempty finite list q1,…,qs∈Z[X1,…,XN]q_1,\ldots,q_s\in\Z[X_1,\ldots,X_N] of integral polynomials of total degree at most two, in N=n+mN=n+m common variables Z=(X,Y)\mathbf Z=(\mathbf X,\mathbf Y) (where mm is the number of nodes of an arithmetic circuit evaluating ff), such that (∃x∈Qn) f(x)=0(\exists\mathbf x\in\Q^n)\ f(\mathbf x)=0 if and only if (∃z∈QN) ⋀i=1sqi(z)=0(\exists\mathbf z\in\Q^N)\ \bigwedge_{i=1}^s q_i(\mathbf z)=0, if and only if (∃z∈QN) ∑i=1sqi(z)2=0(\exists\mathbf z\in\Q^N)\ \sum_{i=1}^s q_i(\mathbf z)^2=0.

In plain English

From an integral polynomial ff in nn variables one can effectively build a nonempty list of integral polynomials q1,…,qsq_1,\ldots,q_s of total degree at most two in N=n+mN=n+m variables, where mm is the number of nodes of an arithmetic circuit for ff. The polynomial ff has a rational zero iff the qiq_i have a common rational zero, iff ∑iqi2\sum_i q_i^2 has a rational zero.

Why it's here

This is the reduction step behind both restricted problems in the parent theorem: it turns an arbitrary H10 instance over Q\mathbb Q into a system of quadratic equations by adding one variable per circuit node. The last equivalence is the standard fact that a sum of squares of rational numbers vanishes iff each term does, so the system collapses to a single quartic. The next claim uses this to give many-one reductions to the degree-four and sum-of-squares problems, which yields degree 0′0'.
Classified routine:
Standard Skolem-style degree reduction: introduce one auxiliary variable per arithmetic-circuit node so each gate becomes a degree-at-most-two equation, then combine the system into a single quartic via the sum-of-squares trick over an ordered field. This is a well-known folklore device in work on Hilbert's tenth problem.

Uses

Nothing else in the paper

Used by

claimQuartic and quadratic-sum problems have degree 0'

Sources

PaperOpen
Section
§7 Turing degree and a quartic normal form
Page
—
Label
—
Line
sections/07-consequences.tex:55
Leannot aligned

Phase 2 aligns this node to a Lean declaration.