Undeclared Library Prior Classifier

Declared versus undeclared library priors

It answers one question about a Lean-accepted proof: did the candidate cite a known library symbol outside the premises its recipe allowed? A theorem prover can return a proof that Lean accepts and still break the rules of the evaluation it ran under. The usual way this happens is quiet: the proof reaches for a library lemma the recipe never put on the table. The symbol is real and the proof is sound, but the run used a fact it was not allowed to assume. This component answers one question about that gap. Given the premises a candidate was allowed to use and the qualified symbols it actually reached for, did it cite a known library symbol outside the allowed set?

It works only from a copied premise index and pre-extracted observations, never running Lean or reading the proof, with the allowed set closed by construction from premise rows. It works only from a copied premise index and a list of symbol observations that were extracted beforehand. It does not run Lean, it does not read the proof body, and it does not treat the standard library as an implicit allowlist. The allowed set is closed by construction: a symbol is admissible because a premise row names it, never because it happens to exist in Lean's standard library.

The public fixture's 11 premises and three observations classify to one undeclared-prior escalation, one budget-violation retry, and one advisory none, each named with its rule and class. The public fixture carries 11 premise rows across four namespaces (Bool, Iff, List, Nat) and three symbol observations. Running it classifies one observation as UNDECLARED_LIBRARY_PRIOR routed to bridge_escalate, one as PREMISE_BUDGET_VIOLATION routed to retry, and one as an advisory NONE. The written records name each symbol, the premise rule it came from, and the class that was computed.

Purpose

Compiling does not mean in-recipe

A checked proof is not a proof that stayed inside the allowed building blocks, and a loose check cannot tell an in-recipe proof from one that borrowed an out-of-recipe lemma. The problem is that "the proof checked" does not mean "the proof stayed inside the allowed building blocks." A loose check that trusts the prover's sign-off, or that admits any symbol found in the standard library, cannot tell an in-recipe proof from one that quietly borrowed an out-of-recipe lemma. Both compile. Both look sound.

Budget breach kept apart from residual breach

An explicit budget breach from a disallowed premise id is kept distinct from a residual breach using an undeclared known symbol, with the budget case taking precedence. The component also keeps two failure modes apart. An explicit budget breach, where the candidate names a premise id the recipe did not allow, is not the same as a residual breach, where the candidate used a known symbol that turns out to be undeclared. The first is settled directly from the cited ids and takes precedence. The second is what the symbol comparison is for. Folding both into one class would either over-escalate honest retries or let genuine out-of-recipe library use pass as a budget note.

How it works

Two entry points into _build_result

run builds the fixture result with negatives included, and run_symbol_bundle runs the same builder over an exported source-body bundle and can reuse a fresh prior record. The fixture entrypoint is run. It calls _build_result with the fixture input mode and negative cases included, then _write_receipts. The exported-bundle entrypoint is run_symbol_bundle, which runs the same builder over an exported source-body bundle and can reuse a fresh prior record. Inside _build_result the stages run in this order.

Loading inputs and the secret scan

_load_payloads reads the four inputs plus seven negative-case files, and scan_paths runs a secret-exclusion pass before the four validators run. _load_payloads reads the four input files (projection_protocol.json, premise_index.json, symbol_observations.json, classifier_policy.json) plus the seven negative-case files. scan_paths runs a secret-exclusion pass over those inputs and records a blocking hit count. Then four validators run.

Validating projection, premises, and policy

Three validators check the projection's refs and digests, require every premise row to carry an id, qualified name, and source ref, and pin the symbol regex and review outcomes. validate_projection_protocol checks that the projection cites real source refs, source pattern ids, target refs, and source digests, and that any omitted proof or provider material carries an omission record. validate_premise_index reads the premise rows, requires each to have a premise id, a qualified theorem_or_def_name, and a public source ref, and reports the premise and namespace counts. validate_classifier_policy requires the declared qualified-symbol pattern to equal QUALIFIED_SYMBOL_RE (the regex over the Nat, List, Bool, Iff, and Eq namespaces), the undeclared review outcome to be bridge_escalate, the budget review outcome to be retry, and it rejects any policy that sets proof_bodies_allowed true.

_classify_row computes the class with precedence

_classify_row maps cited premises to symbols, finds the known ones outside the allowed and cited sets, and applies budget-over-residual precedence, flagging any drift from the asserted class. validate_symbol_observations is the classifier. For each observation it calls _classify_row, which is where the rule lives. _classify_row reads allowed_premise_ids and cited_unallowed_premise_ids, maps them through the premise index to their symbols, extracts the observed qualified refs, and keeps the known ones (those a premise row names). The undeclared set is the known symbols that are neither allowed nor already cited as unallowed. Precedence is explicit: if cited_unallowed_premise_ids is present the row is PREMISE_BUDGET_VIOLATION with retry; otherwise a non-empty undeclared set is UNDECLARED_LIBRARY_PRIOR with bridge_escalate; otherwise the row is NONE and advisory. _classify_row then compares the observation's own asserted class against the recomputed one and records a finding on any mismatch, so the public assertion cannot drift from the premise-index computation.

The exported bundle's provenance check

For the exported bundle validate_source_module_manifest rejects in-result record bodies and verifies each source body against its digests, counts, and anchors as provenance, not a second proof. For the exported bundle, validate_source_module_manifest checks source_module_manifest.json, rejects manifest-level or row-level body_in_receipt: true, and verifies each declared source-body import against its source and target digests, line counts, byte counts, and required anchors. This is a provenance check on copied bodies, not a second proof.

Result records and the compact card

_write_receipts writes the result, board, validation, and sign-off records, and result_card projects a pass or fail card that omits the heavier evidence. _write_receipts writes the result, board, validation, and sign-off records. result_card projects a compact pass or fail card that omits the premise rows, classification rows, source digests, secret-scan detail, and scope limit body, so the card can be shown without exporting the heavier evidence.

flowchart TD inputs["Copied premise index and symbol observations"] policy["Classifier policy regex and outcomes"] classify["_classify_row compute allowed vs undeclared"] budget["cited_unallowed_premise_ids present"] residual["Known symbol outside allowed set"] clean["Allowed or no known undeclared symbol"] retry["PREMISE_BUDGET_VIOLATION route retry"] escalate["UNDECLARED_LIBRARY_PRIOR route bridge_escalate"] advisory["NONE route accept_as_advisory"] records["Result, board, validation, sign-off records"] inputs --> classify policy --> classify classify --> budget classify --> residual classify --> clean budget --> retry residual --> escalate clean --> advisory retry --> records escalate --> records advisory --> records

Negative cases

Seven negative cases and their codes

Seven negative cases each carry a code the run must observe, from leaked proof bodies and non-public refs to correctness overclaim, missing escalation, precedence violations, and false positives. The fixture ships seven negative cases in EXPECTED_NEGATIVE_CASES, each with an error code the run must observe. proof_body_leakage must raise SYMBOL_CLASSIFIER_PROOF_BODY_FORBIDDEN: observations may carry hashes and extracted refs, bounded evidence bodies. private_source_ref_leakage must raise SYMBOL_CLASSIFIER_PRIVATE_SOURCE_REF_FORBIDDEN. theorem_correctness_overclaim must raise SYMBOL_CLASSIFIER_THEOREM_CORRECTNESS_OVERCLAIM, because a library-prior classifier is not theorem-correctness authority. missing_escalation_for_undeclared_symbol must raise SYMBOL_CLASSIFIER_UNDECLARED_LIBRARY_PRIOR_NOT_ESCALATED when an undeclared symbol is not routed to bridge_escalate. premise_budget_precedence_violation must raise SYMBOL_CLASSIFIER_PREMISE_BUDGET_PRECEDENCE when a cited-unallowed row is instead escalated as a residual. allowed_symbol_false_positive must raise SYMBOL_CLASSIFIER_ALLOWED_SYMBOL_FALSE_POSITIVE when a symbol already admitted by allowed_premise_ids is quarantined. unqualified_symbol_overclaim must raise SYMBOL_CLASSIFIER_UNQUALIFIED_SYMBOL_OVERCLAIM when an unqualified token is used to support the qualified library-prior class. A run that fails to observe any expected case is blocked.

Prior Art Grounding

Premise control and library-aware proof search

It sits in the Sledgehammer and Mathlib lineage of premise control, turning the observation that accepted proofs lean on large libraries into a boundary check on out-of-recipe symbols. This check sits in the formal-methods lineage of premise control and library-aware proof search. Isabelle's Sledgehammer makes relevant-fact selection an explicit part of automated proof search, and Lean and Mathlib practice makes clear that accepted proofs can depend on a large library context. The component turns that observation into a boundary check: an accepted artifact is not enough if it quietly used symbols outside the declared premise set. It classifies the symbol-budget breach without judging whether the theorem is true.

• Isabelle Sledgehammer and relevant-fact selection: https://isabelle.in.tum.de/doc/sledgehammer.pdf
• Lean community Mathlib overview: https://leanprover-community.github.io/mathlib-overview.html
• Lean 4 tactic and proof environment context: https://lean-lang.org/theorem_proving_in_lean4/Tactics/

Validation Result record Path

Run from microcosm-substrate:

What a pass certifies

A pass means the fixture still classifies 11 premises and three observations into the expected three classes, the negatives are observed, the secret scan is clean, and the projection edges hold. A pass means the fixture still classifies 11 premises and 3 observations into one undeclared-library prior, one premise-budget retry, and one advisory case, the seven negative cases are observed, the secret-exclusion scan has no blocking hits, and the generated projection reports Mermaid available_from_capsule_edges, Atlas linked_from_capsule_edges, and 19 relationship edges. The validation result records written by _write_receipts carry the same counts and the authority flags. A pass is bounded classifier evidence, not launch or whole-system correctness.