Source-backed substitution experiment
Status: native-checked source-backed type transport, integrated as an optional layer in the compiled proof reader. Earlier projection packages remain immutable.
The previous projection extractor copies the complete structure operand into a
second expression table. A synthetic operand with 196,617 stored nodes exceeds
that table’s 32,768-node bound even though the selected field has type Nat.
This is a serialization boundary, not rejection of the term by Lean.
Representation
ProofAtlasSourceReferences/2 stores ordinary kernel-expression templates and
ordered substitution slots bound to exact source occurrences. Slots are extra
de Bruijn variables in the template environment, after the original context.
They are not another Expr constructor, an inferred type, or a new proof step.
The original source packet stays separate.
For a primitive projection, the anchors are the structure operand and its application-spine arguments, in source order. Collection crosses no binder. Lean 4.33.1 checks the selected projection, its normalized structure type, constructor parameters, preceding projections and selected field conversion. It then replaces exact contextual anchor expressions with fresh variables. Substituting the original expressions back must recover every native expression structurally, including binder names and annotations. Each anchor must also roundtrip through the original lexical context. A changed packet fails native comparison before producing any evidence.
source_reference_view.cjs performs delayed, simultaneous, capture-avoiding
substitution. Its indexed graph interface exposes only the twelve existing
kernel kinds. Source subgraphs stay borrowed. External variables are lifted
under template binders; their internal binders stay intact. Source counts and
scope requirements come from the already validated source table. Template
counts are computed over memoized states. Borrowed identities let comparison
skip an identical source region without enumerating its occurrences or copying
its stored nodes.
ProofAtlasGeometricScene/9 gives this transport its own namespace. Template
roots and hashes, arguments, explicit anchor routes and original context remain
attached. Computed parent routes never become source occurrences. Borrowed
descendants resolve through an anchor route plus their local source path.
Without supplied anchor routes, occurrence provenance is explicitly unavailable.
The ordinary cut, binder and application rules retain exact frontier accounting.
Template descendants acquire no new kernel typing judgment.
Checked finite cases
| Own synthetic case | Source nodes | Template nodes | Virtual nodes during checks |
|---|---|---|---|
| Independent value field | 196,617 | 4 | 34 |
| Dependent proof field | 196,626 | 8 | 35 |
| Dependent function field | 196,627 | 12 | 39 |
| Dependent function capturing the outer variable | 196,634 | 12 | 41 |
The native suite checks 20 projection occurrences in 19 declarations, 124 bounded cuts, 47 scope-link appearances and two contexts for a shared projection node. All 98 comparisons with materialized native expression roots from the existing extractor pass. The validator rejects 205 altered evidence records; Lean independently rejects a changed source packet. Thirty-five small delayed substitutions match an independent tree implementation, including shadowing, external variables and let scopes. A separate guarded access trap checks that an identical borrowed root can be counted and compared without a source scan; that mock graph is not a native proof or a corpus-size benchmark.
These measurements establish that this prototype avoids the observed second table copy in these finite cases, including dependent fields and an open context. They do not establish general asymptotics, human comprehension or performance on AI theorem-solving proofs. The large operands contain balanced arithmetic data; their proofs are reflexivity constructions.
Bounds and remaining work
This transport currently supplies projection observations. Source-backed lambda and application judgments are not yet implemented; their existing type-table bounds remain. The source packet is still loaded and validated in full. This experiment does not implement packet paging. Templates and metadata each retain a 32,768-node bound; views default to 65,536 virtual descriptors, 131,072 property evaluations and depth 512. Comparison defaults to 131,072 pairs. Limits fail explicitly. Anchor discovery is currently limited to a projection operand and at most 128 application arguments; a large unmatched native type can still exceed the template bound. Success does not imply arbitrary sharing/context coverage.
The reader loads immutable sidecars with a 16 MiB decoded limit, verifies the package and template/metadata hashes, and serializes loads. Aborted or stale selections are discarded. Ordinary type records supply enclosing introductions and applications. A source-backed projection supplies its exact result and structure-input observations; fields without this evidence retain source layout.
The released inventory has 241 sidecars: 222 frozen-corpus packets with 229 projection representatives, plus nineteen selected own control packets with 20 projection queries. The control edition is a predetermined subset of its fixture module, not a complete fixture-module inventory. Its large open-context case is available in the compiled reader.
Selecting a field exposes optional source-backed result, expected-field and structure-type views. Native text is collapsed separately from the bounded diagram. A borrowed node opens its exact original occurrence; external variables retain their recorded lift under computed binders. Local inspection retains the source selection. Computed parents have no invented source route or additional inferred type. Syntax comparisons require aligned contexts; they do not establish semantic equality between different environments.
The package audit checks all 249 selected projection queries, 996 bounded type cuts, 392 source-jump appearances and 1,245 corruptions. The native control suite independently replays all compiled fields for the nineteen public controls. Browser checks cover exact source navigation under a dependent function binder, corrupt metadata, cancellation, desktop/mobile layout and both themes. These are finite representation and interaction checks. Broader context coverage, source paging and independently sourced AI proof evaluation remain open.
Reproduction
From the repository root:
node scripts/test-proof-atlas-source-references.cjs
node scripts/test-proof-atlas-source-reference-packages.cjs
node scripts/test-proof-atlas-reference-loading.cjs
python3 research/proof-atlas/verify_source_references.py /path/to/lean-4.33.1 --reserve-gib 30
The native runner builds only the repository’s own synthetic fixture. It does
not read or rebuild private Lean projects. It writes native outputs, source and
module hashes, check results and operational records to its private temporary
directory. The portable finite check summary is in source-reference-results.json.