Evidence for the geometric language

The technical record is organized by research layer. Search for a rule, a declaration or a limitation; open an entry for its observations, exact scope and reproduction links. These are implementation and evaluation records, not independent claims of human comprehension.

Research program · Visual manual · Compiled proof library

1. Kernel notation

First structural implementation

The optional scoped geometry prototype is independent of the article map. Its versioned scene contract retains all twelve kernel constructor kinds, ordered child ports, occurrence-qualified vertices, lexical-scope links and exact collapsed boundaries. Universe and other constructor payloads remain attached; they are not yet a complete geometric notation of their own.

A scene is a finite cut of the expanded occurrence tree, constructed directly from the shared packet. Each displayed occurrence contributes one; a frontier contributes the number of descendants hidden below it. Their sum must equal the selected root’s exact expanded count. External binder targets remain explicit context boundaries. domain is the exporter’s display alias for Lean’s binderType; the scene records both port names. The cut is recoverable against its packet, not a standalone proof certificate.

The audit currently checks 6,166 cuts across all 2,098 packets and 4,972 lexical-scope links. Three synthetic scope controls include a shared bound-variable node with different binders, a let value outside its new binder and an enclosing binder outside the current cut. These controls are structural tests, not additional kernel certificates.

In the real JacobiCore.E_pos proof, shared node 17 appears on two displayed routes and points to different binders. The prototype draws separate occurrences. The initial largest proof-body cut shows 9 occurrences and records 462,476,262 hidden descendants, accounting for 462,476,271 body occurrences. This verifies the cut’s accounting, not meaningful semantic compression or human comprehension. The raw depth cut can stop in a binder telescope before exposing the mathematical argument; the optional abstraction below addresses this specific obstruction.

Reproduce with node scripts/test-proof-atlas-geometry-core.cjs; after the production site build, run node scripts/test-proof-atlas-geometry-browser.cjs. The browser checks real canvas/keyboard selections, distinct scope targets, exact boundary refinement, saved routes and the large body at phone/desktop widths in both themes.

Scene implementation · Independent path/scope audit · Browser checks

Universe-level geometry

Universe levels now have their own compositional grammar: zero, succ, max, imax, param and mvar, with ordered of, left and right ports. They are payloads of Expr.sort and Expr.const, not additional Expr children. imax(a, b) is zero when b is zero and otherwise the maximum of a and b. Raw syntax remains intact, including max(u, 0) and reversed max inputs; the view does not normalize levels. A constant’s universe arguments retain their original slot order.

Parameter references use the serialized structured Lean Name and the enclosing compiled declaration’s packet identity. They occupy a separate universe-context namespace, independent of expression binders. Numeric and string Name components remain distinct. These are exact nominal references; the view does not invent a declaration-parameter slot from a displayed name. Missing structured names and unresolved universe metavariables remain explicit boundaries, without inferred assignments. Optional numeric inputs illustrate constructor semantics and do not instantiate the proof.

The source audit covers 123,121 universe fields and 132,567 serialized Level occurrences in 2,203 packets, containing 2,100,910 stored expressions across both snapshots, the fixed AI-source sample and synthetic recursion controls. It checks all fields and their 4,883 exact nominal references. The maximum stored Level depth is six and the largest per-expression payload has sixteen Level occurrences. The max/imax examples in this inventory come from the separately labelled synthetic recursion edition; these counts do not establish difficult-universe coverage of AI-generated proofs.

The converter retains structural sharing in a bounded Level DAG. A fresh native raw-max control has 81 stored nodes and 2⁸¹−1 expanded Level occurrences. Its large shared shape is a structural control, not a kernel-checked proof. The native suite checks all six constructors, ordered max syntax, exact Name binding and 375 concrete valuations. It also distinguishes two kernel interfaces: an isolated Sort ?u expression check can succeed, while admission of a declaration containing that unresolved universe fails. Neither the renderer nor the valuation treats ?u as solved.

Source, recorded-type, conversion-endpoint and computed-result inspectors reuse the same universe rule while retaining their separate provenance. A scene draws at most 24 Level vertices at four levels; frontier counts retain the complete selected region. The DAG is capped at 4,096 nodes, with bounded input work and depth. Shared-node navigation and parameter inputs are paged. The original published packets retain their tree payloads. The transport rule below extends the native exporter while preserving those immutable packets. The full research goal remains active.

Native universe reference controls · synthetic

The large shared input is a structural example. These controls are separate from the proof corpus.

Source example · Universe model and renderer · Source-field audit · Native controls and reproduction

Shared universe transport

The production serializer used by source terms, inferred types, reduction results and recursor metadata now preserves large Level sharing before JSON serialization. Each payload is a legacy Level tree when it has at most 256 expanded occurrences and depth at most 32. Otherwise it is an envelope with encoding: "LevelDAG/1" and one rooted, postorder Level DAG. The envelope is a transport format, not a seventh Level constructor. Constructor order, structured names and raw max/imax syntax remain unchanged; no normalization is performed.

The library, type checks, type comparisons, substitution and recursive-rule views share one decoder. Syntax keys are independent of wire encoding and local DAG identifiers. Reordered storage tables can denote the same raw Level syntax; reversed constructor ports cannot. A large payload is described by its bounded DAG reference and remains recoverable through its universe diagram. The reader does not expand it to print a term label.

The compatibility audit reconstructs all 123,121 source universe fields in 2,203 packets, then 2,749 fields in 91 runtime expression graphs from 56 type/result packets through an independent inverse. It preserves expression children, lexical scope and exact occurrence counts. Across 48 judgment packets, validation also checks 32 recursor calls, 76 kernel-rule inputs (including 16 recursive premises), the beta package and all 48 let-premise records after lossless level re-encoding. Existing compiled packets, original native fixtures and result archives remain unchanged. A fresh replay records its current producer hash separately from the original fixture’s producer hash; it does not rewrite the original provenance.

Fresh Lean 4.33.1 controls check all six Level constructors, the exact switch at 255/256/257 occurrences and depths 32/33, and both Sort and constant payloads. Eighteen native roots retain the earlier reference syntax and 375 concrete valuations. Five core-only declarations pass native body/type checks and declared-type conversion; their 68 stored expression vertices and inferred types compare equally across tree and DAG encodings. The 81-node shared Level and the 200-successor input remain separately labelled structural controls. They are not large closed proof certificates or AI-generated examples.

An individual Level DAG is bounded to 4,096 nodes and depth 512, with bounded decoder work. Source-packet decoding has a 64 MiB limit, and the compatibility audit checks every current source packet against it. Sharing is retained within each Level payload; repeated Level structures in separate Expr payloads still use separate envelopes. Packet-wide universe interning, paging source declarations larger than the input bound and measured human inspection tasks remain open work.

Native serializer · Independent native roundtrips · Whole-corpus compatibility audit · Compiled transport controls

2. Scoped composition and scale

Binder-telescope abstraction

The optional Fold binder contexts rule contracts a contiguous prefix of lam, forallE and letE along their body ports. Tₙ denotes an ordered n-entry telescope, not an additional Lean constructor. Mixed prefixes retain each entry’s constructor, payload, visibility and original route. Type/domain and let-value regions remain separate hidden regions in the environment before their own binder. The continuation uses the environment after all retained entries.

ProofAtlasGeometricScene/2 distinguishes drawn vertices from retained kernel occurrences. A telescope with n entries retains n binder occurrences and the exact roots of its header regions. Thus retained binder occurrences + hidden header regions + continuation = original subtree, using exact expanded counts. No represented term is rewritten. Ordinary scene version 1 remains available by turning folding off.

References from the displayed continuation to a folded binder keep the original target path plus a telescope vertex and one-based slot. The ordered header list opens the exact binder, its type or let-value region. The continuation also has an exact navigation link. A prefix scan is capped at 64 entries per compound node; a longer prefix is explicitly marked as continuing, rather than silently omitted.

The independent audit checks 4,164 folded cuts across all 2,098 packets: 3,545 telescope vertices, 17,978 retained binder entries and 3,260 displayed links to folded slots. Small adversarial controls check a mixed lambda/forall/let prefix, shadowing, dependent header scopes, exact partition of every original occurrence and a deliberately truncated prefix. Five corruption/limit controls must be rejected. These are representation checks, not a semantic proof-compression certificate.

On the largest compiled proof body, the 13-entry prefix becomes one vertex and the first non-binder application is exposed. The resulting initial view has 14 vertices retaining 26 kernel occurrences plus 462,476,245 hidden occurrences, still accounting for the original 462,476,271. This improves access past the header; readability of the remaining application structure and human comprehension remain unmeasured.

Folded example · Large proof example · Telescope audit · Browser checks

Application-spine composition

The optional Group applications rule gives a left-associated chain (((h a₁) a₂) … aₙ) the representation @ₙ(h; a₁, …, aₙ). It retains all n original Expr.app occurrences, the exact head route and the arguments in call order. Its accounting identity is n + size(head) + sum(size(argument)) = size(original). No beta reduction, implicit-argument omission or term rewriting occurs. The rule composes with the telescope rule; application ports do not introduce binders.

head and argN are explicitly abstract ports, rather than invented kernel fields. A head need not be a constant. The rule stops at lambdas, projections, metadata and other non-application constructors. A selected inner application represents that selected term only; it does not acquire arguments from enclosing applications. A complete function spine does not establish that a call is saturated, that an argument is a proof or that an arrow is logical inference. Those require additional type evidence.

Scene version 3 has separate bounds for drawn vertices, depth, ports per application and vertices per layer. The initial view draws at most 48 term vertices, four levels below the selected root, six ports per compound application and eight term vertices per layer. Undrawn head/argument regions retain their complete roots, routes and occurrence counts. All grouped arguments, including undrawn ones, have navigation controls. Explicit enclosing-context boundary vertices are additional to the term-vertex budget. A function-spine scan is capped at 64 applications; if that limit is reached, the remaining function spine is retained as a region and the visible arguments have relative trailing-slot numbers, not fabricated absolute positions.

Across all 2,098 packets, the audit checks 4,164 composed cuts containing 18,787 application groups, 70,347 retained applications and 8,641 lexical-scope links. Independent controls cover nonconstant heads, metadata boundaries, shared variables under argument binders, selected inner applications, capped spines, complete small-term occurrence partitions, node/depth/layer limits and eight rejection cases. These establish serialized structural correspondence, not new kernel certificates.

For SBracket.mk.inj, a 57-entry telescope leads to a 59-argument application of SBracket.mk.noConfusion. The view exposes the head and first five arguments; the 59th argument remains directly selectable at its original route. On the largest body, the composed initial cut has 21 vertices retaining 70 kernel occurrences plus 462,476,201 hidden occurrences, accounting for the original 462,476,271. These bounds describe a recoverable view, not a measured improvement in human comprehension.

Composed example · 59-argument example · Application audit · Browser checks

Type-expression geometry and structural sharing

Show type diagram draws a recorded type using the same constructor shapes, ordered ports, binder telescopes and application spines as the proof view. A type component is either the selected expression’s type, an argument’s actual type or the corresponding instantiated expected domain. Every component identifies its native judgment route, type-evidence hash and root in the shared type table. This is a structural diagram of a recorded type; selecting a descendant does not produce an additional inferred typing judgment.

Scene version 4 separates two binding namespaces. A type-local bound variable points to its exact binder within the type expression. A variable bound by the original proof context points to an explicit Γ boundary with that original proof occurrence’s route. Type-local navigation refines the type view; selecting Γ returns to the original proof binder. Binder domains and let values continue to use their pre-binder context. The article selection remains unchanged during type-local navigation. An argument component also provides a direct link to its original proof occurrence.

The initial type cut is bounded by 32 term vertices, depth three, six term vertices per layer and four displayed application children; context boundaries are additional. Hidden regions retain exact counts and navigation controls, including all arguments of a grouped application. The same type may have different meanings under different contexts; neither a shared type-node identifier nor visual similarity identifies those meanings.

The serialized format interns repeated type expressions within each declaration, preserving every constructor payload, ordered child, expanded count and scope requirement. The initial type-only projection contained 25,840 shared nodes instead of 144,470 separately serialized nodes, with five compressed files totalling 339,688 bytes instead of 1,232,961. The richer application projection below extends these tables. The publisher compares the original and packed contextual judgments using recursively hashed structural roots, then the audit recomputes that fingerprint. This is lossless structural packing, not definitional equality, semantic compression or a new kernel certificate.

The audit checks all 6,511 initial component cuts, including 1,359 displayed links to original proof binders and 212 to type-local binders. It independently resolves displayed bound variables, checks exact retained/hidden accounting and rejects 20 modified scene controls. A synthetic open-expression control separates an ambient proof binder from an internal type binder; it is a structural test. The sharing audit rejects 15 changed-context, changed-role and changed-payload controls. Browser tests exercise actual canvas and keyboard jumps, component selection, pre-binder domains, source changes, unsupported article selections and accessibility at phone and desktop widths in both themes.

This extends the common syntax/binding notation to the selected recorded types. It does not supply logical inference rules, complete type coverage, an AI-generated corpus benchmark or measured comprehension results. The broader program remains active.

Type geometry audit · Sharing audit · Browser checks

Bounded delivery of computed terms

Computed let terms now use a separate delivery index and bounded result pools. Structural interning shares relative expressions within one declaration, while every query retains its own exact source occurrence, context and computed root. Source packet hashes, typed premises, original native packing hashes and environment attestations remain unchanged. The previous full compiled attestations and their original manifest remain available for audit and older readers. The normal pooled reader does not fetch them.

The 48 computed results previously stored 580,653 result nodes across seven complete sidecars. Deterministic bounded interning stores 330,190 nodes in eight pools. A single pool for all three results of lean_workbook_plus_6206 would require 134,983 nodes, exceeding the existing 131,072-node cap. The packer therefore splits that declaration into two pools rather than increasing the cap or dropping a result. Greedy packing follows the native query order; it is not claimed to minimize packet count or bytes.

Opening a declaration loads type/derivation metadata only. Opening a let view fetches its pool, checks the file hash, graph structure, context-specific roots and independent capture-avoiding substitution, then displays the same computed cut. The reader retains at most one result pool and serializes result loads. Selection changes cancel pending requests, and the geometry engine loads before any result is pinned. The index is capped at 8 MiB of decoded JSON and a pool at 32 MiB and 131,072 nodes. Failed checks preserve the original proof and native type metadata. These are result-layer bounds; source and type packets retain their separate existing limits.

On this fixed sample, complete compressed delivery of the seven indexes and eight pools is 2,083,421 bytes, compared with 3,611,017 bytes for the former complete sidecars. The retained audit archives are additional public files; these numbers compare normal delivery, not the website’s total stored bytes or measured load time. All 48 complete result roots agree with the archived attestations, and all 281 previously sampled computed cuts retain their visible structure, occurrence accounting and lexical targets. The pool audit includes 122 changed-record, corruption, cancellation and byte-bound controls.

The source sample’s let nodes have no alternate occurrence paths, so it cannot test cross-context sharing by itself. A fresh native example adds one shared let under three different outer binders. Two occurrences are queried; their identical relative computed term can share one stored root while their Γ links remain different. The third occurrence receives no reduction record. A provider that returns another occurrence merely because its node identifier matches is rejected. The fresh suite now has 17 examples, 18 exact native queries, 593 computed cuts and 131 rejection controls. It supplements the preceding 16 examples with this shared-context case.

This preserves source-relative proof geometry while reducing repeated result delivery on the evaluated corpus. It does not establish arbitrary-corpus memory bounds, semantic proof compression, universal normalization or measured human inspection benefits. Native records remain environment-relative attestations. The general goal stays active; the blog is unchanged.

Delivery index and pool loader · Lossless pool packer · Archive comparison and resource checks · Browser lifecycle checks · Shared native context control

Paged source composition

The optional paged geometry uses the same occurrence-based language while fetching source fields on demand. Each tuple preserves its constructor, ordered children, payload, expanded count and scope requirement. A hash-addressed index connects the pages to a completely validated offline packet. The client retains at most 4,096 source tuples and four index pages; native queries, type graphs, headers, scenes and decoding buffers have separate residency. This is a source-cache bound, not a whole-application memory bound.

Across the finite 34-packet native-query inventory, all 1,979,510 field values and 23,184 complete scenes agree with independently opened full-source references. The scenes cover 1,288 recorded routes, three priorities, three grouping modes and source fallback on/off. Earlier scene formats remain equal in 11,592 comparisons. This inventory includes twenty released AI-source declarations; the browser scale case represents a 29,794,821-occurrence body without downloading its complete source packet. These checks do not establish all-context typing or human comprehension.

Scene version 7 exposes literal kernel fields where native construction evidence is absent. Dashed source layouts preserve lexical scope and exact routes without assigning unrecorded child types or proof roles. They cannot become checked introduction/context frames. Distinct source-field and typing-premise edges prevent this structural fallback from acquiring an unsupported logical interpretation. Synthetic controls cover all twelve constructors, shadowing and shared variables under different binders.

The paged mode covers four published research declarations, one working-snapshot declaration, twenty released AI-source declarations and nine recursion controls. Other declarations and the article retain the complete loader. Missing assets, unsupported declarations and exhausted resource bounds remain explicit; opening the complete view requires a user action. Native query delivery is described below. Shared type graphs still load fully. Paging the remaining evidence and evaluating proof-inspection tasks remain open.

Protocol and reproduction · Producer verification · Complete-reference comparison · Corruption and scope controls · Browser checks

Parametric source sharing

Repeated source expressions can now share one relative shape while retaining separate original occurrences and binder assignments. Free term references become formal ports; internal binders retain relative routes in a template namespace. Instantiation restores the original source paths and lexical targets. Each occurrence keeps its own recorded root type and role. Refinement preserves the whole-template interface, including ports unused in the smaller cut.

The comparison includes displayed proof regions and collapsed source regions. The independent audit checks 23,198 uses in 11,592 views across the finite 34-packet inventory, including 1,881 proof-role appearances. In lean_workbook_20418, three proof-valued uses of Classical.or_iff_not_imp_left share a 93-occurrence source shape with separate binder assignments and proof records. Selected regions also expose relative source geometry, ordered fields and retained constructor occurrences for local inspection. This is syntactic sharing; native judgments remain specific to each use. Semantic compression and comprehension have separate evaluation requirements.

Example reader · Protocol, bounds and reproduction · Independent corpus audit · Constructor and failure controls · Browser checks

Scope-path traversal

The context walker retains the current source path as it follows a route. It no longer restarts from the declaration root for every enclosing binder. The first binder requests the prefix path once; subsequent fields extend it directly. Binder-free routes retain the earlier lazy access to root-path metadata. No route or context cache is introduced. Domains and let values still precede their own binder; bodies still extend the context by one.

The contract comparison covers all 2,234 public source packets in the five tested manifests: one representative route per 2,888,126 stored nodes, 36,690 additional incoming routes, thirty structural occurrences covering all twelve constructors, and compatibility controls. All 2,924,850 comparisons match the prior context result. No representative route exceeded the existing 512-slot bound. The additional incoming routes are sampled at most thirty-two per packet; this is not all expanded-context coverage. The twenty fresh native controls also retain their original scope, typing and shared-proof targets.

A synthetic prefix of h consecutive binders makes the source-array cost explicit: the previous walk performs h²+2h reads, the incremental walk 3h. At the 512-slot bound these counts are 263,168 / 1,536. This describes source-array traversal. The returned full path strings and copied prefix routes still have their original size; total work, total memory and runtime speedup are not identified with that read count.

Across the fixed 5,152 finite cut constructions, source-array reads change from 51,242,388 to 10,884,226 without grouped introductions, and from 93,678,256 to 18,018,374 with grouping. Every cut touches the same unique source-node set. The measurement starts after complete source and typing-evidence loading and excludes native type-graph accesses, payload bytes and initial validation. It establishes reduced repeated traversal, not source paging, lower total resident memory or improved comprehension.

Full-inventory context comparison and cost controls · Scope implementation

Compiled-packet recovery

The 20 frozen AI-attributed theorem packets, containing 268,356 stored expression nodes, have been reconstructed directly from their public data and checked in Lean without importing their original theorem or proof modules. The production serializer reproduces all six expression-table fields exactly. The kernel checks each expected type as a proposition, proof value and conversion to the expected type. Transitive baseline axiom dependencies match the published records: propext, Classical.choice and Quot.sound, with no sorryAx dependency. Pinned compiled Mathlib/Aesop dependencies remain trusted.

Own controls separately exercise all twelve constructors structurally, including open terms that receive no kernel-validity claim. Four closed terms have native checks. Boolean metadata is supported; other metadata kinds are rejected. The 20 compiled theorems are the successful part of the predetermined 24-script sample, not the complete source dataset. This establishes recoverability for these packets. It does not prove a general decoder theorem, assign types to arbitrary diagram nodes, validate article prose or measure comprehension.

Method, assumptions and reproduction · Public compiled-evidence audit

Paged construction evidence and frontier audits

The frozen proof-premise chain now contains 19 → 27 → 36 → 50 native queries. The last layer adds fourteen checked applications, preserving every earlier contextual judgment. This finite inventory contains sixteen introductions and thirty applications; seven applications also carry elimination metadata. Eighteen next-layer roots remain explicitly unrecorded. Following proof-valued premises omits type/value branches and stops at declaration/context references; even an empty frontier under this policy would not establish complete proofs.

An independent native-field audit checks all three layer transitions, exact source paths, parent incidence and structural type identities. It compares 147 premise appearances across the snapshots and rejects sixteen changed-data or bound controls. Three stored nodes appear at distinct frontier routes; node sharing never substitutes for lexical context. The same independent enumerator agrees with the visual frontier on all 34 existing native inventories, without supplying new kernel checks for those other candidates.

Optional replay records share the 128-query/16-MiB native cache; paged source fields retain their 4,096-node cache. The complete-source reader keeps its source packet in full and one selected observation/query for synchronous inspection tools. Shared type tables remain fully loaded under separate fixed bounds. The historical resident fallback keeps its 32-query/ 256-KiB cap. The current complete replay package exceeds both fallback bounds; the paged reader retrieves individual queries. These are component bounds, not a total-browser memory guarantee. Transport creates no new typing judgments.

Both fresh native runs reproduce all fifty query records identically. The transport audit compares 320 exact observations and 150 complete/paged cuts, forces eviction with a one-query cache, and retains sixteen failure/disposal controls. General typing preservation, semantic abstraction, broader coverage and measured comprehension remain open.

Method and limits · Immutable frontier chain · Independent audit · Native-field implementation

Source-cut refinement laws

Six kernel-checked laws give a structural criterion for refining a cut of an actual Lean.Expr: retained constructors stay at their original paths, retained and hidden occurrences conserve the original size, and the two counts transfer exactly. The model supports all twelve constructors. It supplies a criterion for local refinement, not a proof that the browser implements it.

The distinction matters at a fixed display budget. In finite tests of the proof-focus selection core, increasing depth can reselect previously retained structure; independent source-path checks preserve two small counterexamples, including one with an unchanged retained count. Increasing the vertex budget preserves the tested cuts in the finite initial-root comparison. Native proof observations and semantic or comprehension claims are separate.

Definitions, proofs, counterexamples and limits · Lean laws · Compiled comparison records · Independent audit

Local refinement of source regions

The source reader can replace one hidden region while retaining the existing selected root, source paths and native records. The new cut checks exact transfer between hidden and retained counts; undo returns its prior state. Native type interfaces are recovered from the recorded parent query, with structural agreement required for a separate child type record. Source-only fields keep unknown roles.

The finite audit includes 1,224 initial-region expansions over 34 inventories and 148 expansions at current replay-query cuts. In the large projection control, opening a value input exposes a separately checked proof application that the proof-premise-only traversal omits. The operation keeps fixed display, route, boundary and metadata limits. No whole-proof, general typing or comprehension result follows from these tests.

Rule, bounds and reproduction · Implementation · Independent source audit · Reader checks

A recorded type interface identifies the exact source occurrence, its original lexical context and role, and the referenced type expression. Equal shared term or type roots alone do not identify that judgment. The independent interface checker resolves the original native records and compares stored type syntax in that context, without importing the scene producer or its comparator. Unrecorded parent fields remain source relations when a child has a separate type record. This check adds no kernel typing judgment or general definitional equality rule.

The selected connection retains expected and observed type records separately. The geometry distinguishes a structural type match, a retained parent observation and a source-field connection without parent typing. The judgment keeps the original context; recording-source actions keep their original query routes. Local expansion preserves this interface rather than assigning a type through shared-node identity.

Locality and nested composition

An expression-indexed one-hole context makes local replacement explicit. Ten kernel-checked structural laws include two pointwise equalities: every path outside the selected hole has unchanged visibility, and a path inside it has exactly the replacement’s visibility at its original offset. Nested contexts compose without changing the resulting cut; their hole routes concatenate. The original expression’s constructor fields and payload parameters remain fixed.

The independent fixture reader checks 624 replacements in 156 small cases, including all twelve focus kinds and eleven structural child positions. It compares literal payloads and untouched siblings as well as counts, and rejects twenty-two altered records. The general Lean laws and these finite decoder checks are separate evidence. No JavaScript, source-typing, lexical-link, semantic or comprehension proof follows from them.

Definitions, evidence and scope · Lean laws · Compiled records · Independent reader

Original paths through deep source cuts

Five kernel-checked focusing laws compose finite source-path segments while preserving the original endpoint and lexical target. The optional occurrence window in the compiled library uses compact original paths and draws external binders as context references outside the selected subtree count. It does not rebase a focused subtree or infer typing from a shared node identifier.

The independent walker checks 4,267 selected cuts over the two project snapshots, twenty publisher-attributed Goedel source packets and five large/deep controls. A source-only variable at depth 10,001 remains directly selectable with its original binder. Existing native query and source-cut record limits remain separate; these checks do not verify the codec or renderer, establish semantic compression, or measure comprehension.

Definitions, bounds and reproduction

3. Typed constructions

Checked occurrence types

The first type layer attaches native Lean judgments to exact occurrence routes. It does not classify arguments from constructor tags or declaration names. Before checking a selected term, the extractor compares the native declaration’s complete shared DAG—constructors, payloads, ordered fields, roots, counts and scope requirements—with its published packet. The private extraction driver also verifies the source module hash, compiler version and pinned revisions of compiled dependencies on the search path. Packages pinned in the manifest but absent from that path are recorded separately.

For each route, the extractor reconstructs its lexical context with Lean local and let declarations. Domains and let values use the pre-binder context; bodies use the extended context. Each introduced domain is checked to be a type, and each let value is checked against its declared type before extending the context. The kernel then checks the selected expression in that well-formed context. Argument domains are instantiated in call order, compared with argument types, and checked after substitution into the result type. An argument is labelled proof when its checked type is a proposition, type when that type reduces to a sort, and value otherwise. Binder visibility is recorded separately. These categories do not assert call saturation or turn an application edge into a logical implication.

Each judgment retains a shared type-expression DAG with its context abstracted back to bound indices. Reopening that type in its original context must reproduce the inferred expression by structural equality, including binder names and metadata. Pretty text is a presentation, not the formal type. The browser checks the sidecar hash, packet identity, exact route, complete enclosing-binder list, argument order and type-graph scope. The browser does not rerun Lean. These are native extraction attestations tied to the recorded environment, not portable kernel certificates or certified article equivalences.

The initial primary query inventory contained 943 selected occurrence judgments in five declarations, with 2,784 argument observations. It covers finite geometry-derived queries for JacobiCore.E_pos, JacobiData.slope_bound_abs, SBracket.mk.inj and CrossingData.crossing in the published snapshot, plus JacobiConcrete.AmplitudeChart.midpoint_polynomial in the working snapshot. This is not complete occurrence-type coverage of those proofs or the 2,098-packet inventory. A path without a primary query or an explicit application-trace observation remains without recorded type evidence; it does not inherit a judgment from a shared node or enclosing match.

The data audit checks 146 shared nodes appearing in distinct recorded contexts and rejects 37 altered-hash, stale-packet, wrong-node, wrong-context, changed-count, duplicate-route, reordered-argument, missing-environment and unreviewed source-syntax cases. Small independently run native controls check proof/type/value roles, dependent contexts and let scope. Two deliberately ill-formed surrounding contexts must be rejected; changing a serialized binder name also makes the native/packet comparison fail. The browser exercises exact argument and type selections, statement/proof distinction, missing-path fallback, rejected evidence without losing the original graph, and article synchronization.

This adds typed argument labels and a selected-term typing judgment to the structural geometry. The initial type-expression notation below reuses its constructor rules. Logical introduction/elimination diagrams, broader type coverage and measured proof-inspection tasks remain open work. The blog has no new result claim for this implementation.

Typed example · Type attachment audit · Native controls · Browser checks

Checked Π-application rule

Show application judgment displays one argument stage as a typing rule. It separates this checked relation from the structural graph’s child arrows:

Γ ⊢ f : τ       τ ≡ Π (x : A), B
Γ ⊢ a : A′      A′ ≡ A
──────────────────────────────── Π application
Γ ⊢ f a : τ′    τ′ ≡ B[a/x]

The function premise, argument premise and conclusion retain their original compiled occurrence routes and share the same enclosing context Γ. Type links open the existing constructor geometry for τ, its normalized Π expression, A′, A, τ′ and the substituted result B[a/x]. Selecting a term returns to its original proof occurrence. Stage navigation refines the rule without changing the selected proof or article. A type load from an earlier stage cannot restore that stale selection.

Native extraction kernel-checks the head, each argument and each application prefix. It records the function type before normalization, the Π expression, actual and expected argument types, and both inferred and substituted result types. Conversion is checked by asking the kernel to type-check a typed identity applied to the term at the proposed type. Thus the function-to-Π, argument-to-domain and result-to-substitution checks do not rely on the browser or on Meta.isDefEq alone. Every recorded type still passes abstraction/reopening equality in the original context. These are recorded native checks, not portable kernel certificates.

All 399 applications among the primary queries have complete traces: 2,784 argument stages and 8,352 kernel conversion checks. The longest trace has 59 stages. In 2,268 stages the Π body syntactically contains its current bound variable; this does not measure semantic proof dependence. The corpus queries all have constant heads. Seven fresh small native control applications separately test function-variable heads, dependent substitution, definitionally equal but structurally different domains, let scope and a partial application returning a function. Four of those controls have nonconstant heads. An invalid typed conversion is rejected.

The traces also supply 754 additional exact type observations, yielding 1,697 typed occurrence routes in these five declarations. An observation is an explicitly recorded head, application prefix or argument, with its source query and stage retained. Primary queries and these observations remain distinguishable. All overlapping observations agree structurally on type, role and context. No type is assigned from an arbitrary ancestor or from a shared node identifier. An argument observed as a term does not acquire an invented trace for its own internal arguments.

Complete traces have a fixed allowance of 32,768 shared type nodes per primary judgment; ordinary judgments retain their 8,192-node allowance. The packed declaration table is bounded by 65,536 nodes, and each displayed type cut still uses at most 32 term vertices. The initial 8,192-node trace allowance withheld 33 cases. Retrying those exact routes with the larger fixed allowance resolved all 33; the largest observed table used 13,879 nodes. The merge requires identical packet/environment headers and unchanged contextual core judgments. All 943 original core judgments were independently compared with the preceding release and remain unchanged.

The richer projection has 26,795 shared type nodes instead of 622,744 separately serialized nodes and occupies 844,759 compressed bytes instead of 4,088,554 without interning. The application audit checks all 2,784 rule stages, 16,704 linked type-component cuts, 754 observation cuts and 80 rejection controls. Fresh native controls additionally exercise the visual model and reject changed-context/environment merges. Browser checks cover premise/conclusion and Γ jumps, observation provenance, the 59-stage trace, delayed loads, missing optional code, unsupported article selections and keyboard/accessibility behavior in both themes and viewport sizes.

The application rule supplies one compositional typing relation. The introduction rule below complements it. Recursor-elimination diagrams, inventory-wide type coverage, an AI-origin benchmark, measured comprehension results and shareable rule/type-local selections remain open work. The general research goal remains active; the blog is unchanged.

Application rule model · Application audit · Fresh native model controls · Browser checks

Checked lambda introduction and context discharge

Show lambda introduction represents one binder by the following rule. The domain is outside the extended frame; the body is inside it. The conclusion returns to Γ and discharges exactly the selected binder.

Γ ⊢ A : σ       σ normalizes to Sort u
Γ, x : A ⊢ b : B′       B′ ≡ B
──────────────────────────────────── Π introduction
Γ ⊢ λ x : A, b : τ      τ ≡ Π (x : A), B

The native extractor checks the domain’s type and normalizes it with the kernel to a sort. It checks the lambda at its normalized Π-type, then opens the original body under a fresh local declaration with the original binder name and visibility. Typed identities enforce conversion of the new local to the Π-domain and of the body to the expected codomain. Each type is abstracted in its appropriate context and reopened without structural change. Domain/type/sort and function-type diagrams use Γ; actual and expected body-type diagrams use Γ,x:A. Their proof-context links therefore distinguish the current binder from enclosing binders, including repeated names.

The finite inventory contained 97 typed lambdas. Closing their consecutive lambda bodies yielded 104 introductions, all of which pass the native checks. Five actual body types differ structurally from the recorded Π codomain. They contain unreduced motive applications, such as (fun x => P) h, while the expected type is P. Their recorded kernel conversions establish the connection; the two expressions remain separate. This is a conversion of formal types, not an inferred equivalence of article passages.

Eleven additional primary lambda queries bring the total to 954. The primary queries and explicit application/introduction observations provide 1,737 exact typed routes in the same five declarations. Application traces retain their previous 399 calls, 2,784 stages and 8,352 conversions. All 943 preceding primary core judgments and the complete application records were compared structurally with the prior release and remain unchanged.

The independent audit checks all 104 context extensions/discharges and 832 linked type cuts, including nine displayed links to the current binder, and rejects 80 modified records/scenes. Fresh native controls include repeated binder names, a body type depending on the new binder, and a beta-convertible body type; their visual models check both contexts. Browser tests exercise actual term and binder clicks, observation provenance, stale loads, optional-view failures, article selection, both themes, phone/desktop widths and keyboard accessibility.

The shared type tables contain 26,801 nodes instead of 623,784 separately serialized nodes; the enriched files total 871,865 compressed bytes instead of 4,145,891 without interning. Existing fixed trace, packet and display limits remain in force. A displayed body type does not give its internal subexpressions new inferred types. The source lambdas remain recoverable by exact routes; no lambda is rewritten or removed from the compiled proof.

This adds an introduction rule to the common term/type/binding language. It does not complete the recursor, inductive elimination, universe-formation or semantic-abstraction layers. The corpus remains a finite private-development projection with public compiled data; no AI-origin benchmark or comprehension study is claimed. The research goal remains active, and the blog is unchanged.

Introduction model · Scope/type audit · Fresh native controls · Browser checks

Introduction–application composition and substitution

Show β composition connects the introduction and application rules through one leading β step. For a lambda-headed spine ((λ x : A, b) a₁) a₂ … aₙ, the computed result is (b[a₁/x]) a₂ … aₙ. Only the first lambda is contracted. The original declaration packet remains unchanged. This is a checked conversion between terms, rather than an inference from matching types or visually similar subgraphs.

The native extractor kernel-checks the original term, its lambda introduction and argument stages. It constructs the result with Lean’s capture-avoiding substitution, kernel-checks that result, checks it at the original selected type through a typed identity, and asks the kernel to compare the two terms. The result and its type are abstracted and reopened in the original context without structural change. These recorded checks depend on the pinned native environment; the public browser does not replay Lean and the record is not a portable kernel certificate.

A second implementation independently substitutes de Bruijn indices in the serialized DAG. It shifts ambient indices when inserting an argument under binders, leaves argument-internal binders intact, removes the discharged slot, and respects the pre-binder scope of domains and let values. Repeated subexpressions are interned instead of expanding the occurrence tree. The computed graph must match the native graph structurally. This comparison tests the exported substitution and scope correspondence; it does not independently establish the private corpus’s typing.

The finite corpus inventory contains three checked type-level redexes in CrossingData.crossing, under contexts of 13, 14 and 12 binders. Each applies a proposition-valued function to a real-valued argument. Each original selected region has 197 expression occurrences; its computed result has 193 occurrences in a 123-node DAG. These are proposition expressions, not proofs of those propositions. The separate compiled sidecar occupies 3,852 compressed bytes. The preceding primary type inventory and compiled declaration packets are unchanged.

Scene version 5 uses the existing constructor, telescope, application and binding notation for a computed-term namespace. An initial cut has 14 vertices retaining 20 occurrences plus 173 hidden occurrences. The fixed display limits remain 32 term vertices, depth three, six vertices per layer and four displayed ports per grouped application. Ringed nodes contain hidden regions; every region has navigation controls. A computed descendant has no invented original occurrence route and no new inferred type. Source buttons identify the original application, lambda, body and first argument. External Γ boundaries link to exact original binders; computed-local navigation leaves the source proof and article selection unchanged. Zoom, pan and keyboard-equivalent node controls apply to the computed view.

The data audit checks 369 computed-node cuts, 102 lexical links and 60 rejection controls. Nine fresh raw-kernel examples separately cover proof/value results, a dependent result, shadowed names, a binder inside an argument, duplicated arguments with sharing, multiple application arguments, let-value scope and a dependent binder domain. Their independent substitution models match Lean, and 36 changed-record controls are rejected. The kernel also rejects conversion between two unequal natural values of the same type. Browser checks exercise source and Γ jumps, computed refinement, introduction evidence, unchanged article selection, unsupported selections, stale loads, missing optional data and accessibility at phone/desktop widths in both themes.

This is one compositional conversion rule with a finite evaluation set. Reductions headed by constants, recursor computation, projection/let reduction, conversion chains, inventory-wide type/reduction coverage, an AI-origin benchmark and measured inspection benefits remain open. The general research goal is active; the blog is unchanged.

Checked example · Substitution and view model · Compiled-data audit · Fresh native controls · Browser checks

Recursor elimination and branch contexts

Show case elimination adds a rule view for a complete native recursor core. It separates the major premise, motives, minor premises, parameters, indices and result. Each minor premise is associated with its constructor through the compiled reduction rule. A branch frame shows the actual source lambda inputs and body when those exact judgments have been recorded. Domains use the context before their binder; bodies use the extended context. A function without recorded source lambdas retains its checked function type and an explicit missing-body notice.

Classification uses native ConstantInfo.recInfo, not a name suffix. The first wrapper adapter accepts a complete bijection of source inputs, with optional literal η-forwarding of functions. For example, Or.casesOn forwards its major premise before the branches, whereas Or.rec takes the major premise last. Its branches are forwarded as fun h => branch h. The extractor records the original compiled wrapper body, universe instantiations, source-slot permutation and η-prefix lengths. Independent checks recover those mappings from the serialized body and reject capture, repeated source-slot mappings and reordered inputs inside an η-forwarding prefix. Arbitrary wrapper computations are outside this adapter.

A constructor reduction’s body must call its recorded minor premise. That minor’s declared result must refer to the recorded constructor. These structural checks supplement the native kernel checks of the rule expressions, projected core, argument domains and result conversion. Kernel conversion alone is insufficient for source provenance: a fresh control confirms that two distinct proof constants of the same proposition are definitionally equal through proof irrelevance. No branch wiring is accepted merely because two proof terms convert.

The finite public projection contains 16 complete shared-node representatives in CrossingData.crossing and JacobiData.slope_bound_abs: nine Exists/And cases in the crossing proof and seven And/Or cases in the Riccati proof. Eight partial calls are withheld from elimination while retaining their ordinary type/application judgments. 32 exact branch-input lambda queries supply the source frames. The two sidecars contain 56 native type queries and occupy 39,530 compressed bytes. Their 46 overlapping type observations agree structurally with the preceding inventory. These are representatives under recorded contexts, not all expanded occurrences or inventory-wide recursor coverage.

The view uses the existing typing-rule bars, binder frames and type-expression geometry. Parameter/index terms, source branch functions and constructor cases retain exact source links. Expected branch types and source body types open the same bounded type notation. The initial rule view renders at most two cases and four source input frames per case; paging and direct constructor selection retain access to the other recorded entries. Type requests from an earlier source selection cannot restore that old view. Local type exploration and case paging preserve the source proof and article selection.

Original source occurrence accounting is explicit: core applications + source head + all source argument regions = original core. Additional applications and their argument regions account for the rest of a selected term. The source packet is unchanged. The projected kernel core’s type is linked by recorded conversion; its result button opens the original source prefix. A further application can change the selected term’s proof/type/value role, so the core retains its own recorded role.

The audit checks all 16 rule views, 242 type cuts, 32 context extensions and 304 rejection controls. Eleven fresh native cases separately exercise direct recursion, dependent and indexed motives, function-valued results, additional arguments, all three typing roles and empty elimination. Two further controls withhold a partial recursor and a non-forwarding wrapper. Their models check 17 branches, 18 source lambda frames, 143 type cuts and 77 changed-record controls. Browser checks cover all public rule views, seven kinds of exact source jump, input/case paging, domain/body contexts, article isolation, stale requests, optional failures and four accessibility configurations. Existing application, introduction, β and type-view browser regressions also pass.

The fixed extraction limits are 128 core arguments, 32 minor premises/rules, 128 inputs per minor, 16,384 metadata nodes and the existing 32,768-node type-trace allowance. Schemas outside the supported structural adapter remain unavailable or unclassified. The recursive-premise layer below extends these cases. Arbitrary computed wrappers, unsupported mutual schemes, an AI-origin benchmark and measured inspection benefits remain open. These records are native attestations with structural audits, not portable kernel certificates or certified prose equivalences. The general goal remains active; the blog is unchanged.

Riccati case split · Recursor model · Compiled-data audit · Fresh native controls · Browser checks

Constructor fields and recursive premises

The elimination rule now distinguishes a constructor field from a recursive premise supplied to the corresponding minor input. Classification reads the compiled reduction right-hand side. A direct reference to a constructor binder is a field. A call to the exact attested recursor, with unchanged parameters, motives and minor premises, and a constructor field as its major argument, is a recursive premise. A lambda family forwarding its arguments to that field is supported. Other shapes remain unclassified; mutual or nested schemes are not covered by this pattern merely because their names resemble recursors.

Show kernel rule geometry, inside a case view, opens the same constructor, telescope, application and binding notation in a separate kernel-rule namespace. Its formal rule binders and recursive calls are metadata, not additional source-proof calls or execution events. Selecting a rule node refines only this cut. The original branch input buttons still open exact source lambda occurrences. Each recorded input reports its number of references in the branch body after all inputs; zero references remain zero. This is a syntactic count, not a claim of semantic necessity. Missing source lambda judgments or an exceeded traversal budget yield unavailable counts.

The controlled corpus adds one separately labelled edition to the existing compiled library. It contains 85 declarations from a self-contained Lean 4.33.1 module importing Lean, including generated helpers. Nine selected declarations supply 88 native type queries, 13 complete recursor-call representatives and 38 classified minor inputs: 22 fields and 16 recursive premises. They cover natural numbers, lists, binary trees, a function-valued recursive family, an indexed family and an ignored induction hypothesis. An independent native-Expr traversal agrees with all 38 input roles and source-body reference counts. Exact-context queries are retained separately when one lambda node is shared under different routes. No original private project source or tactic script is added to the public package.

Three deterministic sharing controls use 85, 181 and 421 stored nodes. The largest has 12,912,720,851,596,686,131,202 expression occurrences, including its statement and proof, and opens with 24 displayed vertices. The source-reference count for its outer input is 2,379,629,985,508,532,158,464, computed in 390 scoped DAG states. A separate algorithm control counts 2^80 repeated references in 81 states. Exact integer accounting and immutable shared packets avoid expanded-tree allocation. The kernel-rule cut retains the existing limits of 32 vertices, depth three, six vertices per layer and four visible application ports.

The packet audit validates all 85 exported declarations, 140 rule cuts and 90 modified-record controls. The preceding two snapshots remain separate and unchanged. The module generator and native-expression oracle are reproducible without either private project. Browser checks exercise all 13 case views, rule-local navigation, exact source-binder jumps, indexed/family cases, zero-use inputs, delayed loads, optional failures and phone/desktop accessibility in both themes.

These controls are assistant-authored synthetic formal examples with deterministic expression amplification. They establish this representation’s structure and sharing behavior on the stated inputs. They do not establish an independently sourced AI-proof benchmark, scaling across arbitrary recursors, general semantic compression, or measured human understanding. The general research goal remains active. No blog entry is added for this implementation milestone.

Natural-number induction · Recursive family · Shared proof · Input model · Compiled-data and native audit · Reproduction driver · Browser checks

Checked local-definition substitution

The let rule represents let x : A := v; b as two source premises and one computed result. The declared type and value belong to Γ, before the binder. The body belongs to the context Γ, x : A := v, which retains the local definition. One ζ step produces the capture-avoiding substitution b[v/x]. Other lets and beta redexes remain unchanged. Every premise has an exact source occurrence route. The result uses a separate computed-term namespace with explicit links to the original Γ; it does not acquire source occurrences or additional inferred judgments for its descendants.

The native extractor checks the declared domain’s sort, the value at its declared type, the body in its local-definition context, the substituted body type, and the result at the selected term’s type. Kernel conversion alone is insufficient to identify a transformation of proof terms because of proof irrelevance. A separate serialized-DAG algorithm must reproduce the exact native substitution result, including binder names, metadata and retained lets. The occurrence identity size(result) = size(body) + references(x, body) × (size(value) − 1) is checked separately using the scoped reference counter. Counts include type annotations.

The released AI-source sample supplies 48 native checked let steps in seven declarations, one exact representative occurrence for every stored let node. The independent substitution matches all 48 complete result graphs. Nineteen selected judgments overlap the primary type inventory and agree. The audit checks 281 representative computed cuts, 57 independently resolved scope links and 556 changed-record controls. The largest result contains 92,227 stored nodes and 45,769,074 expanded occurrences. The initial result cut retains a bounded number of vertices; hidden regions retain complete roots and exact counts. Substitution can increase expanded size, so this rule is not presented as compression.

Sixteen fresh core-only examples cover proof, value and type results, dependent domains and results, shadowing, a value outside its own binder, a function-valued input, unused bindings, nested lets, retained projections and metadata, universe-polymorphic contexts and an 80-level shared term. Their 591 computed cuts and 113 rejection controls include two different same-proposition proof variables: native proof irrelevance permits conversion, but replacing the actual substitution result with the other variable is rejected by structural comparison. A wrong-typed let value is rejected by the kernel.

The computed DAG is capped at 131,072 nodes, substitution at 524,288 work states and binder depth at 512. The view uses at most 32 term vertices, three levels below its root, six vertices per layer and four application ports. These are finite native attestations and structural audits, not a browser kernel or portable certificate. Another occurrence of the same shared let does not inherit a typed reduction record. Source scripts and compiler logs remain private. The research goal remains active; no blog post is added.

Let example · Rule model · Corpus audit · Native controls · Browser checks

Types of local-definition premises

A recorded let step supplies three occurrence-type observations as well as its computed substitution result. These now use the existing type-expression language: the declared type’s inferred type, the value’s inferred type and the body’s inferred type. The value’s declared type is a separate component, linked by the recorded native conversion check. A checked type does not supply an application trace, a lambda rule or a further let reduction for its subject.

The declared type and value keep Γ, before the new binder. The body keeps Γ, x : A := v, including the local definition. Every component retains its source child route, original native query and type-graph root. Direct checked queries take precedence over derived observations at the same path. Premise inspection needs only the checked metadata index; it does not load a computed-result pool. Type-only navigation preserves the selected proof occurrence; source and context jumps select exact original routes.

The 48 released let records contain 144 premise-type observations, 48 per field. Sixty-five paths were already reachable through primary observations or direct let queries; 79 additional paths are now available. There are still 48 native let queries, with no new inference or claim of complete type coverage. All 144 types agree with their native fields and exact contexts; the audit checks 336 type scenes and rejects 799 altered-record cases. Declared-type presentations are summaries of the compiled type constructor, rather than invented native pretty text. Value and body type text retain the native presentation. Four of the 48 value judgments have structurally different inferred and declared types; the recorded kernel conversion check relates them, while the diagrams preserve both expressions.

Fresh core-only checks reuse the 17 native examples and 18 queries. Their 54 premises and 72 type scenes include a universe-polymorphic example whose value and body types refer to the same outer type binder at different bound indices, a body type referring to the current let, and one shared let under distinct outer contexts. A body that is itself an unqueried let gets a type observation without acquiring a reduction record. The suite checks 593 computed cuts and 135 rejection controls. Browser checks exercise all 192 parent components, 144 exact child selections, keyboard source/context links and four accessibility configurations, without requesting a result pool.

These results extend exact typed navigation for the stated records. They do not establish new kernel certificates, complete occurrence typing, semantic compression or measured proof-inspection benefits. The general research goal remains active; the blog is unchanged.

Premise example · Observation model · Type geometry · Data audit · Fresh native checks · Browser checks

Root conversion frames and structural correspondence

A conversion frame connects two complete type-expression roots in the same recorded context. Its gold relation is the native conversion attestation, with the exact query, field and type roots retained. The two type regions keep separate namespaces and their own lexical links. The rule covers the recorded function/domain/result conversions of applications, lambda function/domain/sort/body conversions, let value/sort/result/substituted-type conversions, beta result types and recursor argument/core types. Kernel normalization of a domain sort is labelled separately from checking a term at a convertible type. Whole-term beta, zeta and recursor transformations retain their existing rules; a type conversion frame does not reconstruct a normalization sequence.

The frame also supplies an ordered structural partition of the two roots. Equal relative syntax is a closed region; matching constructor fields may be refined; a different constructor or payload is a boundary. Binder names, universe payloads and metadata participate in exact syntax comparison. Identical bound indices inside different type binders remain separately scoped occurrences. A native conversion of roots does not imply conversion of aligned children, so no descendant receives a conversion attestation from this partition. Paired region buttons refine both views; independent type navigation preserves the original proof selection. Source and context actions identify exact original occurrences.

On the frozen packages, 1,382 checked query entries supply 11,166 relation records in 14 families; 341 relate structurally different roots. Counts include repeated queries and stages wherever stored in the primary, AI-source, recursion, beta, let and recursor packages; they are not counts of unique mathematical equalities. The audit checks 22,332 type cuts, 8,734 independently resolved scope links and both complete occurrence partitions. It also checks altered-record controls and an 80-level shared comparison that reaches an explicit finite frontier without expanding its occurrence tree. The class table is bounded by 65,536 type nodes. Each visible side has at most 24 term vertices and three levels; the structural partition has at most 48 records and six levels. These are different, explicitly accounted cuts. The adapters also pass on 582 derived observation entries with 3,881 reused root relations, retaining their original query/field provenance without adding native checks.

Fresh core-only fixtures check the same adapters on native type, lambda, application, beta and let records, including aliases, dependent contexts, shadowing and a shared let under different binders. Opening a let conversion uses the already verified metadata and fetches no computed-result pool. Four released let values have identical printed inferred/declared types but different compiled ordering-instance expressions; both graphs remain available. This is a finite representation result, not a new kernel certificate, descendant equivalence theorem, complete typing inventory or measured comprehension result. The general goal remains active; the blog is unchanged.

Conversion example · Conversion model and renderer · Full recorded-pair audit · Fresh native model checks · Browser checks

Composed typing rules

Show judgment geometry, available at a compiled occurrence in the compiled library, composes source rules into one bounded diagram. Premises appear above their conclusion. Lambda and let body frames extend the original context by one binder; domains and let values retain the preceding context. Selecting a judgment inspects it locally. Open source selects its exact occurrence in the shared graph/Lean reader and the article index when that occurrence is indexed. Local focus, source-region paging and pan/zoom do not change the original proof selection.

The ordinary scene contract is ProofAtlasJudgmentScene/3; the optional frontier policy below uses version 4 and checked introduction frames use version 5. Native constructor layouts are described below. A complete application spine retains its head, every ordered argument and every original application occurrence. Native function/argument/result roles, binder visibility, dependency and complete-root type-conversion checks remain attached to each stage. A recorded stage with proof-valued function and result is labelled → elimination only when its argument is a proof and the normalized Pi body does not use that binder. Other such proof stages are ∀ elimination; remaining stages are Π application. This classification describes the compiled typing rule, rather than the mathematical importance of the argument. A declaration reference is not automatically a lemma. Proof terms inside a declaration type or binder domain retain that source-region label, including instance proofs used by numeric notation.

Lambda introduction, local definition and checked recursor applications use their existing native records. Recursor branches retain the constructor-to-original-argument mapping, including wrapper permutations and trailing application arguments. Let composition uses the validated premise metadata and does not fetch its substitution-result pool. A parent record can supply its child’s type, but cannot supply an unrecorded child construction rule. Such children remain typed boundaries. A bound variable retains its exact lexical target; a target outside the current cut is an explicit context boundary.

The default cut has at most 13 judgment vertices and depth three. It retains a complete, paged catalogue of source premises even when they are not drawn. Each compound rule partitions its source region: its retained constructors plus its premise regions equal the original expanded count. Across the cut, retained occurrences plus hidden occurrences equal the selected root’s count. This is exact source accounting; displayed judgments are not a proof-size or comprehension measure.

The finite audit covers 1,288 selected regions in 34 declarations from the published, working, released AI-source and recursion-control inventories. The overlapping cuts contain 975 application, 941 introduction, 190 local-definition and 84 recursor vertices; these are appearances across cuts, not distinct native queries. All source arguments, scope transitions and 1,103 bound-variable link appearances pass independent source checks. Changed scene records are rejected in 448 controls, including the optional frontier policy and introduction frames. Twenty fresh Lean 4.33.1 core-only definition controls query all 1,169 source occurrences, including nested composition, dependent application, shadowing, local proofs, case analysis and mixed instance roles. Their ordinary bounded cuts retain 1,666 lexical-link appearances and reject 181 changed-record or unqueried-construction controls. Both ordinary and proof-focused policies pass all 1,169 native cuts; the additional grouped checks are described below.

This layer composes the available native records; it does not infer missing records for every source occurrence, reconstruct tactics, certify prose equivalence or establish human readability. Proof-valued instance arguments and computational terms remain present. The fixed AI-source sample is still small. Corpus-scale rule extraction, packet paging and measured inspection tasks remain open.

Scene model and renderer · Finite corpus audit · Fresh native reproduction · Browser checks

Proof-premise frontier policy

Follow proof premises is an optional cut policy in the composed geometry. The existing default and source-order policies retain their version 3 outputs. Version 4 selects one pending source region at a time across the whole frontier: proof arguments first, function heads next, then other eligible inputs, with source discovery order breaking ties. A newly exposed proof premise can therefore be explored before earlier data inputs consume the display budget. The browser limit remains 13 vertices and depth three; the model supports at most 32 vertices and depth eight. This selection operates on recorded rule ports, without enumerating the expanded occurrence tree. The source packet and its type evidence remain resident; this is not packet paging.

Only a numbered argument of a proof-valued rule can be intentionally folded, and only when its recorded role is type, or its recorded role is value and its kernel binder information is instImplicit. Proof-valued instance arguments, ordinary value arguments, function heads, unknown roles, lambda domains and let headers remain eligible. This does not infer whether the surface author supplied an instance explicitly. A type or instance-value input may itself contain proof terms. Its complete source subtree, exact route, context, type provenance and expanded count remain in the ordered, paged input catalogue. Opening it makes that exact subtree the local root; Open source uses the existing shared selection. Folding records no term rewrite or new typing judgment.

Every intentionally folded input remains a frontier boundary. The displayed rule constructors plus all hidden source regions still account for the selected subtree exactly. foldedInputOccurrences is a subset of the hidden count, never an additional term in that sum. Source-only constructor layouts have no inferred argument roles and are not folded by this rule. Scope links and constructor, projection, recursor and let interfaces keep their original contracts.

At fixed budget 13 and depth three, the 1,288 recorded query cuts in 34 declarations expose 1,373 checked proof-rule appearances with the new policy, compared with 1,349 under the default: 14 cuts increase, 1,274 are unchanged and none decrease in this finite sample. Proof-valued vertex appearances increase from 2,598 to 2,676: 28 cuts increase and 1,260 are unchanged. The cuts intentionally fold 519 input regions representing 30,431 source occurrences. These are overlapping sums across cuts, not distinct proof steps or compressed proof size. On a recorded Riccati subregion at route 1:1.1.1.1.1.1.2.2.2.2.2.1, the same 13-vertex budget exposes seven checked proof rules instead of five.

A fresh native counterexample, AtlasCompose.wideProofHead, applies a proof-valued lambda to twelve proof arguments. At the same 13-vertex budget and depth three, its application region shows two checked proof rules under the default and one under the new policy: the twelve arguments fill the cut before the lambda head is opened. No input is intentionally folded in this example. Thus the policy does not monotonically improve the number of visible proof rules in general. At budget 32 and depth eight, both policies expose nine rules. The selection tradeoff is retained as an explicit regression assertion; the default remains unchanged.

The fresh native controls keep proof-valued instances eligible and fold value-valued instances. Two explicitly checked folded inputs contain proof subterms, testing the boundary warning and complete source recovery. Source-only constructor checks reject invented role classifications, and native projection cuts preserve their structure input. Browser checks cover policy switching, folded-input inspection and exact source jumps, unchanged article synchronization during local navigation, phone/desktop fit, both themes and keyboard accessibility. These checks establish recoverable source cuts; they do not show that the policy is optimal, that every proof gains visible structure, or that people understand proofs better.

Checked introduction frames

Checked introductions in the Grouping selector contracts a consecutive prefix of proof-valued lambda introductions into one ordered context frame. Each member must have its own recorded native lambda construction and a proof-valued body; a type observation alone cannot supply a missing construction. Grouping stops at a non-lambda, a missing native construction, a value-valued function introduction or sixteen members. It does not cross a let definition or recursor application. The earlier source-only telescope rule is a separate syntactic abstraction and does not supply these typing records.

ProofAtlasJudgmentScene/5 retains every member’s source occurrence, original domain/body ports, native type and premise references, binder visibility, context, conversion checks and attestation. Domain i uses the context before binder i; the continuation uses the context extended by all N binders. The source partition is N retained lambda occurrences + all N domain regions + continuation = original subtree. Intermediate body regions overlap and are retained as navigation/provenance links, rather than counted again. No represented expression or type is rewritten.

A bound-variable link keeps its original target path. When that binder is inside a displayed frame, displayTo identifies the frame and binderSlot its one-based member position. Otherwise the original external-context boundary remains explicit. Shared DAG identifiers, shadowed names and displayed frame positions do not determine binding. The inspector pages eight members at a time; each binder, domain and continuation opens its exact original source region. Focus frame continuation changes the local root while preserving the graph/Lean/article selection. Open binder in source changes that shared selection. Turning grouping off restores the ordinary scene. The default remains thirteen vertices and depth three; the depth control offers levels two through six, within the model’s existing depth-eight bound.

The compact card explicitly labels the body type in the extended context, while the inspector keeps the original full quantified type and all native premise references. Recursor branches show the constructor identity from the recorded native branch-to-source mapping. These labels do not infer a tactic history, mathematical lemma boundary or article correspondence.

At fixed budget thirteen and depth three, the finite audit checks 2,576 grouped cuts over the same 1,288 queried regions in 34 declarations. Its type providers are the recorded query/premise inventories; the optional constructor catalogue is excluded from this comparison. Here a non-introduction proof record means a proof-valued application, recursor, local definition, construction or projection record.

Priority	Non-introduction proof-record appearances before / after grouping	Cuts with more / equal / fewer such records
Default proof-first	554 / 691	90 / 1,198 / 0
Follow proof premises	568 / 802	124 / 1,164 / 0

Across twenty declarations in the released AI-source sample, proof focus with grouping improves 49 of 204 queried cuts and increases these record appearances from 332 to 446. All 88 queried cuts in the nine controlled recursion declarations are unchanged on this metric. This is a finite source-cut comparison, rather than a massive-AI-proof readability benchmark.

The cuts contain 291 / 327 frame appearances retaining 1,970 / 2,301 introduction-record appearances under the two policies, with 89 variable-link appearances targeting retained frame slots across both. These are overlapping sums across cuts. Displayed frames, retained construction records and retained source occurrences are separate measures: one application record can itself retain multiple native application stages. These counts are not mathematical proof steps, compressed proof size or evidence of comprehension.

Fresh Lean controls check 3,507 grouped cuts: all 1,169 source occurrences under all three priority policies. A twenty-binder proof checks the sixteen-member bound, the remaining four-member frame and variable references into both. Twelve changed-slot, wrong-display-target, changed-type-reference and changed-context controls are rejected. A proof-variable shadowing control targets the correct inner slot; dependent headers, unused hypotheses, let boundaries and deliberately unqueried child constructions retain their original scope and availability. An additional native control reuses the same two-lambda proof DAG under two source routes: the shared binder node has two distinct actual targets and two frame identities under all three policies. Both previous scene formats remain available when grouping is off. Browser checks cover member paging, domain and continuation focus, original binder-source jumps, slot-qualified references, case labels, reversible depth/grouping changes, article synchronization and keyboard access in both themes at phone and desktop widths.

In the selected Riccati region representing 55,415 source occurrences, grouping at depth four exposes five non-introduction proof records instead of three: the additional records are native And eliminations. At depth three both cuts still expose three. The analytic applications remain further inside the branches. This is a specific access improvement through the logical context; full-proof readability, complete occurrence typing and packet paging remain open.

Checked context frames

Checked context frames extends the introduction rule to a single chosen source-premise chain through proof-valued lambda introductions, proof-valued local definitions and checked recursors with exactly one minor premise. Each selected continuation must itself have proof role. A member needs its own native construction record; a type observation inherited from a parent does not supply a construction. A recursor with two or more minor premises remains a visible split. Ordinary applications, projections, value constructions and unavailable construction records end the chain.

ProofAtlasJudgmentScene/6 retains every member’s original source route, kernel kind, context, judgment type, ordered premise ports, native checks and attestation. Recursor metadata, argument stages, binder visibility and let type/value/body interfaces remain on their original members. The frame has no new kernel rule. The compact card labels the final continuation type in its own context; the inspector retains the original root judgment and all intermediate judgments.

The frame interface contains every off-chain source region and the last continuation. Intermediate continuations identify the next retained member and are not counted twice. Its source accounting is sum of retained member constructors + all off-chain regions + last continuation = original subtree. An application member can retain several kernel application constructors; construction-record counts and source-occurrence counts remain separate. Aggregate ports identify their original member, field, source route and scope extension. The inspector labels each premise with its original context size.

Binder slots enumerate only lambda and let binders; recursor records do not introduce source binders. Every variable link keeps the exact original target path. A frame identity and binder slot are additional display coordinates. Shared DAG nodes under different source routes therefore retain different binder targets. The inspector pages eight records and twelve source premises at a time. Member and continuation focus preserve the shared graph/Lean/article selection; source jumps change it through the existing synchronizer.

A frame retains at most sixteen construction records and 256 interface ports. The model can use smaller limits for controlled comparisons. It records whether it stopped at the member bound, premise bound, unavailable construction, or another construction. A size bound does not claim that the following source region has another eligible member. All deferred regions remain accessible. The default is still individual rules, thirteen displayed vertices and depth three; the earlier scene formats remain available through individual-rule and introduction-only modes.

The finite audit checks 2,576 cuts over 1,288 queried regions in 34 declarations, with the same vertex/depth budgets and native providers as the introduction-only comparison. It excludes the optional constructor catalogues. Here an ordinary proof call means a proof-valued application, construction or projection; introductions, local definitions and recursors retained inside frames are excluded from this metric.

Priority	Ordinary proof-call appearances: introduction-only / context frames	Cuts with more / equal / fewer
Default proof-first	368 / 427	29 / 1,259 / 0
Follow proof premises	459 / 501	24 / 1,264 / 0

All gains on this metric occur in the twenty-declaration released AI-source sample: 29 / 24 of its 204 queried cuts improve under the two priorities. The published and working snapshots and the nine recursion controls are unchanged on this metric. These are overlapping cut appearances, not distinct mathematical proof steps, a massive-AI-proof benchmark or evidence of semantic importance. The cuts contain 324 / 356 frame appearances retaining 2,757 / 3,080 construction-record appearances, with 253 variable-link appearances targeting frame slots across both policies.

The auditor reconstructs every primitive interface and independently checks the resulting source partition and lexical bindings. It rejects 45 altered order, scope and type-reference controls and six invalid mode/bound combinations. Twenty fresh Lean core-only definitions check 3,507 context-frame cuts, covering all 1,169 type/body source occurrences under three policies. Their frames retain introduction, let and single-case recursor records and 884 slot-qualified variable-link appearances. Twelve independent corruptions are rejected. Smaller member/premise bounds, unavailable construction records, dependent witnesses, nested single cases, shared proofs and an explicit two-case split have targeted controls.

In the selected Riccati region, two ten-record frames expose the end of both logical contexts while accounting for all 55,415 source occurrences. Their continuations are applications without recorded construction rules. They remain explicit typed boundaries; grouping does not create missing application evidence. Browser checks cover all three modes, record paging, original-context labels, exact member/binder jumps, unchanged article selection during local focus, the additional AI-source application and four accessibility audits across phone/desktop widths and both themes.

The complete source packet and native type evidence remain resident. Record/port/vertex limits bound this representation, not total application memory. Packet paging, complete construction coverage and measured proof-inspection tasks remain open. Fitting the complete cut can make formulas small; zoom and exact source inspection remain necessary.

Context-frame model · Finite corpus comparison · Primitive-interface and independent source audit · Native controls · Browser checks

Native query composition

The same paged view now loads individual native records through a hash-checked occurrence index. It preserves direct queries and derived application/lambda, recursor, beta and let observations, including their original native archive and source/type references. Missing evidence and failed loading remain different states. The complete article/library loaders retain their existing behavior.

The finite inventory comprises 48 packages in 34 declarations: 1,382 original records, 3,188 selected observations and 1,177 own-query lookup values. Complete-reference checks cover those values and 23,184 complete scenes under the same priorities/groupings as source paging. A provider-kind control shows why a prepared cache cannot be keyed by archive/query alone: ordinary typing and beta composition can interpret the same checked archive differently. Native record identity therefore includes the provider kind.

The initial thirteen-region SBracket.mk.inj view retains fifty-nine construction records and consults sixty-five native records. Their decoded JSON totals 2,088,296 bytes; the separate shared type graph occupies 639,823 bytes. The original complete evidence package occupies 28,093,346 decoded bytes. These are serialized view-specific working sets, not browser-memory or comprehension measurements. Query caching is capped independently of the source cache; shared type graphs remain resident within explicit fixed bounds. The released-AI case retains its 29,794,821-occurrence body accounting without complete-package requests.

The mechanism preserves the existing geometric language under partial evidence delivery. It does not add native typing observations, establish semantic proof compression, reconstruct tactics or demonstrate human understanding. Other source-backed provider families, shared-type paging and proof-inspection tasks remain separate work.

Protocol and reproduction · Native producer · Complete-reference check · Failure and namespace controls · Browser checks

Native constructor layouts

Inductive datatype constructor metadata (Lean’s ConstructorVal) adds a second relation to the composed view. The input is Lean’s ConstructorVal, rather than a declaration-name convention or a match on the function type. A complete source spine retains the constructor head, every parameter, every field and every original application prefix in native order. These are datatype constructors, not additional constructors of the twelve-kind kernel Expr grammar. An implicit index may be a constructor field; it is retained. A partial reference reports its remaining inputs and is not labelled an introduction. Ordinary definitions named .intro and wrappers around constructors retain their application structure.

Display	Evidence	Type scope
Solid typing rule / construction	Existing exact occurrence judgment, native application checks where arguments are supplied, and a structurally matching native constructor head type	Recorded source context Γ
Dashed constructor layout	Native declaration metadata, exact constant identity and universe instance, source arity and ordered arguments	Missing occurrence/argument types remain unavailable
Boundary	Exact compiled subtree, without a matching construction rule	No inferred type is invented

Constructor layouts introduced ProofAtlasJudgmentScene/2; the field-projection rule below extends it to version 3. Source-only layouts are available even when there is no individual occurrence-type query. Their cards show source expressions rather than repeated unavailable-type text. Native constructor signatures are presented separately as generic declaration metadata. Every original application prefix remains directly navigable. Formal field domains use the preceding inputs of the constructor telescope; they are not the actual argument types in Γ. Result-index expressions retain that metadata namespace and telescope context. Recorded source argument types, when available, keep their existing native roots and context. Recursor reduction-rule roots and their binders use the separate kernel-rule and kernel-rule-context namespaces.

The four catalogues cover every referenced constant name in the 2,203 compiled packets: 1,600 names in the published snapshot, 2,494 in the working snapshot, 476 in the released AI-source sample and 96 in the synthetic recursion corpus. All names resolve in their recorded native environments. They yield 27, 34, 10 and 17 constructor records, respectively, with 101 native universe instances in total. Lean supplies each instantiated constant type, including its universe simplification; the browser does not approximate that operation. Source-file and compiled-module hashes and dependency revisions are checked before and after extraction from the existing project environments. Original project scripts remain private.

The census of 2,100,910 stored Expr nodes finds 18,203 regions with complete constructor arity and 18,081 partial references or application prefixes. These counts include declaration types, proof/definition bodies and recursor rules, across overlapping snapshots; they are not distinct mathematical proof steps. The census uses literal constructor heads. Metadata-wrapped heads, aliases, quotient primitives and non-constructor introduction theorems are not silently reclassified. The 656 bounded source-layout checks retain every parameter/field and exact hidden-region count, with 261 independently resolved lexical-link appearances and 357 changed-metadata, wrong-source or wrong-type controls. Three additional checks keep kernel-rule contexts separate.

The released typing inventory supplies three directly checked complete constructor application traces, all in the AI-source sample. Their actual head types and argument slots match the native metadata. Forty-one owned constructor/inductive declaration signatures also match the original compiled packets structurally. It supplies no partial constructor application trace. Source-only recognition does not fill that typing gap. Fresh Lean 4.33.1 controls therefore also query partial calls, dependent pairs and indexed constructors, logical and data constructors, nullary constructors, two universe instances requiring simplification, and ordinary proof/data functions named .intro. The 20 declarations yield 444 source cuts, including 30 partial typed application appearances; misleading ordinary names remain ordinary applications. A shared constructor body under two different lambdas retains two distinct lexical contexts when opened through either rooted index. The public recursion catalogue is independently replayable and preserves all compiled fields. Private project catalogues remain native extraction attestations, rather than portable kernel certificates.

The same view can index constructor regions inside the current selected subtree, including through unrecorded-rule boundaries. The index offers native-family filtering, optional partial references and twelve rows per page. It uses one representative route per stored node within the selected root, rather than enumerating every expanded context. Work is bounded to 131,072 visited nodes and 524,288 inspections; source routes remain bounded to 512 slots. Counts and route/list truncation are reported explicitly. The audit checks discovery against independent reachability and arity counts in all 4,368 compiled roots, with 18,421 listed complete-arity representatives across those overlapping root queries. Limits and partial-reference discovery are checked separately.

The reader retains one decoded constructor catalogue and serializes catalogue loads. Constructor layouts do not load substitution-result pools. Exact source selection, local inspection, pan/zoom, phone fitting and the existing article synchronizer remain shared. Missing or corrupt optional metadata leaves the source graph and existing typing rules available. This is a structural construction layer; it does not infer all occurrence types, reconstruct tactics, certify article equivalence or establish human comprehension.

Native metadata extractor · Bounded extraction · Whole-inventory census · Fresh native controls · Public replay · Compiled metadata

Derived constructor expectations

The next rule instantiates a native constructor signature with the preceding arguments at an exact source occurrence. For input j, it substitutes arguments 1 through j−1 into that input’s native domain. For a partial call, it can also show the next input domain and the residual dependent function type. For a complete call, the residual expression is its expected result. Later missing inputs are not replaced by invented terms.

The output uses the separate constructor-expectation namespace and ProofAtlasConstructorExpectation/1 derivation record. It records the native instantiated signature root and catalogue hash, ordered source argument routes, original source context and capture-avoiding method. It is distinct from generic constructor metadata and from recorded inferred argument types. No new kernel typing or conversion check is claimed. Universes come from Lean’s existing native instances; this operation does not normalize universes or reduce source expressions.

Simultaneous de Bruijn substitution lifts the external variables of an inserted source argument under any local binders in the signature. The argument’s own internal binders remain intact. Lambda/forall domains and let types/values use their preceding scope; bodies use the extended scope. The implementation memoizes states and interns the result DAG without expanding shared occurrences. Default limits are 32,768 result nodes, 131,072 traversal states, 8 MiB of interned identity strings and depth 512. Reaching a limit leaves the original source and its typing view available with an explicit unavailable result. The reader holds one selected derived expression, with at most twelve expected-input controls per page.

The same bounded geometric vocabulary draws these expected expressions, using ProofAtlasGeometricScene/8. Computed descendants have their own routes, not fabricated proof occurrences. Context links return to original source binders; kernel-rule context remains separate. Expanding a computed node does not add a type judgment. The derivation checker recomputes the expression and provenance from the bound source and native signature; the scene checker separately checks its cut and binding links.

Fresh Lean 4.33.1 controls cover 26 declarations, including dependent Sigma/Exists fields, indexed constructors, partial references, universe simplification, shadowing, nested domains and let scopes. A shared equality-constructor body opened under two different binders retains two different context targets. All 224 queried expected domains and 99 residual constructor types match the independently extracted native expressions structurally. Their 323 bounded scenes retain exact occurrence accounting and context links. The released inventory contributes three directly checked constructor application traces with twelve native expected domains; broader occurrence typing remains unavailable.

Across the four released catalogues, 164 sampled source layouts and 19 kernel-rule contexts produce 183 bounded expected-expression scenes. These are constructor/status samples, not all-occurrence typing coverage. The audit rejects 1,537 changes to derivation records, source identity, components or limits. A separate synthetic shared-argument control represents 9,671,406,556,917,033,397,649,407 expanded occurrences with 167 result nodes and 168 traversal states. This is a structural sharing control, not a massive AI-generated proof benchmark or a measurement of comprehension.

Derivation and scene adapter · Released-data and sharing checks · Native comparison · Own synthetic controls · Browser checks

Native field projections

The geometric vocabulary now composes kernel field projections with native function introductions and applications. A solid projection rule retains the exact Expr.proj source occurrence, its single struct input and the native result type. Its field index is zero-based and excludes constructor parameters. The displayed field name comes from the checked constructor telescope. Named projection functions, inherited accessor wrappers and ordinary functions with similar names retain their original application structure; the actual primitive is visible when its declaration body is opened.

A projection result can depend on earlier fields. The extractor checks the operand type, normalizes that type to its recorded single-constructor family, instantiates the native constructor type at its exact universe instance, and supplies the structure parameters and preceding kernel projections in order. Lean checks each preceding projection against its field domain and checks the selected projection against the resulting expected domain. The inferred result type and expected field type remain separate roots, related by an attested kernel conversion at those complete roots. This relation does not assert equality of their descendants.

The browser independently reconstructs the expected field domain by capture-avoiding instantiation of the native telescope. It checks family/constructor identity, field ordering, parameter expressions, preceding projections, original operand syntax, exact context and full source cuts. Constructor metadata has its own namespace; reconstructed earlier projections in a type graph do not acquire invented proof occurrences. Kernel, extraction-environment and packing provenance remain attached. No browser Lean checker or portable certificate is claimed.

ProofAtlasJudgmentScene/3 gives a typed projection one structure-input port and one retained source occurrence. The accounting identity is 1 + size(structure input) = size(projection). Missing occurrence evidence leaves a dashed source layout with that same recoverable input. It does not borrow another route’s projection rule. Existing type observations, when separately recorded at that exact path, retain their own provenance. Selecting the structure or its context binder uses the original source synchronizer; an unindexed article selection remains unindexed.

Across the four frozen inventories there are 229 stored Expr.proj nodes in 222 packets: 108 in each research snapshot, 13 in the synthetic recursion corpus and none in the released AI-source sample. Every stored node has one native checked representative. Another 326 native application/lambda queries retain the selected paths’ enclosing compositions, giving 555 query records. The audit checks all 229 field-domain reconstructions, 687 projection cuts, 222 bounded body cuts and 432 scope-link appearances. Of those 32-node, depth-eight body cuts, 221 expose a native projection rule. This is finite cut coverage, not all-context typing or complete rule coverage of the remaining source regions. Types and bodies can use the same stored node under different occurrence paths.

Fresh Lean 4.33.1 controls query every source occurrence in 14 small declarations: 216 bounded cuts, including 14 primitive projections. They cover type-, value- and proof-valued fields, dependent records, universes, embedded parents, nested records, function-valued fields, let scopes, metadata and an unregistered single-constructor family. The same stored projection under two binders retains two distinct context targets. A named wrapper remains an application, and invalid primitive projections are rejected by Lean. Public-record controls reject 1,794 changes to field identity, instantiation order, source binding, conversion flags or source hashes; the fresh controls reject 99 changed records.

Two additional native-checked stress controls project a value and a proof from record operands containing an 80-level shared arithmetic term. The selected value projection represents 4,835,703,278,458,516,698,824,706 source occurrences; the proof projection represents 9,671,406,556,917,033,397,649,412. Their complete source packets have 169 and 177 stored nodes. Initial cuts draw five and six regions with exact hidden accounting. Four bounded queries per stress declaration check the type root, lambda, projection and operand; the expanded occurrence trees are never enumerated. The combined small/stress suite rejects 114 changed records. These are deterministic synthetic terms with large data annotations, not AI theorem-solving benchmarks or measurements of logical proof complexity.

The six public synthetic packets independently replay all 13 projection records and 92 surrounding application/lambda queries, preserving all compiled fields. Private project proofs are neither rebuilt nor published. Their metadata are extracted from existing compiled modules with source and compiled-module hashes and dependency revisions checked before and after extraction. The reader retains one current projection package and serializes optional package loads, cancelling aborted or stale selections. Each decoded package is capped at 16 MiB; type/metadata graphs and telescope substitution retain their existing explicit bounds. Large shared source regions remain recoverable through bounded cuts. These results do not establish human comprehension, a large AI-generated projection benchmark, source packet paging or complete Lean elaboration coverage.

Native extraction · Field validation · Complete stored-node census · Own native controls · Synthetic replay · Compiled inventory

Source-backed field types

The next transport layer avoids copying an entire source operand into a second expression table. Native Lean checks a projection and its field conversions, abstracts exact contextual source regions into substitution slots, and requires substitution back to recover the original expressions structurally. Slots are ordinary template variables, not an additional kernel constructor. The reader evaluates these substitutions through a bounded graph view and keeps computed parents separate from original source occurrences.

Four synthetic operands contain 196,617–196,634 stored source nodes. Their type templates contain 4–12 nodes; the native-control cuts require 34–41 virtual descriptors during the checks. The cases include a dependent proof field and a function-valued field capturing the outer variable. These are arithmetic-data and reflexivity controls, not difficult theorem-solving or comprehension benchmarks. The previous extractor exceeds its 32,768-node second-table bound on the independent-field case.

The optional reader layer supplies 249 exact projection queries: 229 representatives in 222 frozen-corpus packets and 20 queries in nineteen selected own control packets. The package audit checks 996 bounded type cuts, 392 source-jump appearances and 1,245 rejected record changes. Fresh native extraction compares 98 roots with the existing materialized representation and independently replays all compiled fields of the public own controls. Selecting a borrowed region returns to its exact source route; its variables retain their original binding under computed function binders. Native text is available separately from the diagram.

This field-specific transport covers projection observations. The separate contextual and application compositions below supply source-backed lambda/type and application-stage records. Existing records supply enclosing rules where available. The complete source packet still loads and validates in full. Templates, virtual states, comparison work and metadata decoding have explicit bounds; unrecorded contexts retain source structure. Article correspondence, semantic compression, AI-proof scale and human comprehension retain their separate evaluation requirements.

Dependent control · Method and limitations · Package audit · Browser checks

Contextual type composition

A checked lambda introduction now composes a source domain with its body type without copying a large domain into another expression table. The source lambda and computed Pi binder are distinct occurrences connected by their native introduction record. Domains stay outside their new binder; body observations use the extended context. Source anchors borrowed from an enclosing binder header retain the original occurrence and a checked context extension.

Two own controls contain 196,628 and 196,631 stored source nodes. Their whole-function types exceed the earlier template-table bound; introduction composition reconstructs them with eight-node terminal templates. Across twenty self-contained declarations, 113 selected queries check 108 independent type-root comparisons, 4,541 bounded geometric cuts and 6,974 borrowed-variable binding appearances. They include dependent types, shadowing, local definitions, universe parameters, all binder visibility kinds and a 64-entry telescope. These are arithmetic-data and reflexivity controls, not an AI theorem-solving or comprehension benchmark.

Lexical context prefixes are shared in metadata. Every query in the deep-binder test is retained; the fixture bundle is approximately 6.55 MB after the unshared form hit the output bound. The reader keeps one prepared composition and serializes its bounded metadata loads. The complete source packet still loads in memory.

The optional Show composed type view has 44 exact queries in the nineteen existing own source-reference examples, including a representative for each of their 27 stored lambda nodes. This is stored-node coverage, not all lexical-context coverage. Native conversion to the complete declared type is checked separately: four inferred types match the declared syntax and fifteen differ syntactically. No correspondence between their descendants is asserted. Other paths retain their existing source and type evidence. The current native record rejects more than 64 contiguous introductions; longer typed chains, interleaved large let constructions and packet paging remain open. The application transport below extends selected exact queries to the frozen AI-attributed sample.

Composed example · Method and reproduction · Native controls · Reader package audit · Browser checks

Source-backed application types

Application composition now borrows exact contextual source regions instead of copying them into a second type table. Native Lean checks each function, argument and substituted result before abstraction. Templates must reconstruct those expressions structurally; an independent browser substitution check supplies a separate consistency test. Computed type parents and original proof occurrences retain different identities and exact contextual links.

The frozen AI-attributed sample supplies all 36 application queries in its 175-query primary inventory: 146 application stages in nineteen of twenty compiled declarations. The previous native type records independently agree at 948 roots. The bounded cuts retain 305 borrowed-variable binding links and 4,686 source-jump appearances. The twentieth declaration has no application query in that inventory. These are finite recorded-path checks, not all-application or all-context coverage, and model generation is publisher-attributed.

Seven self-contained controls include a 196,623-node source packet whose result type represents 786,439 expanded occurrences using twenty template nodes. The older materialized table reaches its 8,192-node bound on this type. This establishes a representation counterexample on synthetic data/reflexivity, not a theorem-solving advantage. Source packets remain resident; whole-proof paging, composition with paged introduction chains and human inspection benefits remain open.

The existing library type controls use these records where available. Other selections retain their previous evidence. Example · Method and limits · Package audit · Browser checks

Closed-context typing transport

Show context type derives a selected occurrence’s type from a native checked closed-context representative. A context class retains the original expression, ordered binder headers, visibility, domains and let values. Closed expressions drop their unused ambient prefix; source occurrence identities and binder targets remain distinct. The reader matches the selected route directly, without building the full expression/context index or expanding the occurrence tree.

Native extraction closes the representative term with lambdas and lets, and closes its inferred type with matching Pi/let wrappers. Lean checks the closed term, expected type and conversion in an empty local context. The reader’s separate derivation uses identical retained headers, context-variable renaming and unused-prefix weakening. Computed type nodes use the existing constructor geometry; Γ links point to the selected target’s exact source binders. Native representative evidence and derived target typing have separate identities. No native query, inferred type for a type descendant, or article correspondence is invented.

The finite inventory has 633 native exact routes in 394 context classes: every occurrence in twelve own small control declarations, plus 128 predetermined representatives and 21 predetermined alternate routes in one AI-attributed proof. An older exporter independently agrees on all 633 inferred types. All 239 additional selected routes also pass native checks of the transported type, applied closure and term conversion. These counts do not establish complete type coverage of the frozen AI sample. The implementation is tested, not a formally proved Lean metatheory or portable kernel certificate.

A source-backed closure recipe avoids copying large retained let values into another type table. One selected AI context uses an 81-node raw type and a nine-entry recipe borrowing 59,967 existing source nodes, under the unchanged type-table bound. This derived-type control uses the complete resident source packet. Its exact recorded closure modules have a separate paged path below; paging derived targets and measured comprehension remain open. Missing context classes expose no context-type control. Failed optional metadata leaves the original graph and native type records available.

AI proof example · Own dependent control · Method and reproduction · Compiled evidence checks · Browser checks

Public-packet construction recovery

An internal lambda in the AI-attributed sample had a checked type but no introduction record, so the composed geometry stopped at a typed source boundary. A predetermined union of 17 prior primary queries and 14 proof-role context roots gives 19 distinct queries. Native replay reconstructs them from the public compiled packet, with the original proof module absent. The inventory records ten checked introductions and five checked applications; one application also has elimination metadata. Three local definitions retain their separate earlier records.

At node 30853, proving ¬a = 0 → a = 1 / 2, the recovered introduction distinguishes the seven-entry domain context from the eight-entry body context and records all four kernel conversions. The shared reader vocabulary now draws the introduction rather than a boundary. A recorded body type does not create an internal application rule.

The common schema has a distinct public-packet replay environment and does not assert verification of an original compiled module. Independent checks preserve all 17 previous primary judgments and 62 exact type observations, compare 57 full/paged scenes and reject twenty-three altered records or limit controls. The paged reader’s small supplement has a separate 32-query/256-KiB cap; source traversal remains paged. This is finite construction recovery, not complete proof coverage or measured comprehension.

Method and reproduction · Independent checks · Browser checks

Recorded proof-premise frontiers

A reusable query policy follows native proof-valued premises of recorded constructions, retaining exact occurrence routes. Terminal declaration/context references remain boundaries; source fields and unknown types do not acquire proof roles. Applied to the frozen nineteen-query AI-proof seed, it identifies eight distinct missing construction roots from nine premise appearances. Three requests share node 166 under three different lexical contexts. Both fresh native reproductions check all eight additions, while preserving the nineteen earlier judgments.

The resulting 27-query inventory records twelve introductions, eleven applications and three elimination records within those applications. It supplies a checked application for the previously unrecorded body of lambda 30853. The next layer still has nine unrecorded proof-premise roots: 36 cumulative requests would exceed the small supplement’s 32-query limit. Further expansion needs bounded query paging; the memory limit is retained.

The policy also enumerates candidate frontiers in 34 frozen earlier native-query inventories, with 112 distinct candidate routes in total and at most 31 in one inventory. These candidates are drawn from earlier recorded premise roles; they have not all received new construction checks. The independent audit derives candidates directly from native application, introduction and let fields, checks contextual sharing, and keeps the unresolved next layer explicit. This is finite construction coverage, not complete proofs or semantic explanation.

Policy, limits and reproduction · Independent frontier audit · Corpus candidate audit · Reader checks

Native contextual queries at deep source positions

A separate core-only checker follows original source fields and reconstructs the ordered lexical context before checking a selected expression. It retains one query path plus binder depths rather than copying a complete path for every binder. Domains and let values use their prior context; each new domain and let value is checked before extending it. Recorded types use a computed namespace and must reopen exactly in the original context. Proof/type/value roles come from kernel type checks and normalization.

Finite tests cover eight generated controls and the existing public deep-syntax packet: 27 selected judgments, depth 10,002 and a context of 10,000 shadowed binders. The independent reader compares them with 54 original source cuts. It distinguishes shared variables with the same Nat type but different binders, checks dependent type context and let scope, and refuses nine altered records; eight invalid contexts, paths or terms are rejected natively. The public source control retains its original bytes and producer claim; its new replay is separate.

The occurrence reader can attach these records at their exact hash-bound source positions. A computed type has a separate namespace and original Γ references; type-local navigation keeps the source selection fixed. Native records are optional for the old deep-syntax control and available in the synthetic context controls. Unrecorded positions remain without typing. The original producer metadata stays unchanged. A separate finite audit checks the attachment and type cuts; it adds no kernel judgments to descendants of a recorded type.

These are finite native replay and structural correspondence checks. They do not verify the query/codec/renderer, provide project/AI corpus typing or establish semantic abstraction and human comprehension. The older 512-entry renderer and native transport retain their existing limits.

Method and reproduction · Context checker · Independent compiled reader

Existing project records in occurrence windows

The bounded occurrence reader also accepts the existing native extraction records for five project declarations and twenty publisher-attributed AI-source declarations. Its 1,129 direct queries and 1,174 explicit application/introduction observations remain distinct. Each recorded position retains its exact source route, context, selected root in the shared type table and original extraction provenance. An observation links back to the query that recorded it. A missing position remains without a recorded type.

The type view uses the same constructor ports and scope rules in a separate computed namespace. Type-local navigation preserves the source selection; original Γ links return to exact source binders. In JacobiCore.E_pos, shared source node 17 has both a value use and a proof use under different contexts. The reader preserves those contextual judgments rather than assigning a single role to the DAG node. Shared type arrays are stored once, and the recorded-position list is paginated.

This reuses published judgments; it adds no kernel checks or inventory-wide type coverage. Complete source packets and the selected type table still load within fixed bounds. The browser checks correspondence and does not independently verify private module bytes or original AI generation. Method and limits · All-record correspondence audit · Browser checks. The general program remains active; there is no new blog claim for this bridge.

Recorded uses in ordinary source cuts

The reference rule also applies to an ordinary source cut. A recorded variable use is either a retained source occurrence or lies in exactly one hidden frontier. Retained uses reuse their existing lexical edge; hidden-use references connect their original region to the exact binder or an explicit internal or external boundary. Each reference adds zero occurrences. Source forallE binders remain source type binders, without an invented proof-introduction role. The selected observation types only its original use; the cut remains untyped.

The independent model comparison covers 1,209 cuts, 13,923 reference placements and all 170 indexed uses across 51 profiles. The public-browser audit reaches all 152 indexed uses across 26 extraction profiles, including the 28 outside mixed-interface frames. It checks 204 source cuts, existing lexical-edge reuse at all 152 retained uses, 309 source and binder selections, 308 native-type selections and three retained forallE binder cases. Complete-mode controls, optional failures, stale responses, keyboard access and four accessibility configurations are checked separately. These are finite correspondence results; there are no new native judgments, exhaustive typing or comprehension results. The existing catalogue still omits 141 separate alternate Meta observations.

Reference rule and reproduction · Independent source-cut checks · Browser audit

Visual notation manual and field fidelity

The visual manual separates ordered expression children, lexical references, non-expression attributes and native typing judgments. It documents the twelve semantic Expr forms, scope and occurrence identity, reversible telescopes/application spines, exact frontier accounting, universes and the limits of source/tactic recovery. Its capability assessment separates tested structural laws, sparse native records and unmeasured comprehension.

The older constructor gallery used a generic two-input illustration, omitting the third letE child and obscuring reference/payload roles. It now shares a schema-driven field renderer with the manual. Every semantic field is retained in constructor order, and binder body fields identify the extended context. This corrects representation fidelity; it is not a new native judgment or a comprehension result.

Four authored structural controls use the existing production scene algebra: dependent binders sharing a bound-variable node, a let value outside its new binder, a shared application and a 60-level doubling DAG. They are explicitly not extracted declarations or certified proofs. The manual tests check fields against the pinned catalogue, lexical targets against an independent path walk, cut accounting and folding, corrupted-scene refusals, keyboard selection, external binder navigation, mobile/dark-theme accessibility and continued compiled-library navigation. Exact test results are kept with the release evidence. The blog and mathematical article are unchanged.

4. Context interfaces and references

Scope interfaces for retained regions

A retained source region now exposes its exact free term-binder mentions, including type annotations. Targets keep the original occurrence route and any folded-frame slot. The view bundles these links by context frame, with individual source navigation; it does not classify a syntactic mention as logical necessity. A shared DAG node can use different binders in different contexts, so only its relative support summary is shared. The scene’s original geometry and provenance remain unchanged beneath this additive layer.

Independent finite-set calculations agree with all 395,902 stored summaries in the 34-packet inventory. At 1,288 recorded routes, three priorities and three grouping modes give 11,592 checked cuts and 181,702 binder-target appearances across overlapping views. One 527-occurrence SBracket.mk.inj region mentions 57 external term binders, represented by four introduction-frame bundles of 16, 16, 16 and 9. These results establish structural correspondence, not semantic necessity or improved comprehension. Unresolved objects, unsupported widths and failed evidence remain explicitly unavailable.

Method, bounds and reproduction · Independent audit · Failure controls · Browser checks

Checked context modules

Term-variable ports alone do not retain a typing interface: a proof hypothesis h : p mentions h, while its recorded type also depends on p. The context interface closes the term/type support under binder types and let values, preserving their original order and source routes. This is syntactic support, not logical necessity.

The checked-module prototype represents a closed term and its expected type as separate computed components in the same constructor notation. Each original use keeps its own source map. Retained definitions are rebuilt as lets; only assumptions are supplied as arguments. Native records check the closed judgment, its instantiation and conversion back to each selected term. Matching closed syntax does not merge different context-entry boundaries.

Finite own controls supply 594 observations, 313 modules and 281 further checked instantiations. Geometry checks cover 5,634 cuts and 6,860 inverse mappings; fresh Lean replay matches all 594 stored observations and rejects 31 context omissions. The existing reader exposes term/type geometry, original-use switching, context references and exact source or raw-type navigation. Other occurrences remain unsupported. Three selected AI routes have separate reduced-context native checks in the ordered projection extension below; the other audited interfaces gain no new typing. The source-backed full-context construction below extends this notation to one large proof. Other semantic abstractions and measured human inspection benefits remain open.

Rule, data and reproduction · Geometry and inverse-map checks · Reader checks

Source-backed context modules

The same Show checked context module control now draws the native full-recorded-context closure for 149 exact observations in one frozen AI-attributed proof. Term and expected type use the existing constructor notation, ordered fields and binding links. Only lambda/Pi/let wrappers are created; large term and header regions remain borrowed from the original source. The complete proof body represents 31,752,787 occurrences, and one borrowed let value represents 10,844,757. No occurrence tree is expanded in the paged reader.

Each full-context class has one canonical computed identity. Changing the selected original use preserves that identity and changes the inverse source/binder map. Canonical closed-root typing, selected-use native instantiation checks and raw expected-type structure remain separate records. Focused descendants gain no additional typing judgments. This construction keeps the full recorded context. The ordered projection extension below separately supports three native-checked reductions. The package’s 21 alternate instantiations are types or values, with no alternate proof-role observation.

Across 633 native observations in thirteen packets, the independent audit checks 5,926 cuts and 1,299 displayed inverse variable-link checks, including 239 alternate uses at both term/type roots. The source-paged AI subset supplies 2,182 cuts. Source cache and prepared snapshot limits are separate; raw-type packages and offline materialized references are separately resident. The explicit complete-reader mode retains its full source. This is a finite implementation result, not a general metatheory, semantic proof compression or a measured inspection benefit.

Large proof · Construction, limits and reproduction · Model audit · Browser checks

Ordered context projection

The Required syntactic context mode represents a checked reduced-context closure through source-backed index remapping. Ordered retained slots determine new free-variable indices; internal binders, constructor ports and original source maps remain distinct. Domains and let values retain their pre-binder scopes. The full recorded context remains the default, and unsupported routes receive no inferred reduced typing.

Three exact routes in one frozen AI-attributed proof have separate native reduced-context typing and instantiation-conversion checks. One type-valued closure changes from 9,439,756 to 95 occurrences. Two proof closures change from 575 to 285 and from 20,284,420 to 10,845,049. These are local context-closure sizes, not whole-theorem or semantic compression. The last reduced module exceeds the existing materialized-table limit; delayed projection draws its cuts without copying that table.

Across 594 own native observations and these three AI observations, the independent audit checks 5,582 cuts and 2,031 inverse variable links. In 302 displayed cases the index changes while the original binder is preserved. Existing own native instantiation checks supply the reuse controls; there is no new AI module-reuse result. The browser exposes both term and expected-type components through the same reader control. Full offline references, raw type packages and source caches have separate residency. General metatheory, broader reduced-context coverage and measured inspection benefits remain open.

Example · Rule, scope and reproduction · Model audit · Reader checks

Structural laws for context projection

Seven kernel-checked theorems on an explicit Lean.Expr renaming function establish exact recovery under a partial inverse, composition, injectivity, preservation of expanded constructor counts and internal binder cutoffs. All twelve constructors retain their ordered fields and non-variable payloads. The proofs depend on propext and Quot.sound. They concern syntax, with an explicit inverse condition; they do not establish typing preservation or semantic proof compression.

The bounded JavaScript projection matches the native function on 713 generated primary cases and 1,969 second-stage selections, including missing-variable failures, shadowing, let scope and shared nodes under different binders. These finite comparisons do not prove the JavaScript implementation. The existing native checks of closed context modules and their instantiations remain separate. General typing results, broader implementation verification and measured inspection benefits remain open.

Definitions, proofs, scope and reproduction · Lean source · Implementation comparison

Exact context support

Four further kernel-checked laws characterize free de Bruijn support for the same projection function. Projection succeeds exactly when its partial variable map covers every required index. The structural scope maximum bounds those indices, and a zero maximum is equivalent to an empty set. Binder domains and let values use their original scope; lambda/Pi/let bodies remove their newly bound variable. These are syntax laws, not typing preservation or logical necessity.

A proved counterexample has two terms with the same positive scope maximum but different support: under a b c : Nat, retaining only a admits a and rejects Nat.add a c. A maximum cannot replace an exact dependency interface. The bounded browser summary agrees with native support on 875 generated source nodes at four widths, with conservative withholding allowed; all 713 retained-context decisions agree. Deliberately omitting a lower support index demonstrates why authenticated exact summaries remain an API precondition.

The proofs use the recorded standard axioms propext, Quot.sound and, for two laws, Classical.choice. Unresolved named variables, metavariables, universe data, context typing and metadata semantics remain separate. The laws prove the explicit Lean function; finite comparisons do not prove the browser implementation. General typing preservation, wider evidence coverage and measured proof-inspection benefits remain open.

Support laws and boundaries · Lean source · Summary comparison

Inspecting context dependencies

The Required context diagram exposes the dependency interface already used to construct checked context modules. A selected term, its recorded type or a retained header connects to exact original context entries. Term, recorded-type, binder-type and let-value references keep separate labels. Header inspection follows the syntactic dependency chain within the module; original-binder and recorded-type actions retain their existing namespaces. A page shows at most sixteen edges, with explicit continuation.

The view is available for the own checked-module controls and the three recorded reduced AI contexts. Full-context mode and unsupported selections gain no inferred reduction or typing. Existing native root checks and the finite dependency audit remain separate evidence. This is a navigation layer over the qualified interface, not a new semantic abstraction or a measured comprehension result.

Construction and limits · Browser checks

Least syntactic context closure

Six kernel-checked laws characterize the ordered dependency closure used by context interfaces. If every header dependency points to an earlier binder and every seed is inside the context, the descending pass retains all seeds, stays inside the context and yields the least dependency-closed superset. Reapplying closure changes no membership. For two bounded seed sets in the same dependency graph, closing their union equals the union of their closures. This is a compositional rule for syntactic interfaces, not a theorem of logical necessity or general typing preservation.

All 76 ordered graphs through depth four and all 1,099 seed choices agree between native Lean, the existing browser closure and an independent reachability calculation. The comparison also covers 16,933 union pairs and larger controls up to 512 context slots. A single ascending pass fails on the chain 2 → 1 → 0; the current descending implementation retains all three slots. The proofs use propext and Quot.sound. Finite comparisons do not prove the JavaScript implementation or its support producer. Native types, source identities and original binder maps remain separate requirements.

Definitions, proofs and boundaries · Lean source · Implementation comparison

Reference-chain witnesses

The context interface now supplies one shortest syntactic reference chain from a term/type seed to a retained binder. Its edges retain their relation, original originating region and exact target binder. Header domains and let values stay in their pre-binder scopes; type origins stay in the recorded-type namespace. A source-support edge identifies a region mentioning a binder, not an individual variable-use occurrence or a logical implication.

The search reads the prepared interface without reopening proof subtrees. It retains at most 512 predecessor records and pages chains sixteen edges at a time. Independent source-set and distance checks cover 454 paths across 746 existing observations. Six indirect paths occur in own let controls; audited AI interfaces have direct paths. The browser exposes witnesses only where the dependency interface is already available. No additional typing or measured comprehension benefit follows from this navigation layer.

Algorithm, limits and coverage · Model audit · Browser checks

Reduced-context replay coverage

All 149 routes in the frozen context inventory of one AI-attributed proof now have native reduced-closure checks from their public compiled packet, without importing the original proof module. The kernel checks closed terms/types, expected-type conversion and instantiation back at every original use; an independent offline reconstruction agrees with every native module. All 109 predetermined direct-support omission controls reject for the required free-support reason. The observations form 87 canonical modules and 62 checked alternate instantiations.

Of 93 proper context reductions, two are proof-valued, thirty type-valued and sixty-one value-valued. Alternate instantiations are types or values, with no alternate proof-role observation. These are local closures in a predetermined route inventory, not whole-proof or semantic compression. The protocol reuses the pinned compiled dependencies and preserves the earlier three native roots. It publishes compact compiled evidence, not original scripts or materialized closed graphs.

The broader replay evidence has a distinct public-packet environment. A dedicated reader adapter exposes all 149 recorded routes while retaining the earlier imported-module evidence as a separate fallback. The full recorded context remains the default. Unrecorded descendants, other declarations, general typing preservation and measured comprehension remain open.

Method, coverage and reproduction · Compiled evidence manifest · Independent artifact audit

Replay-backed context geometry

The reduced-context reader now covers the complete frozen 149-route inventory of lean_workbook_plus_6206, using the public-packet replay checks above. Its 87 canonical modules and 62 recorded type/value instantiations retain separate original-use maps. Diagram provenance names the replay environment and qualifies the earlier source-module hash as an input record; the original proof module was not imported for replay. Native judgments cover complete closed roots only.

An independent paged audit compares 1,071 cuts with reconstructed references, checks 124 canonical-use component pairs and 199 variable links, and rejects sixteen altered evidence or typing controls. In 138 variable-link appearances a projected index changes while its original binder is retained. Browser checks prepare all 298 term/type root components and exercise representative visual navigation. These establish finite coverage and structural correspondence, not whole-proof compression, general typing preservation or measured readability.

Reader and adapter boundaries · Paged model checks · Browser checks

Exact accounting of context reduction

Nine kernel-checked structural laws state where context-projection size changes occur. Closing a term adds one wrapper and its type/value regions per header. Successful projection preserves the selected body and each retained header’s expanded occurrence count. Therefore the difference between full and required-context closures is exactly the sum of omitted header weights, with a strict decrease exactly when some header is omitted. This is an identity for actual Lean.Expr constructors, not a general typing-preservation theorem.

The finite arithmetic comparison covers 421 successful and 292 withheld projections in 713 synthetic rows, plus 743 existing native term/type contexts. All recorded reduced root sizes agree; 143 selected contexts strictly shrink. In the type-valued 9,439,756 → 95 example, the selected body remains 93 occurrences and omitted headers account for 9,439,661. These are context closures, not whole-theorem compression or fewer displayed vertices.

The reader retains this distinction in Closure size accounting: each omitted binder links to its original type or let value. The disclosure belongs to the selected use, while canonical module geometry stays shared. No new typing for descendants or measured comprehension benefit is asserted.

Definitions, proofs and reproduction · Lean laws · Corpus comparison · Reader checks

Context size and body access

A fixed-budget comparison separates context-size accounting from access to the selected expression. Across 149 frozen AI-source routes, both components and four budgets, all 1,192 initial full/reduced comparisons retain identical relative body paths. In this inventory the smaller context closures do not expose additional body constructors under the current initial-cut policy. A separate 193-header structural control demonstrates that this equality is not general once the telescope limit is reached.

The optional Focus selected term / Focus recorded type action navigates past checked module wrappers while keeping computed binding links and exact original-use maps. At the reader’s 32-vertex/depth-three budget, 68 of 298 term/type views retain more body constructors and 230 are unchanged. At budget eight/depth two, one view retains fewer. The root policy remains the default. Retained constructors include folded members and annotations; they are not counted proof steps or a comprehension measure.

Full and reduced focused cuts agree on relative body paths, with 19,008 original-constructor comparisons and 514 independent lexical-link checks. Focusing does not infer a typing judgment for a computed descendant. The same navigation rule is available in the own small-proof and source-backed module readers.

Definitions, budgets, counterexamples and reproduction · Finite comparison · Reader checks

Hidden-region interfaces

A fresh core-only counterexample demonstrates that an empty proof-premise frontier can omit a proof-valued application below a value input. The projection, value application and a separate proof-witness query retain their exact source paths and native contexts. The selected projection expands to about 9.67 × 10²⁴ source occurrences but uses 177 stored source nodes. This concerns syntactic coverage, not the mathematical importance of the omitted reflexivity proof.

The Hidden source regions disclosure makes these boundaries explicit. Its source-root antichain accounts for every hidden occurrence in the displayed cut; root roles do not classify descendants. Opaque source children remain untyped. The finite audit covers 612 initial cuts across 34 inventories and 150 current replay cuts, with 9,177 boundary appearances and twenty rejection controls. Preparation is bounded and lazy; individual rows preserve exact source and focus navigation. General semantic abstraction and comprehension remain unevaluated.

Counterexample, rule and limits · Compiled control manifest · Source accounting audit

Composing constructions through original context references

A separate core-only reference model records Π introduction and one stage of Π application at original source positions. Native checks retain the prior domain context, extended body context and dependent result substitution. A composed child must have the same exact premise position, context, role and structurally identical recorded type. Unsupported constructions remain source boundaries.

Query-relative addresses avoid repeating deep source paths for each displayed premise and external binder. They recover the complete packed-route scene against the authenticated native inventory, including separate computed-type origins. Finite checks cover twelve construction records in eight synthetic packets, 108 cuts in each address representation, and a premise at depth 10,002. The same-node type/value and dependent-substitution controls retain their different original binders. This is source/context correspondence and metadata reduction, not semantic proof compression, a verified codec or a comprehension result.

The optional construction lens in the existing occurrence reader uses these interfaces with the frozen controls and 1,018 earlier project/AI construction records. Source selection, computed types and original Γ links stay synchronized. Missing constructions, declaration/context references and type expressions remain explicit boundaries. Native pretty-print text follows its exact type component; distinct Meta and kernel argument-type observations keep separate origins.

The reader stores one packed selected-root path with short field suffixes and original ancestor-prefix depths. Its finite audit checks 108 reference-model comparisons, 3,054 corpus cuts and all 2,036 recorded premise text components. The eleven synthetic controls retain 49 distinct typed positions, including the previous 27. Source/type tables remain resident under their existing bounds; record transport adds no native judgments, source-module verification or whole-proof coverage. The general program remains active. Rules and native evidence · Reader scope and checks.

Compositional local-definition interfaces

For let x : A := v; b, the interface keeps the source declared type A, the value’s recorded type B, the context extension, the body’s recorded type C and the whole expression’s result type R distinct. A and B use the prior context; C uses the extended context. A shared formula display requires structural equality of A/B in the same context and preserves both formal ports. The context extension does not invent a source occurrence or a typing judgment for the introduced variable. A value’s proof/type/value role comes from its own record.

Two consecutive definitions compose at the exact original body occurrence, with matching context, role and recorded type syntax. The parent’s body type and the child’s conclusion type retain separate native origins even when they agree. The represented region is a disjoint source cut: n retained lets, 2n header regions and one remaining body. Overlapping whole-unit subtrees are not added. Continuation retains its exact original address; missing, incompatible and unsupported records remain explicit boundaries.

The candidate reader offers the same local-definition view in complete and paged modes. The paged implementation compares source and type expressions through resumable row reads and bounded caches, without a complete-archive fallback. Four definitions form the default chunk; eight is the maximum. The finite evidence covers60 corpus positions and34 owned native calibration positions. The latter include value-, type- and proof-valued definitions and mixed chains; ten cases distinguish the value role from the enclosing-expression role. These are calibration controls rather than complete Lean coverage or an independent AI benchmark.

This establishes finite source/context/type-origin correspondence for the implemented rule. General mixed proof units, introduced-variable witnesses, semantic abstraction and measured human proof-inspection benefits remain open.

Riccati definition chain · Rule and evidence scope.

Mixed introduction and definition interfaces

The optional Typed interfaces → Introductions + definitions view composes recorded assumptions and local definitions through their actual original body interfaces. An introduction keeps source domain A, the recorded type of A, actual body type C, expected expression D and result type R separate. Source lambda and computed Pi binders retain distinct identities and an explicit correspondence. The native C ≡ D conversion does not replace C at a structural join. Expected expressions do not acquire new typing judgments; codomain geometry is navigation inside the existing recorded R.

The same rule has complete and paged models, bounded chunks and exact source cuts. The finite inventory contains209recorded introductions and60recorded local definitions across26profiles; it is not complete Lean coverage. Seven actual/expected body types differ structurally. At two published crossing positions, the next recorded application’s actual result matches C but not D, so joining through D would change the implemented structural relation. Applications beyond the admitted context chain remain boundaries. Rechunking checks preserve original regions and separate native origins. General preservation, broader elimination coverage and measured human inspection benefits remain open.

Integrated reader and reproducible checks · Rule specification.

Recorded variable uses: reference rule

A separate reference model attaches existing typed variable observations to their exact original source uses and lexical binders. A use belongs to one original header/body region and links to a retained binder slot, an external original-context boundary, or an internal binder hidden in that same region. Such a reference contributes zero source occurrences. Its typing belongs to the use in its own context; it does not type the enclosing region or invent a new variable judgment. Sparse source/binder indexes retain separate native origins and bounded delivery pages.

Finite checks cover 340 observations at 170 distinct source uses across 51 profiles, including 36 uses whose binders lack a current typed-interface record. The reference links compose with 909 mixed frames without changing source accounting. A separate syntax counter completes 296 of 303 binder counts within its state limit; seven remain unavailable. In 229 completed cases the syntax contains more uses than the recorded typing inventory, so those coverage measures remain distinct. The candidate reader attaches these references to its existing mixed interfaces through a sparse index, with separate source and native-type selections. Public delivery covers 152 uses and 304 observations across 26 extraction profiles; missing records remain missing. This adds no native judgments or semantic-necessity claim. The general program remains active.

Rule, bounds and reproduction · Candidate reader and checks.

Syntax multiplicities under source-cut refinement

A source region has a sparse multiplicity vector over free term de Bruijn indices. Application fields add their vectors; binder bodies drop index zero and shift the other indices, while domains and let values keep the prior scope. Shared fields contribute with their expanded occurrence multiplicity. In a source cut, retained free variable occurrences plus scope-adjusted hidden-region vectors recover the root vector. This is a syntax annotation, separate from native typing and logical necessity.

The bounded reference method completed all 44,143 stored binders in the 2,098 library packets, with 36,358 small-body enumeration comparisons. All 303 selected construction counts agree with a separate scalar evaluator, including seven previous refusals. The finite refinement check covers 909 cuts and 4,929 hidden frontier terms. The new delivery includes twenty frozen publisher-attributed AI packets as well: 44,887 stored-binder rows across 2,118 packets. The candidate reader attaches these rows to original binder/body positions in the existing source and typed context views. It preserves raw source forall binders and keeps recorded typed-use coverage separate.

Count delivery retains one bounded page. Whole-source residency and the 35-profile source-paging inventory remain separate limits; other declarations use the complete source reader. Missing metadata stays unavailable. This adds no native judgments or semantic-necessity result. Candidate verification and public deployment remain distinct, and the general program stays active.

Rule and reference evidence · Candidate reader and scope

5. Evaluation

Evaluation on released AI-source proofs

A fourth, separately labelled library edition uses the official Goedel-LM release of scripts attributed by its publisher to Goedel-Prover-SFT. The pinned dataset revision is b731852af8d8ab11498fda27bce9020738c01c59; the publisher declares an MIT dataset license. The sample was selected before compilation: 16 records by a deterministic hash, plus the eight longest scripts. Length includes comments. This is a finite evaluation sample, not a population success-rate estimate or an independently observed generation run. Pinned release and attribution.

Twenty of 24 unchanged scripts compile under Lean 4.33.1 and the recorded Mathlib revision. Four report errors: two have unsolved goals, one has missing identifiers and one uses rejected sum syntax. The scripts are retained unchanged in private reproduction inputs; failures are not replaced with easier examples or attributed solely to version drift. Every successful source module’s owned declaration, type and complete body is exported. Native checks additionally force the body at its declared type through a kernel-checked typed identity.

The public projection has 20 complete theorem graphs, 268,356 stored nodes and 82,348,388 expression occurrences across their types and bodies. The largest proof has 91,424 stored nodes and 31,752,787 body occurrences; its initial grouped cut has 24 vertices, retaining 50 occurrences and hiding 31,752,737. The audit checks 120 initial type/body cuts and 744 cuts at source binders, with 500 independently resolved scope links. External Lean and Mathlib declarations remain named boundaries. The statements’ correspondence to their source comments’ mathematics is not certified.

A finite native type inventory records 175 exact queries, including 99 lambda introductions and 36 application traces with 146 argument stages. It follows outer bindings and let values, then adds the exact lambda inputs of three checked Or eliminations. Their six source frames remain navigable. A fourth candidate’s eta forwarding is unsupported and stays unavailable with its ordinary type judgment intact. Other internal paths have no invented typing record. Original source scripts and logs are not published.

Show binding references adds a source scope projection for a selected lambda, forall or let. It summarizes references from the collapsed body back to that binder, while its own domain/type and let value remain outside its scope. Every region keeps its exact source path and occurrence accounting. The projection uses a fixed number of visible regions and a bundled scope relation; it does not draw one vertex per reference or replace the underlying proof. A count is syntactic, includes type annotations and does not establish semantic necessity.

The corpus has 744 stored binders, including 48 lets. Independent native Expr counts and absence checks agree with all 744 browser counts; 33 let bodies have no reference to their bound variable. A compositional free-variable support table resolves twelve counts that exceeded the preceding traversal budget. The table uses at most 131,072 source entries with 512 variable slots each; reference traversal keeps its 65,536-state/depth-512 limits. Larger or unsupported support tables fall back to bounded counting, with unavailable rather than fabricated zero results. This establishes count coverage on the stated inputs, not general runtime improvement.

Fresh core-only controls check lexical boundaries, repeated names, dependent domains, nondep metadata, wide scopes and an exponentially shared proof. The compiled corpus remains a re-elaboration under the stated environment; original-environment equivalence, broader AI-proof coverage, semantic abstractions and measured human inspection benefits remain open. The general research goal stays active. The blog is unchanged.

AI-source corpus · Binding-use example · Data and native-count audit · Binding model · Reproduction and scope · Dataset license and attribution