QF_NIA single-variable polynomial UNSAT carries an independently re-derivable refutation

Identifier: F:qf-nia-univariate-unsat-is-certified
Proof route: smt-term-level
External status: unknown
Axiom footprint: smtlib2.int-semantics, axeyum-ir.int-term-collector, axeyum-solver.i128-guarded-arithmetic, rational-root-theorem-over-Z

Recorded description

Every single-variable integer polynomial EQUALITY that axeyum decides unsat by a non-square discriminant, non-integral rational quadratic roots, or rational-root exhaustion emits a source-bound certificate carrying only integers, and that certificate re-validates against a FRESH PARSE of the original SMT-LIB text by an argument re-derived from the coefficients alone.

Formal statement

(declare-fun x () Int)
(assert (= (+ (* x x) x (- 1)) 0))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

qf-nia-univariate-unsat-is-certified-1

Kind: unsat-certificate
Status: checked

Supports: One named refutation reaches `outcome=verified` end-to-end. Anchored on the row rather than on a test-count line: `test result: ok` is true of a suite that produced no certificate at all, and this pattern is false unless a certificate was produced AND re-derived.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test certified_implies_revalidatable -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'nia_non_square_discriminant .*kind=unsat-int-univariate-poly .*certified=1 outcome=verified')" -ge 1

Evidence notes

Anchored on `certified=1 outcome=verified` in one row of `certified_implies_revalidatable`, which re-validates against a FRESH PARSE of the SMT-LIB text rather than the producing run's arena. That distinction is the whole point of the anchor: checking against the producer's own arena passes for any certificate, including one that merely copies the producer's conclusions. `UnsatQuantInstanceSet` shipped `certified=1` over a FAILED re-check on 2026-08-17 because its TermIds meant nothing in a second arena, and this suite exists because of it.

qf-nia-univariate-unsat-is-certified-2

Kind: unsat-certificate
Status: checked

Supports: The POPULATION, not one survivor. All three arguments -- non-square discriminant, non-integral rational roots, rational-root exhaustion -- must verify. A `grep -q` would still pass if two of the three regressed to `outcome=failed`, which is how a three-argument claim silently becomes a one-argument claim.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test certified_implies_revalidatable -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'kind=unsat-int-univariate-poly .*certified=1 outcome=verified')" = 3

Evidence notes

Count pinned at 3. Raising it is a new argument and must be deliberate; a fall is a regression. Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output.

qf-nia-univariate-unsat-is-certified-3

Kind: unsat-certificate
Status: checked

Supports: The strand's PRIMARY METRIC moved, not just a test passing. `docs/mathematics-2026-08/01-decide-vs-certify.md` asks, per area, whether a verdict comes with an artifact a third party can check; `QF_NIA` answered no. It now ranks band 1, `artifact already built`.

Checker command

out=$(python3 scripts/check-capability-assurance.py --rank --quiet 2>&1) && test "$(printf "%s\n" "$out" | grep -A1 'band 1' | grep -Ec 'QF_NIA')" -ge 1

Evidence notes

The exit status depends on the FINDING: `grep -A1 'band 1'` fails when QF_NIA sits under any other band, and the same command asserted against `band 3` exits 1 today -- so this discriminates rather than merely running. Deliberately NOT a claim that an external checker reads the artifact: band 1 means one could be pointed at it, and `checked_by` stays `SelfChecker` until one is.

Provenance

{
  "date": "2026-08-20",
  "established_by": "agent-capability-assurance",
  "source": "crates/axeyum-solver/src/nia_univariate_cert.rs (producer + independent checker + 13 white-box tests); crates/axeyum-solver/tests/nia_univariate_cert.rs (6 black-box tests); crates/axeyum-solver/tests/certified_implies_revalidatable.rs (the general obligation); commit 119a91c53"
}