Lean Correspondence

Lean Correspondence is a small, deterministic relationship kernel for independently governed Lean repositories. A record binds exact Git commits, files, declaration spans, Lean toolchains, dependency lockfiles, assumptions, adapters, and an executable witness. Verification produces a content-addressed receipt. It does not create authority over either repository.

Vela remains the authority, custody, replay, and local-Standing substrate. Foundry may later read Lean Correspondence reports as ordinary artifacts. This package does not depend on Vela, change Protocol/Core, establish scientific acceptance, or maintain a universal theorem graph.

Install and run

Python 3.12 and uv are the reproducible toolchain. Normal verification uses only local Git objects and the command named by a lean_command witness; it never fetches commits or packages.

uv sync --frozen
uv run lean-correspondence schema --output-dir schemas
uv run python scripts/build_fixture.py
uv run lean-correspondence verify \
  fixtures/minimal/generated/fixture.byte-identity.relation.json \
  --repo-root "fixture/source=$(pwd -P)/fixtures/minimal/generated/source-repo" \
  --repo-root "fixture/target=$(pwd -P)/fixtures/minimal/generated/target-repo" \
  --output fixtures/minimal/generated/receipt.json
uv run lean-correspondence recheck \
  fixtures/minimal/generated/fixture.byte-identity.relation.json \
  fixtures/minimal/generated/receipt.json \
  --repo-root "fixture/source=$(pwd -P)/fixtures/minimal/generated/source-repo" \
  --repo-root "fixture/target=$(pwd -P)/fixtures/minimal/generated/target-repo"
uv run lean-correspondence impact \
  --records path/to/records --changed relation-id

Canonical repository bindings contain only a source repository ID and exact commit. verify and recheck resolve those identities only at execution time through repeated --repo-root id=/absolute/path arguments. The supplied map must exactly equal the IDs required by the record and witness. Missing, duplicate, unknown, relative, symlink-resolved, dirty, or wrong-commit mappings fail closed. Verification reads committed blobs with git show; physical checkout and temporary-work paths never enter records, receipts, reports, manifests, or roots. Relation and receipt JSON reject unknown fields.

v0 vocabulary and states

The closed relation vocabulary is byte_identity, definitional_equivalence, implication, specialization, generalization, representation_transport, and unknown. A verified record must use a non-unknown relation, an executable byte_identity or lean_command witness, and a current invalidation status. Unknown or unproved claims remain candidate or unverified, with a none witness permitted.

Canonical roots are SHA-256 over UTF-8 JSON with recursively sorted keys, compact separators, and no floats. Receipts contain no clock or host field, so identical inputs regenerate identical bytes. The committed JSON Schemas are derived from the closed models.

recheck distinguishes source declaration changes, source changes outside the selected span, target changes, environment drift, witness failure, unchanged validity, and metadata-only record changes. The declaration hash is a source-span hash, not a claim that the kernel understands Lean semantics. Explicit dependency and witness edges power impact; closure is reverse-edge-only and reports exact source repositories and commits with authority_claim: none.

Fail-closed boundary

The kernel rejects missing Git objects, non-absolute or mismatched checkouts, dirty worktrees, symlinked checkout paths, unsafe object paths, changed toolchains or lockfiles, ambiguous declaration selectors, stale dependency roots, forged content or receipt roots, failed witnesses, malformed JSON, and unknown schema fields. A lean_command executes directly without a shell, from the selected clean repository, with a small environment allowlist and a bounded timeout.

Tests and release gates

uv run ruff format --check .
uv run ruff check .
uv run mypy
uv run pytest
uv run lean-correspondence schema --output-dir schemas
git diff --exit-code -- schemas

The adversarial suite mutates refs, worktrees, lockfiles, declarations, roots, receipts, witnesses, and schema fields. The fixture generator creates two independent deterministic Git repositories from fixtures/minimal/{source,target} without a network.

Before extracting a public repository or integrating a real case, require: an independent review of the exact commit and tree; reproduction of schemas, fixture repositories, receipt, and hostile tests from a fresh checkout; review of the declared witness command; and a separately qualified, commit-pinned source/target case. The reviewed calibration imports below satisfy those local gates; publication and any reviewer study remain separate decisions.

Reviewed calibration imports

The independently reviewed candidate packets from lean-proofs commit 148e18cce542f397ccb60b21a896ba063f6d6cca are retained byte-for-byte under source/reviewed-packets/. IMPORT.json binds the producer commit, tree, reviewed subtree, and review disposition. The original packet statements are historical evidence and are not silently updated. In particular, the old adapter reachability note remains in the packet even though 2654e42de2026de6cdb248ad5ed0f1c7d659c8fa is now reachable from fork/comparator-workspaces.

Materialize exact historical checkouts at any empty work root and deterministically regenerate the native records, receipts, historical recheck, and impact report:

work_root=$(mktemp -d /private/tmp/lean-correspondence-materialize.XXXXXX)
uv run python scripts/materialize_real_cases.py \
  --packet-repo /absolute/path/to/lean-proofs-at-148e18c \
  --formal-conjectures /absolute/path/to/formal-conjectures-object-source \
  --lean-eval /absolute/path/to/lean-eval-object-source \
  --work-root "$work_root"

uv run lean-correspondence verify \
  cases/records/erdos-730.affirmative-rhs-defeq.relation.json \
  --repo-root williamjblair/lean-proofs=/absolute/path/to/lean-proofs-at-148e18c \
  --records cases/records

uv run lean-correspondence verify \
  cases/records/oeis-303656.fc-to-leaneval-generated-lineage.relation.json \
  --repo-root williamjblair/lean-proofs=/absolute/path/to/lean-proofs-at-148e18c \
  --repo-root google-deepmind/formal-conjectures=/absolute/path/to/fc-at-9f5ee77 \
  --repo-root leanprover/lean-eval=/absolute/path/to/lean-eval-at-7699436 \
  --records cases/records

uv run lean-correspondence recheck \
  cases/records/oeis-303656.historical-source-transport.relation.json \
  cases/receipts/oeis-303656.historical-source-transport.before.receipt.json \
  --repo-root williamjblair/lean-proofs=/absolute/path/to/lean-proofs-at-148e18c \
  --repo-root google-deepmind/formal-conjectures=/absolute/path/to/fc-at-81e700d \
  --records cases/records

uv run lean-correspondence impact --records cases/records \
  --changed oeis-303656.historical-helper-rename-defeq

The materializer is deliberately local and offline. It reads already available Git objects, creates detached exact checkouts beneath the caller-selected work root, and requires the exact reviewed packet worktree with its existing Lean build environment. A committed no-shell wrapper receives the verified runtime repository map through a process environment variable and invokes the two Lean witnesses or frozen packet verifier. It does not fetch, modify a source worktree, or run the original generator. The retained request, response inventory, packet verifier, and independently reviewed frozen replay are the bounded generation evidence.

The path-diversity gate runs that materialization twice from distinct exact source and work locations, then byte-compares every record, receipt, recheck report, impact report, ROOTS.json, and MANIFEST.sha256:

uv run python scripts/check_path_diversity.py \
  --packet-repo-a /absolute/path/a/lean-proofs-at-148e18c \
  --packet-repo-b /absolute/path/b/lean-proofs-at-148e18c \
  --formal-conjectures /absolute/path/to/formal-conjectures-object-source \
  --lean-eval /absolute/path/to/lean-eval-object-source \
  --work-root-a /absolute/empty/work-a --work-root-b /absolute/empty/work-b \
  --output-root-a /absolute/empty/output-a --output-root-b /absolute/empty/output-b

Both lean-correspondence console commands are installed package artifacts. One local review environment retained a stale editable console script after the wrapper entry point changed; this is an installation issue, not record drift. The release gate therefore builds a wheel and installs it into a fresh, non-dot-prefixed virtual environment before reproducing the CLI and real witnesses. Running uv sync --frozen also refreshes the development environment.

Erdős 730 relates only the two affirmative-RHS adapter propositions in the reviewed Lean witness. The complete Formal Conjectures answer(sorry) ↔ S.Infinite declaration is expressly outside the relation. OeisA303656 records deterministic source-context-to-generated-Challenge lineage and a separate exact historical helper-rename equivalence. The generic recheck correctly reports the historical source bytes as source_semantic_change; only the dependent Lean witness supports the narrower meaning_preserved_with_witness conclusion. The source theorem and generated Challenge remain open and contain sorry.

These two cases and the packet's two recorded-not-reproduced environment failures are calibration fixtures. They are not held-out evidence. A future reviewer study must use separately selected cases and must remain NO-GO until its own protocol is preregistered and passes review. Nothing in this repository authorizes a study, outreach, publication, or an acceptance decision.

Non-goals and v0 limitations

• No database, daemon, web service, remote fetch, provider/model inference, or outreach.
• No Vela or Foundry repository, dependency, custody, Standing, or acceptance semantics.
• No automatic theorem matching, universal graph, transitive scientific inference, or trust merge.
• No Lean parser or proof-kernel reimplementation. Declaration selection is a strict lexical span; a lean_command witness is responsible for Lean checking when equivalence is not byte identity.
• No sandbox for witness commands. Records and commands must be reviewed before execution.
• Environment roots cover the exact files listed in each record; v0 does not discover transitive package state automatically.