No integer squares to minus one

Identifier: F:no-integer-square-is-minus-one
Proof route: smt-term-level
External status: proved
Axiom footprint: axeyum-ir.integer-arithmetic-semantics, axeyum-solver.single-variable-polynomial-collector, negative-discriminant-quadratic-root-theorem

Recorded description

There is no integer x with x * x = -1.

Formal statement

(assert (forall ((x Int)) (not (= (* x x) (- 1)))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

autogenesis-operation-0cb40006d9fc2a83

Kind: unsat-certificate
Status: checked

Supports: There is no integer x with x * x = -1.

Checker command

python3 scripts/check-autogenesis-fact-operation.py --fact artifacts/facts/F-no-integer-square-is-minus-one.json

Evidence notes

Derived from a clean-commit typed execution receipt. The registered fact-operation checker replays the exact source artifact and requires its fresh-arena certified result; no caller-authored route, footprint, checker, or shell command is accepted.

Provenance

{
  "date": "2026-08-17",
  "established_by": "axeyum-autogenesis execution 87a53dd4bc892ad6da1331fb41d5afba732d80485037b4ed5b1f33c387f9f519",
  "prior_art": [
    {
      "date": "2026-08-17",
      "establishes": "the proposition is valid",
      "oracle": "z3 -smt2 artifacts/facts/smt2/neg-no-integer-square-is-minus-one.smt2",
      "result": "unsat"
    }
  ],
  "source": "authored by the skolem-cert lane as the replacement negative control for scripts/check-smt-evidence-certified.py; statement written here, not copied"
}