Module verify 

Unified theorem verification — the single door.

Every public theorem entry point in the workspace funnels through prove_certify_check, so they all share one trust guarantee:

A proof is verified iff the backward chainer produced a derivation, the certifier turned it into a kernel term, and the kernel type-checked that term.

A derivation alone never counts as verified — verified == true is always backed by a [Term] that re-checks under [infer_type] in the returned [Context]. This core lives in the proof crate (not the compile crate) so both logicaffeine_language and logicaffeine_compile can reach it without a dependency cycle.

Structs

ConflictReport

The result of checking a rule set for an internal contradiction.

Definition

A user-introduced predicate definition (Rung 0a), expressed in the proof layer’s own vocabulary so logicaffeine_proof keeps its no-language-dependency invariant. Read as name(params) :↔ definiens.

DependencyGraph

The uses dependency graph among definitions and from a theorem to its definitions — the Rung 0b graph seed (each node a definition/theorem, each edge a uses). Direct edges only; transitive use is a query over this. This is the structure a mathscrapes node/edge compiles into.

LibraryResult

The outcome of proving one theorem in a library.

LibraryTheorem

One theorem in a dependency-ordered library: proved from its own premises plus the conclusions of the theorems it cites. This is the unit the multi-theorem driver discharges in citation order (the Euclid-graph engine).

VerifiedProof

Outcome of running a goal through prove → certify → kernel type-check.

Functions

check_derivation

Certify and kernel-check a derivation built EXTERNALLY (e.g. by the fast grid solver) against premises ⊢ goal, WITHOUT running the backward chainer. The trust guarantee is identical to prove_certify_check: verified is true only when the certifier produced a kernel term whose inferred type IS the goal type. So an external solver sits OUTSIDE the trusted base — it hands us a DerivationTree, the kernel re-checks it, and a wrong tree yields verified == false, never a false claim.

check_derivation_with_defs

Like check_derivation but with user Definitions in scope (Rung 0a), so an externally-built derivation of a definiens can certify against a goal stated with the definiendum — δ reconciles them at the root.

dependency_graph

Build the DependencyGraph for a set of definitions plus a theorem (premises + goal), recording which definitions each definiens uses and which the theorem uses. Pure, allocation-light, O(total expression size).

detect_conflict

Detect whether premises are jointly inconsistent, returning a kernel-checked proof of False and the indices of the clashing premises.

prove_certify_check

Prove goal from premises, certify the derivation, and kernel-check it.

prove_certify_check_bounded

Like prove_certify_check but caps the backward-chainer search depth, so a goal the kernel cannot reach fails FAST instead of exhausting the default depth. Keeps “prove-with-ours-first” cheap when answering a grid cell by cell: a shallow kernel attempt certifies what it can, then falls through to the oracle.

prove_certify_check_bounded_with_defs

The depth-bounded pipeline with user definitions (Rung 0a). Definitions are validated (recursion + lowering) up front, registered as δ-unfoldable kernel definitions in the context, then the goal is proved and kernel-checked. The engine still treats the definiendum opaquely during search (Stride 3 adds expand-for-search); δ reconciles the certified term with the folded goal type at the [finish_check] root.

prove_certify_check_with_defs

Like prove_certify_check but with user Definitions in scope (Rung 0a).

prove_library

Discharge a library of theorems in citation order. Each theorem is proved from its own premises plus the conclusions of the (already-proved) theorems it cites, so a citation graph is walked exactly like the scraped Euclid dependency graph. Results are returned in the INPUT order. A citation of an unproved/failed theorem simply isn’t available as a premise (so the dependent proof fails too).

prove_library_with_axioms

Like prove_library but with a shared axioms base in scope for every theorem — a named theory (e.g. the Tarski geometry axioms) on which the whole dependency graph is discharged.