Lean/Std Premise Index

A premise catalogue before proof search

A premise index is the catalogue a theorem-proving system reads before it tries to prove anything: the named lemmas and definitions it may cite, with enough metadata to retrieve the relevant ones. A premise index is the catalogue a theorem-proving system reads before it tries to prove anything: the named lemmas and definitions it may cite, with enough metadata to retrieve the relevant ones. lean_std_premise_index does not build such an index and does not run a prover. It takes a small public catalogue that was copied out of a private Ring2 premise-retrieval run and checks that the copy is faithful and metadata-only.

The component consumes a fixture of JSON inputs, opens the source artifact the catalogue claims to copy, and emits metadata-only result records. The component consumes a fixture of JSON inputs, opens the source artifact the catalogue claims to copy, and emits metadata-only result records. A pass means the public rows match the opened source row for row after a single allowed path rewrite, the six copied body files match their declared digests and line and byte counts, and none of the five things that would turn the catalogue into an answer key slipped in.

It reads metadata only. It never imports Mathlib, never runs Lean or Lake, and never prints a proof body. It reads metadata only. It never imports Mathlib, never runs Lean or Lake, and never prints a proof body.

Purpose

The value of a premise index for a benchmark sits one edit away from its danger. The same rows that tell a reader which standard-library facts are on the table would, with a proof body or an oracle-needed id attached, tell a solver exactly which lemmas it needs. The value of a premise index for a benchmark sits one edit away from its danger. The same rows that tell a reader which standard-library facts are on the table would, with a proof body or an oracle-needed id attached, tell a solver exactly which lemmas it needs. A loose copy is worse than no copy: it looks authoritative while leaking the answer.

So the question this component answers is narrow. Given that a real premise index already exists inside a private run, can a cold reader see its public shape and be sure the public shape is a faithful copy and not a hand-written stand-in? So the question this component answers is narrow. Given that a real premise index already exists inside a private run, can a cold reader see its public shape and be sure the public shape is a faithful copy and not a hand-written stand-in? The answer rests on opening the declared source and comparing, not on trusting a hand-maintained mirror.

How it works

run validates the first-wave fixture with negative cases included. run_index_bundle validates the exported bundle with the source-module manifest required. run validates the first-wave fixture with negative cases included. run_index_bundle validates the exported bundle with the source-module manifest required. Both call _build_result, which runs the checks below in order and sets status to pass only when there are no positive findings, no missing negative case, and no blocking secret-scan hit.

_validate_entries walks the eleven premise rows in the positive fixture. Each row must cite an Init/ Lean toolchain source ref, carry retrieval terms, and name a nonempty split drawn from train, dev, and test. _validate_entries walks the eleven premise rows in the positive fixture. Each row must cite an Init/ Lean toolchain source ref, carry retrieval terms, and name a nonempty split drawn from train, dev, and test. The index as a whole must carry at least ten rows and cover the namespaces Nat, Bool, List, and Iff. A row is rejected if it carries a Mathlib ref, a proof body, an oracle_needed_premise_ids field, or a duplicate premise id.

_validate_source_artifact is the check that makes the copy claim real. It reads the declared source_ref, recomputes the file's SHA-256, and compares it to the declared digest. _validate_source_artifact is the check that makes the copy claim real. It reads the declared source_ref, recomputes the file's SHA-256, and compares it to the declared digest. It then matches every public row to a source row by premise_id and compares signatures. The one permitted difference is a path rewrite: _normalize_source_ref turns a raw Lean toolchain path into a public lean-toolchain://.../Init/... reference so the reader sees where a lemma lives without seeing a private filesystem. A digest mismatch, a row-count mismatch, or a signature mismatch blocks the record.

_source_module_manifest_result checks the six copied body files: one normalized Lean/Std descriptor index plus five Ring2 body files. _source_module_manifest_result checks the six copied body files: one normalized Lean/Std descriptor index plus five Ring2 body files. For each it recomputes the target digest, line count, and byte count against the manifest, confirms the declared source file opens and matches its own digest, and requires body_copied true with body_in_receipt false. Exact copies must still equal their opened source. The body text stays out of every record.

The five expected negative cases are declared in EXPECTED_NEGATIVE_CASES. _build_result runs each negative input through the same entry and policy checks, collects the codes it actually observed, and blocks if any expected case was not raised. The five expected negative cases are declared in EXPECTED_NEGATIVE_CASES. _build_result runs each negative input through the same entry and policy checks, collects the codes it actually observed, and blocks if any expected case was not raised. A silent secret-exclusion scan over the inputs is the last gate.

flowchart TD inputs["fixture inputs premise_index, projection_protocol, index_policy, 5 negative cases, source_module_manifest"] entries["_validate_entries 11 rows, Init/ refs, namespaces, splits"] source["_validate_source_artifact reopen source, rehash SHA-256, compare rows by premise_id"] manifest["_source_module_manifest_result 6 copied body files by digest, line, byte"] gate["_build_result no findings + all negatives seen + clean secret scan"] record["metadata-only result record"] inputs --> entries inputs --> source inputs --> manifest entries --> gate source --> gate manifest --> gate gate --> record

Negative cases

The fixture ships five inputs that must be rejected, each mapped to its error code in EXPECTED_NEGATIVE_CASES: The fixture ships five inputs that must be rejected, each mapped to its error code in EXPECTED_NEGATIVE_CASES:

• mathlib_premise_forbidden raises LEAN_STD_INDEX_MATHLIB_FORBIDDEN;
• proof_body_leakage raises LEAN_STD_INDEX_PROOF_BODY_FORBIDDEN;
• oracle_needed_ids_leakage raises LEAN_STD_INDEX_ORACLE_IDS_FORBIDDEN;
• test_split_tuning_attempt raises LEAN_STD_INDEX_TEST_SPLIT_TUNING_FORBIDDEN;
• namespace_without_source_ref raises LEAN_STD_INDEX_SOURCE_REF_REQUIRED.

If any expected code is not observed, the run is blocked. These stay stable because the index is meant to be useful without becoming proof authority. If any expected code is not observed, the run is blocked. These stay stable because the index is meant to be useful without becoming proof authority.

Prior Art Grounding

This component borrows the closed-index discipline from formal-library indexing and premise-selection work. The Lean mathematical library anchors the library-as-corpus side. This component borrows the closed-index discipline from formal-library indexing and premise-selection work. The Lean mathematical library anchors the library-as-corpus side. LeanDojo and HOList anchor the need for premise metadata, retrieval splits, and theorem-proving environments a learning system can inspect. Premise ids, declaration names, namespaces, source refs, retrieval terms, split eligibility, and copied-body digests are public metadata here; proof bodies and oracle-needed ids stay outside the boundary. It does not import Mathlib or prove theorems.

Validation Result record Path

Run these from the public clone root without mutating durable result record or generated projection surfaces: Run these from the public clone root without mutating durable result record or generated projection surfaces:

./repo-pytest tests/test_lean_std_premise_index.py -q --basetemp=/tmp/microcosm_lean_std_premise_index_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

The focused test drives the runner over the fixture and the exported bundle: it asserts all five negative cases are observed, opens the real Ring2 source artifact, and rejects digest, row-count, row-signature, source-ref, source-module digest, and rehash-body-swap mutations. The focused test drives the runner over the fixture and the exported bundle: it asserts all five negative cases are observed, opens the real Ring2 source artifact, and rejects digest, row-count, row-signature, source-ref, source-module digest, and rehash-body-swap mutations. A pass means the copy was faithful and metadata-only on this input, not that any theorem is correct.