# Exact Rational Sum-of-Squares Certificate

## Problem

`input/polynomials.json` defines THREE polynomials p1, p2, p3, each in
**5 variables of degree 6** with **integer** coefficients:

```
{"n_vars": 5, "degree": 6,
 "polynomials": {"p1": [{"exponents": [e1..e5], "coeff": c}, ...],
                  "p2": [...], "p3": [...]}}
```

meaning p(x) = sum over terms of c * x1^e1 * ... * x5^e5. The three
instances are structurally different (balanced, stiff, and flat-valley
landscapes); **every one of them must be certified** — the grade is the
minimum over instances.

For EACH polynomial: certify a **global lower bound** — find gamma as large
as you can, and *prove* p(x) >= gamma for all x in R^5 by exhibiting an
exact sum-of-squares certificate

        p(x) - gamma  =  z(x)^T Q z(x),

where z(x) is the vector of all 56 monomials of degree <= 3 (the exact
ordering is given in `input/basis.json`, and you must use that ordering),
and Q is a symmetric **rational, positive definite** matrix. Positive
definiteness is what turns the identity into a proof: it forces
z^T Q z >= 0 for every real x.

Everything is checked in **exact integer arithmetic**. There are no
numerical tolerances anywhere in this task: an answer is either a valid
proof or it is not.

## Required output

`output/solution.json` mapping each instance key to its certificate:

```
{"p1": {"den":    <positive integer>,
         "G":      <integer>,
         "Q":      [[<integer>, ... 56 entries], ... 56 rows],
         "x0_num": [<integer> x 5],
         "x0_den": [<positive integer> x 5]},
 "p2": {...}, "p3": {...}}
```

The first three encode the certificate: gamma = G/den and Q = Qint/den (the
same denominator for both). The last two encode a **witness point**
x0 with coordinates x0_i = x0_num[i] / x0_den[i], exact rationals.

The certificate proves min p >= gamma; the witness proves min p <= p(x0).
Together they **enclose** the global minimum, and the enclosure must be
tight: p(x0) - gamma <= 1e-5, checked in exact rational arithmetic (p has
integer coefficients and x0 is rational, so p(x0) is computed exactly).

Constraints on the encoding:

- **den <= 2^20 = 1048576.**  (A coarse rounding grid is part of the
  problem: you cannot escape by using an enormous denominator.)
- every integer must satisfy |v| < 2^220;
- Q must be exactly symmetric.

## Evaluation (exact; recomputed from your file alone)

1. **Identity.** For every monomial alpha of degree <= 6,
   `sum over ordered pairs (i,j) with z_i + z_j = alpha of Q[i][j]`
   must equal `den * p_alpha - G * [alpha == 0]`, as integers. Any
   violated equation fails the task.
2. **Positive definiteness.** Decided exactly by Sylvester's criterion:
   every leading principal minor of Q must be strictly positive. The
   minors are computed by fraction-free (Bareiss) elimination, so this
   test involves no rounding whatsoever.
3. **Tightness.** gamma = G/den is compared to the targets by exact
   rational arithmetic.

4. **Witness / enclosure.** p(x0) is evaluated exactly as a rational, and
   0 <= p(x0) - gamma <= 1e-5 is checked by exact rational comparison.

Per-instance targets (each = the instance's SOS optimum minus 2e-5,
compared by exact rational arithmetic):

    p1: gamma >= -13.816645      p2: gamma >= -86.681433
    p3: gamma >= -15.831777

Score 1.0: every instance passes checks 1-4 at its target.
Score 0.5: every instance has a valid exact certificate at its loose target
(p1 >= -13.917, p2 >= -86.781, p3 >= -15.932), with witnesses optional.
Score 0.0 otherwise (one bad instance sinks the submission).

There is no hidden reference solution: any certificate passing these checks
is accepted, and the checks constitute a complete proof of the bound.

## Constraints

- Use only Python 3 with NumPy and SciPy. Note that SciPy contains **no
  semidefinite-programming solver**; whatever optimisation you need, you
  must build.
- No network access, no package installation.
- Wall-clock budget: 2 hours on 4 vCPUs / 8 GB RAM.
- Write only under `output/`.