Determine the exact optimum of a degree-twelve quadratic module

Let x1,...,x12 be independent real indeterminates and gi=xi-xi^2. Define

C* = inf { C in R : x1*x2*x3*x4*x5*x6*x7*x8*x9*x10*x11*x12 + C = sigma0 + sum(i=1,...,12) gi*sigmai,
                   sigma0,...,sigma12 are sums of squares,
                   degree(sigma0)<=12 and degree(sigmai)<=10 for i=1,...,12 }.

Determine C* exactly and prove that the infimum is attained. Supply matching exact primal and dual certificates.

The primal certificate must give explicit polynomial bases and positive-semidefinite Gram matrices satisfying the identity at C=C*. The dual certificate must give a linear functional L on all polynomials of degree at most twelve such that L(1)=1, L(f^2)>=0 for every polynomial f of degree at most six, L(gi*h^2)>=0 for every i and every polynomial h of degree at most five, and L(x1*x2*x3*x4*x5*x6*x7*x8*x9*x10*x11*x12)=-C*.

All coefficients and positivity claims must be exact. Real algebraic coefficients are permitted. A decimal optimum, an approximate feasible SDP point, a numerical eigenvalue calculation, unequal upper and lower bounds, or a certificate for a merely feasible constant does not solve the task. The identity must hold as an ordinary polynomial identity over the reals; imposing xi^2=xi on the primal identity is not permitted.

No polynomial bases, matrices, candidate optimum, moment values, or active constraints are provided.

Deliverables: exact machine-readable primal and dual certificates, a derivation, and a verifier that checks all coefficient identities and positivity claims using exact arithmetic. The certificate representation may be chosen by the solver, as described in certificate_format.txt.
