Checked context modules

Checked context modules

Status: integrated prototype in the existing compiled reader. Source-shape sharing remains a distinct syntax layer. Typed-module evidence covers the finite own-control observations and three separately selected AI-proof routes in the ordered projection extension below.

A term’s source-variable links do not define its typing interface. For example, a proof hypothesis h : p mentions only h as a term, while its recorded type requires p. A retained let definition can also require an earlier variable through its value. ProofAtlasDependentInterface/1 begins with the free context slots of the selected term and its recorded type, then closes that set under selected header types and let values. Headers use their pre-binder context. Original order, constructor, visibility, universe namespace and source routes remain attached.

Dependency edges have four distinct roles: term-support, recorded-type-support, binder-type and let-value. Edge access returns at most sixteen edges per page with an exact total. This operation is syntactic. It does not establish logical necessity, new typing or shared typing. Missing or unresolved support is rejected.

Module rule

The native producer closes a selected term and expected type with an ordered subset of its source context. Assumptions become lambda/Pi pairs; definitions remain lets rebuilt with nondep=false. It checks the closed term at the expected type, applies the closure at the original context and kernel-checks conversion to the original selected term using Eq.refl.

Two uses share a module only when their closed terms, closed expected types, context-entry counts and let/assumption patterns match exactly within the same source declaration and compiled environment. Every additional use receives native instantiation and conversion checks. Retained definitions are not freely supplied arguments: records distinguish contextEntryCount, argumentCount and letSlots. Original occurrences, actual arguments, binder identities and root observations remain distinct.

The context boundary matters. Closing an entire function, its open body and a more deeply open body can yield identical closed syntax. Different interfaces remain separate modules. This rule does not quotient by arbitrary definitional equality, proof irrelevance, universe renaming or cross-declaration equivalence.

Geometry and navigation

ProofAtlasGeometricScene/10 draws the same constructor glyphs, ordered ports, binder links, telescopes and application spines as existing scenes. It has separate checked-module-term and checked-module-type categories in the checked-context-module namespace. A cut has at most 64 vertices and depth six; defaults are 32 vertices and depth three. Retained plus hidden occurrences account for the selected computed subtree. Root typing evidence does not supply inferred judgments for descendants.

createModule requires a previously authenticated and validated closed module graph and native provenance. It is a geometry constructor, not a browser kernel. The package hash, producer/request/output hashes, compiled environment and original source hashes qualify the module. A module path is a computed path, never an original source occurrence.

locate derives a separate per-use inverse map:

Computed variable links remain links to computed binders. Following the inverse map must recover the original binding in the selected use, even when source indices or binder targets differ between uses.

Finite evidence

Fifteen own declarations supply 594 exact native observations, 313 closed modules and 281 additional checked instantiations. Twelve declarations are the existing public closed-context controls. Three additional controls exercise proof reuse across unused binders and preservation of module boundaries. Three proof-valued groups span different source node IDs and old context classes. Three pairs of identical closed term/type syntax retain different context boundaries.

An independent reconstruction of the source term, type and reordered header expressions matches all stored module term/type graphs. Geometry checks cover 5,634 cuts and 6,860 inverse mappings, including 563 original-source variable links and 441 raw-type variable links. Sixty-five geometry/provenance/limit alterations must be rejected. A fresh own-control replay matches all 594 stored entries and rejects 31 deliberately omitted required context entries. These are finite checks, not a proved Lean metatheory, a portable standalone kernel certificate, semantic compression or a comprehension result.

The interface operation is also independently checked on 743 recorded observations: the 594 own observations and 149 existing AI-attributed observations in lean_workbook_plus_6206. All 149 AI source/scope-paged interfaces match the full-source reference with a source cache capped at 4,096 tuples and a scope cache capped at sixteen entries. The original context-type package is separately resident. Three selected AI routes have separate reduced-context native checks in the ordered projection extension below. The interface computation does not confer typing on the other routes. These cache bounds do not describe total browser memory.

Data and reproduction

context-modules-manifest.js pins fifteen compressed compiled-observation packages and three additional compiled source packets. Existing twelve source packets retain their existing hashes. Metadata-only projection of the three new source packets records both their public index hash and original native packet hash; expression constructors, payloads, ordered edges and roots are unchanged. Each package is capped at 8 MiB decoded and each native graph at 32,768 stored nodes. Original research proof scripts, private source projects and raw native logs are excluded. The replay generates only own synthetic fixtures and rebuilds no private project or Mathlib.

node scripts/test-proof-atlas-dependent-interfaces.cjs
node scripts/test-proof-atlas-context-modules.cjs
python3 research/proof-atlas/context-modules/verify_controls.py --lean lean

Reader

Open an exact source occurrence and choose Show checked context module. Term and expected-type views reuse the existing constructor renderer, with visible variable/declaration captions, zoom, pan, keyboard navigation and a module-root control. Changing an original use preserves the selected computed region and changes its inverse map. Source jumps are explicit. Raw type-body selections open their native type graph; they never acquire invented proof-source routes. Header dependencies have separately paged field labels. Retained let definitions remain distinct from callable assumptions.

The optional loader authenticates a package of at most 8 MiB decoded, checks its source/environment and finite native inventory, and retains one prepared selection. Source-dependent preparation and inverse maps run through the source owner. Small own packets use a support table capped at 4,096 nodes; a paged support callback is accepted separately. Closing or changing a proof cancels its view. Failed optional data/assets leave the source reader available and support retry. Missing routes remain explicitly unsupported. Original context-type packages and other reader data retain their separate bounds; this is not a total browser-memory bound.

The shared renderer now preserves the actual term/type component root. Its validator hash was updated in the native-page catalogue; existing native query and type-graph bytes are unchanged. Browser checks cover original uses with different binders, local refinement, exact source and native-type binding jumps, let values, universe namespaces, delayed maps/scripts, failed package retry and four desktop/phone theme/accessibility combinations. Existing source-sharing, beta, context-type, native-page and complete-library checks remain separate regressions. No blog update accompanies this implementation.

node scripts/test-proof-atlas-context-module-loading.cjs
# After the production site build:
node scripts/test-proof-atlas-context-modules-browser.cjs

Source-backed full-context modules

The same reader control also supports the existing full-recorded-context native observations. It borrows the original term, header domains and let values from authenticated source pages, and borrows the separately recorded raw type graph. New lambda/Pi/let wrappers close the term and its expected type. New lets use nondep=false. The original context order is retained; this operation supplies no newly minimized typed interface.

ProofAtlasSourceContextModuleScene/1 uses the same constructor glyphs, ordered fields, binder telescopes and application spines as the materialized module view. Term and expected-type components have separate roots. Default cuts contain at most 32 drawn vertices and depth three; the hard limits are 64 and six. Retained plus hidden occurrences account for the selected computed region. Native root evidence does not supply additional typing for a focused descendant.

The computed class is qualified by its canonical native observation, source/environment and evidence hashes. Switching an original use preserves that computed path. A separate inverse map selects the use’s original header, term or raw-type occurrence. Raw types retain their native-type namespace; Γ links return to exact original binders. Selected-use header captions are captured independently of canonical binder identities. Different context-entry boundaries remain separate classes. The method uses recorded canonical-to-target kernel checks and structural equality of raw expected types; it creates no new native judgments or arbitrary unqueried-route transport.

The existing AI package has 149 exact observations in 128 full-context classes, with 21 recorded alternate instantiations (four type and seventeen value observations). It includes the 31,752,787-occurrence proof body in lean_workbook_plus_6206 and a context borrowing a let value with 10,844,757 occurrences. No alternate proof-role observation occurs in this package. These frozen sources are publisher-attributed to Goedel-LM/Lean-workbook-proofs; original generation is not independently reproduced. The interface is available at these exact recorded routes. Unrecorded routes clear the module view and remain explicitly unsupported.

Five AI observations have different inferred and wrapped expected closed-type syntax. Their recorded kernel conversion checks pass. closedTypesStructurallyEqual describes that inferred/expected comparison; it is not a canonical-to-target equality flag. Both the original syntax flag and the selected target’s native conversion evidence remain visible in provenance.

The model audit covers 633 existing native observations in thirteen packets: twelve own controls and the frozen AI proof. It checks 5,926 cuts, including 478 canonical-use cuts, 1,299 displayed variable-link checks and 163 rejection controls. Of these cuts, 2,182 use source pages. Their largest copied source snapshot contains 48 tuples and 5,426 decoded JSON bytes; this is a measurement of the finite audit. The underlying AI source stores 91,424 nodes, and the independent materialized reference reaches 91,425 nodes. That offline reference is fully resident in the test process. These are finite structural tests, not a Lean proof of the implementation, semantic compression or a comprehension study.

In paged mode the reader shares its original source cursor, capped at 4,096 tuples. A prepared module snapshot has separate hard limits of 4,096 source tuples and 8 MiB decoded JSON. The existing native context package is separately resident, capped at 8 MiB decoded; each raw type graph is capped at 32,768 stored nodes. One prepared selection is cached. The preceding visible cut can coexist briefly with its replacement during asynchronous preparation. These limits do not describe total JavaScript heap or whole-browser memory. Complete mode retains its existing fully resident source.

The asynchronous viewport prepares source-dependent fields, labels and inverse references under the source queue. A sealed cut then renders without accessing evicted source pages. Failed optional data preserve the current cut or source graph, with retry. Proof, use and region changes cancel stale work. Existing own reduced-context modules retain their original component and remain available without the new optional code.

The extension reuses published compiled context data. It rebuilds no private proof project or Mathlib and publishes no original AI proof scripts. The shared viewport has optional initial-route and asynchronous navigation hooks; its synchronous callers retain their existing behavior. Its code hash is reflected in regenerated native metadata manifests; native queries and type graphs are unchanged.

node scripts/test-proof-atlas-source-context-modules.cjs
node scripts/test-proof-atlas-source-context-module-loading.cjs
# After the production site build:
node scripts/test-proof-atlas-source-context-modules-browser.cjs

Computed occurrence references

Computed region Relation to the selected original use
Added lambda/Pi/let wrapper Exact source context header; relation new-wrapper-from-source-header
Wrapper domain or let value Exact original header field and descendant route, in the pre-binder context
Closed term body Selected original term route followed by the computed descendant route
Closed expected-type body Selected native raw-type graph and type-local route

The canonical observation identifies the computed graph. The selected observation identifies the inverse map and retains its own native flags. The audit additionally opens 1,432 cuts through recorded context header fields across term/type components. Variable checks compare each displayed computed binder reference with the corresponding original source binder or native type-local binder; raw-type ambient references resolve through the selected original context. Wrapper references retain their construction relation rather than acquiring an invented identical source expression.

Ordered source-context projection

The same reader now offers Required syntactic context at three separately checked routes in lean_workbook_plus_6206. Full recorded context remains the default. Other full-context observations receive no reduction control and explicitly report that a checked reduced context is not recorded at that route. Missing optional inventory is labelled unavailable. The article remains a separate application; this rule operates on compiled terms without article correspondences.

The source-backed projection changes free variable indices while retaining constructor payloads, ordered ports and every internal binder. For an original context of depth d, let S be its retained slots in increasing order. Under c internal binders, an index i < c remains unchanged. Otherwise its original context slot is j = d - 1 - (i - c); if j is the qth entry of S, its projected index is c + |S| - 1 - q. An omitted required slot is rejected. Header domains and let values use the retained prefix strictly before their own source binder. New assumptions become lambda/Pi pairs; retained definitions remain lets with nondep=false.

Authenticated source support summaries and the validated recorded-type graph supply the dependency interface. The native retained slots must match that interface. Projection preserves each borrowed region’s occurrence count. Its exact maximum free index follows from the monotone ordered index map, without scanning every borrowed node. Only accessed source tuples and virtual states are retained. This is a tested implementation rule, not a Lean metatheory proof.

Fresh native checks in the same frozen compiled AI environment verify closed term/type typing, expected-type conversion, instantiation typing and conversion to each original occurrence. Two additional queries deliberately omit required support; both fail specifically because support remains free. The finite results are:

Selected original route Role Context entries Full closure occurrences Reduced closure occurrences
1:1.1.1.1.1.1.1.2.0 type-valued proposition 8 → 1 9,439,756 95
1:1.1.1.1.1.1.1.1.0 proof 7 → 1 575 285
1:1.1.1.1.1.1.1.2.1 proof 8 → 7 20,284,420 10,845,049

These counts describe three context closures. They are not a reduction of the entire theorem, logically minimal assumptions or semantic proof compression. The largest reduced module contains 33,484 distinct nodes and exceeds the existing materialized-module limit of 32,768. Its source-backed view does not raise that limit or load a second complete closed graph. It borrows the original source cursor and remaps indices lazily.

ProofAtlasProjectedContextModuleScene/1 uses the source-projected-context-module namespace and the existing constructor notation. Complete closed roots carry the corresponding native judgment; focused descendants receive no additional typing. Each selected use has its own inverse map. Header regions and term-body routes return to exact original source occurrences; expected-type bodies retain a native-type namespace. The original-type view uses the original context and exact Γ targets, including omitted headers needed only to identify that original context.

projected-context-modules-manifest.js pins a 16,243-byte decoded compiled package with the three recipes and small original type graphs. It excludes original Lean scripts, logs and materialized closed graphs. Separate constructor-root fingerprints pin native closed terms and expected types independent of DAG node numbering and sharing. The public offline checker reconstructs those expressions and matches their fingerprints. The reader authenticates the package and computes finite cuts; it does not rerun Lean or recompute an entire closed graph. Fingerprints and archived native attestations are not a portable kernel certificate. Fresh native reproduction additionally requires the pinned compiled module and dependency environment.

The model audit covers 597 native observations in sixteen packets: 594 existing own controls and the three AI routes. It compares 5,582 cuts and 2,031 displayed inverse variable links with independent references. In 302 displayed cases an index changes while its exact original binder is preserved. It also checks 562 canonical-use selections, 506 header-region cuts and 99 rejection controls. The AI subset has 54 source-paged cuts; full offline reference graphs are separately resident. Native reuse checks belong to the existing own controls; the three AI records contain no further module instantiation or cross-proof reuse result.

A prepared cut has hard limits of 4,096 captured source tuples, 8 MiB decoded source tuples, 8,192 virtual states and 65,536 virtual property operations. The finite audit reaches 47 source tuples, 5,145 decoded bytes, 61 states and 191 operations. Source and scope caches, raw type metadata and the preceding visible cut during replacement have separate residency. Complete mode retains its full source. These bounds do not describe total browser memory.

The integrated browser checks both contexts, all six term/type roots, exact binder and raw-type Γ jumps, preserved source selections, optional-load recovery and stale preparation. Desktop/mobile and light/dark accessibility checks cover the reader. These checks do not establish readability or improved human comprehension; central edge captions can still overlap.

node scripts/test-proof-atlas-projected-context-modules.cjs
node scripts/test-proof-atlas-projected-context-loading.cjs
# After the production site build:
node scripts/test-proof-atlas-projected-context-browser.cjs