Two QF_NRA refutation certificates reconstruct to a kernel-checked Lean False over the CONSTRUCTED reals

Identifier: F:nra-refutations-reconstruct-over-constructed-reals
Proof route: kernel-lean
External status: unknown
Axiom footprint: creal-prelude.constructed-carrier, axeyum-lean-kernel.type-checker

Recorded description

Monomial-divisibility and degree-2 Positivstellensatz QF_NRA refutations each emit a Lean term whose type the trusted kernel infers to False, built over CReal (the Bishop setoid of regular rational sequences, trusted surface 0) rather than the axiomatized AxReal package, and classified as theory reconstructions rather than structural attestations.

Formal statement

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (= (* a b c d) 0))
(assert (not (= (* a b c d e) 0)))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

nra-refutations-reconstruct-over-constructed-reals-1

Kind: kernel-term
Status: checked

Supports: Nothing in the suite failed. Anchored on `0 failed` rather than on a test name plus `ok`, because the latter contains no digit or boolean and so survives every mutation the scaffolder applies — it would have gone into the ledger as a checker that cannot discriminate.

Checker command

out=$(cargo test -p axeyum-solver --features full --lib reconstruct::arithmetic 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'test result: ok\. [0-9]+ passed; 0 failed')" -ge 1

Evidence notes

Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output (`0 failed` -> `1 failed`).

nra-refutations-reconstruct-over-constructed-reals-2

Kind: kernel-term
Status: checked

Supports: BOTH reconstructions check over the CONSTRUCTED reals, not one. The two named tests build `CReal` explicitly via `try_new_over_constructed_reals_reporting`; `LraReconstructCtx::new()` would build `AxReal` and its 30 assumptions, and the terms would still infer to `False` there. Without pinning the count at 2, one route regressing onto the axiomatized carrier would leave this green.

Checker command

out=$(cargo test -p axeyum-solver --features full --lib reconstruct::arithmetic 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^test reconstruct::arithmetic::(zero_product|product_positivstellensatz)::.*constructed_reals \.\.\. ok$')" = 2

Evidence notes

POPULATION-ONLY, deliberately, and `--allow-population-only` was passed to say so: no mutation of the output moves the count. It catches a test disappearing or being renamed, which is the failure mode that matters here -- a carrier assertion silently dropped. It does not catch a value changing inside a surviving row; the `0 failed` row above covers that.

Provenance

{
  "date": "2026-08-20",
  "established_by": "agent-capability-assurance",
  "source": "crates/axeyum-solver/src/reconstruct/arithmetic/zero_product.rs (commit bc4b6f589); crates/axeyum-solver/src/reconstruct/arithmetic/product_positivstellensatz.rs (commit 71f1c29a0)"
}