# 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:

- New lambda/Pi/let wrappers refer to the exact original context header, with the relation `new-wrapper-from-source-header`.
- Header fields map to their original domain/value expressions through context reindexing.
- The term body maps to the selected original term and exact descendant route.
- The expected type body maps to the separately qualified native raw-type graph. It acquires no invented source-proof occurrence.

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.

```sh
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.

```sh
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.

```sh
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 `q`th 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.

```sh
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
```

### Connection captions in computed views

The shared computed-term viewport measures the rendered caption font and reserves glyph and node-name bounds. It tries five fixed positions along each connection, rejecting collisions with previous captions, nodes, names, other connections and the viewport boundary. A caption remains on its own straight segment. At narrow widths, or when no candidate fits, the visual caption is omitted; the edge title and keyboard connection list retain the exact field or scope role and both endpoint paths. The endpoint buttons use the same computed/original namespace distinction as node navigation. Resize and font-load events remeasure the finite scene without changing its mathematical structure.

`node scripts/test-proof-atlas-beta-captions-browser.cjs` audits actual SVG bounds and exact connection lists on all three native routes, both context modes and both term/type roots, at four widths in both themes. It deliberately overlaps two captions and changes a keyboard port to check rejection, exercises font remeasurement and follows an endpoint button. This is a finite caption-placement check; node-name layout, edge crossings away from captions, and human comprehension remain separate questions.

The [structural projection theory](../context-projection/README.md) proves recovery, composition and count laws for a specified `Lean.Expr` function. A finite bridge compares the lazy implementation with that function. These results do not replace the closed-module typing and instantiation checks above.


### Dependency interface geometry

**Required context** draws the existing qualified dependency interface as a selected origin and its referenced context entries. The same view serves the own checked modules and the three native reduced AI contexts. It separates term references, recorded-type references, binder-type references and let-value references. These arrows are syntactic references, not logical inference. Full recorded contexts receive no invented reduced interface.

Inspecting a target's header changes only the dependency origin; it preserves the selected source occurrence and computed module. A separate action opens that exact original binder. Recorded-type navigation opens the selected original type in its existing native-type namespace. Header types and let values use the context before their own binder. Retained let definitions remain visibly distinct from assumptions. The native typing scope remains the complete recorded closed roots; this view adds no judgments.

Each origin shows at most sixteen reference edges. Later pages retain the remaining edges, and each target keeps its exact source reference. Repeated relations to one header remain separate edges. Contexts and local origin history are capped at 512 entries. The component uses an already prepared interface and makes no source requests, builds no occurrence tree and creates no additional proof/type graph. Source, scope and native evidence residency remain separate. Each change of module disposes the previous interface and its handlers.

`node scripts/test-proof-atlas-context-interface-browser.cjs` checks a proof hypothesis whose type depends on another context entry, all three native reduced AI interfaces, local header inspection, exact original/type jumps, complete 33-edge paging and stale-handler disposal. Desktop/phone checks in both themes cover visible cards and accessibility. The independent dependency audit remains the source of correspondence checks across 743 existing observations. These are implementation and navigation checks, not a comprehension result.

The separate [ordered closure theory](../context-closure/README.md) proves leastness, closure, bounds, idempotence and union composition for an explicit descending dependency-list function. Its earlier-header condition describes the pre-binder scope used here. Finite comparisons with this implementation are separate from the source-summary checks and native module typing records; no additional occurrence receives typing from the closure theorem.

### Reference-chain witnesses

**Why retained** displays one shortest reference chain from the selected term or recorded type to a retained slot. Each edge distinguishes term support, recorded-type support, binder-type support or let-value support. It identifies the complete originating region and exact original target binder. A support set does not identify an individual variable use inside that region; the view makes no such claim. Recorded-type origins keep their native-type namespace.

The search uses the prepared qualified interface only. It fetches no source or support pages and expands no proof occurrences. Breadth-first discovery starts both term and type roots before visiting headers. Equal-length ties prefer term, then the existing ascending slot and field order. The index retains at most 512 predecessor triples; its queue has at most 514 origins. It performs at most 524,288 mask-slot inspections, counting both zero and present references. A chain has at most 512 edges and returns sixteen per page. The input interface, source/type evidence and temporary reference pages have separate residency. Exhausted bounds or inconsistent closure produce an unavailable explanation, preserving the dependency diagram. These are fixed representation bounds, not whole-browser memory measurements.

The optional witness code loads on first request. Failed code can be retried. A new explanation cancels its preceding code waiter. Disposal removes that waiter immediately, even while the shared script request is still pending, so it does not keep the previous module alive until download completion. A late load cannot restore the disposed view. Original-region and target-binder actions use the existing source maps; type-origin actions open the original recorded type. The witness operation adds no native typing or article correspondence.

The independent audit covers 746 existing observations: 594 own module observations, 149 original AI observations used for offline interface checks, and the three native reduced AI observations. It checks 454 retained-slot paths and 460 edge appearances against independent expression-support sets and repeated distance relaxation. Six paths are indirect, all in own controls; the audited AI paths are direct. The browser retains its existing coverage of own modules and three reduced AI routes; the offline 149-observation audit creates no new full-context interface control. A synthetic 512-slot chain checks complete path paging, while competing-root controls check shortest paths and deterministic ties. These finite checks do not prove the JavaScript implementation or establish logical necessity or comprehension.

```sh
node scripts/test-proof-atlas-context-witnesses.cjs
# After the production site build:
node scripts/test-proof-atlas-context-witnesses-browser.cjs
```