Extend reconstruction past the decidable fragment — instantiation replay, and SOS certificates for the relax route

[maxinelevesque]

Extend reconstruction past the decidable fragment — instantiation replay, and SOS certificates for the relax route

Split out of the RFC-2 thread because it stands on its own: this is a trust-base improvement per clause and needs no presentation change to be worth doing.

The framing that reopened this

Scoping by what theorems forbid rather than by difficulty estimate:

theorem	forbids	does not forbid
Matiyasevich	a decision procedure for nonlinear integer arithmetic	checking any particular proof that exists
Gödel / Church	a complete procedure for provability	kernel-checking a given term
Goldfarb	decidable HO unification outside the pattern fragment	checking a term whose implicits are resolved

All three constrain finding proofs, not checking them. Kernel type-checking is decidable everywhere; RFC-1 already names its only real limit as KernelBudget — "decidable but non-elementary in cost" — which is a resource verdict, not a wall.

Nothing forbids reconstructing any proof that exists. What is forbidden is a complete procedure that always finds one.

Reconstruction is a checking problem, and search is untrusted by construction — which is exactly the architecture Reconstruct.lean already uses, where the SAT solver is a proof producer and the kernel evaluates the LRAT check.

Why the current paths are fragment-bound

Three reconstruction paths ship today, and they are mechanically quite different:

• QF_LIA — SmtExport.lean, generated by lean_smt_export.rs, discharged by smt through lean-smt to cvc5. cvc5 emits a proof; lean-smt replays it.
• QF_BV — no external solver at all. Lean's own bit-blaster and SAT solver, then an LRAT certificate checked by unsat_of_verifyActions, deliberately avoiding the native-evaluation axiom bv_decide uses.
• S₂.0 EPR — LRAT, via epr_reconstruct.rs with PinEprLrat / PinEprReplay.

The common shape: each replays a certificate produced by a complete procedure. The certificate exists precisely because the procedure terminates with either a proof object or a model. That is the real reason reconstruction currently rides on decidability — not because kernels need it, but because that is where certificates come from.

Proposal A — instantiation replay

A general Verus VC is not discharged by a decision procedure. It is discharged by quantifier instantiation — E-matching against triggers, or MBQI.

The observation that makes this tractable:

Once the instantiations are applied, the residual goal is quantifier-free — and quantifier-free is a fragment Thermite already reconstructs.

So instantiation is a reduction into solved territory. Better: the instantiations need no trust. If you replay them and the residual QF goal checks, the proof is valid regardless of how those instantiations were chosen. Quantifier instantiation is a proof producer, structurally identical to the role the SAT solver plays in the BV path. That the heuristic is MBQI rather than CDCL changes nothing about the trust story.

This is the same architecture with a wider front end, not a new kind of thing.

What is genuinely hard: Z3's proof objects use roughly forty rules, and several — th-lemma for arithmetic especially — are effectively "trust me" steps needing their own reconstruction. Objects for heavily-instantiated goals get large.

Honest scoping: quantified linear arithmetic plus EUF looks plausible. That is a large and useful region, not universal coverage.

Proposal B — SOS certificates for the relax route

I had written this off, and the reason I was wrong is worth stating: I assumed nlsat reconstruction meant replaying a CAD trace, which is impractical. That is the wrong certificate format.

For a universally quantified polynomial claim over ℝ — which is exactly what the relax route handles — the natural certificate is Positivstellensatz / sum-of-squares. If ∀x. p(x) ≥ 0 holds, there is an algebraic witness p = Σ σᵢ·mᵢ with each σᵢ a sum of squares, and checking one is polynomial identity verification: expand, compare coefficients. That is ring-level in Lean, and Mathlib already has the polynomial infrastructure via the lean-smt dependency.

Degree bounds are astronomical in the worst case. That is complexity, not impossibility, and certificates for real program obligations are typically low-degree.

The payoff is specific: r_relax_sound — the ℝ→ℤ bridge — is already kernel-proven. Only the real-side result is solver-trusted. Give it an SOS certificate and the entire relax route moves from solver + spine-lemma to fully kernel-checked, with Z3 leaving the trusted base.

Note this can be done independently of the solver that proved the claim — search for the certificate separately and check it. No dependency on Z3 emitting anything new.

What stays out of reach

Nonlinear integer arithmetic: Matiyasevich forbids completeness. But the relax route already routes through ℝ plus the proven bridge lemma, so the integer case is already structured as (real result) + (kernel bridge) — which is exactly the shape Proposal B completes.

Why this is worth doing on its own terms

Every clause it touches keeps its rung and improves its trust base — Z3 leaves the residual, exactly as engine.rs:130 describes for the BV path: "the SAT solver and LRAT converter are proof producers only: neither remains in the trusted base."

It also has a structural payoff for the assurance order discussed in #119, but that is a bonus rather than the argument. The argument is that a clause currently trusting ~500 kLOC of solver can stop doing so, and no theorem prevents it.