Reading expressions and checking outcomes

Four kinds of information

A claim about one layer is not automatically a claim about all four. In particular, kernel acceptance does not certify the rendered diagram or establish that its explanation is useful to a reader.

Context and identity

Names in scope describes lexical availability. A context can contain user parameters, local definitions, recorded auxiliary declarations, and binders entered during inspection. These have different roles. Listing an entry does not assert that the selected term uses it.

Names alone do not establish identity. Read the context position, the expression's constructor path, and the relation through which it was reached. Two objects with the same displayed name need not be the same object. Fields and laws belong to their recorded owner and remain available within that owner's scope.

Relations between expressions

One physical check can serve more than one role. Counting it twice does not provide independent confirmation. Occurrence, relation, step, and outcome numbers refer to different things.

Attempts, prefixes, and navigation

An attempt records a bounded sequence of requested inspections and their outcomes. Step reading, Ordered provenance, and Supply reading describe the selected step or the prefix through it. Attempt outcomes retains the whole attempt, including checks outside that prefix.

Section navigation and its return links move reading focus within the displayed attempt and step. They do not change the selected attempt, open disclosures, or run Lean. Explicit inspection actions make fresh captures; selecting retained data or changing its presentation does not.

Inspect type makes the inferred type the next term. Read logical structure of this term (one layer) inspects the displayed term. To inspect the logical structure of its inferred type, inspect the type first. Operations are bounded and can be refused or unavailable; those states must remain visible.

A law belongs to its owner

structure Rotor where
  Carrier : Type
  turn : Carrier → Carrier
  fixed : ∀ x, turn x = x
example (owner : Rotor) (unused : Nat) : Rotor := owner

The example takes owner : Rotor as a parameter. Its fixed field already supplies a law about that owner's turn. The example does not construct a Rotor or independently establish its law.

The inspection route catalogues the fields, projects fixed, inspects its type, reads the universal layer, and enters its body. A field catalogue by itself is not a typing check. Inspecting the equality inside the law does not produce a separately specialized proof of that equality.

Keep the full context, including unused, when reading the conditions. The presence of unused does not assert that the proof depends on it. Recorded auxiliary entries also retain their own kind.

The initial guided view of the selected structure value can refuse to produce a reading. The retained source and checked occurrence route is distinct from that guided response. The source's unused-variable warning is a diagnostic, not a rejected kernel outcome.

Recorded data and live editor context

Saved records have an unverified origin. Recorded outcomes do not establish that a file describes the current buffer, engine, or imported environment. Format validation and internal consistency are not authentication of the recorded computation.

The accepted application has separate import routes for composition packets and raw source frames. Neither is a saved editor-history importer. This revision can serialize editor snapshots but has no accepted saved editor-snapshot loader. The static lessons do not supply one or offer live checking of visitor input.

In live editor use, changes to the buffer or selection invalidate the attachment. The editor sidecar elaborates the whole trusted buffer, including commands outside the selected range, against existing built dependencies. Lean commands and elaborators can execute code. A separate process and resource bounds do not make that execution a security sandbox.

Setup and support

Local use currently requires manual source setup. A matching public distribution with qualified installation, upgrade, rollback, and uninstall paths is not yet established. Do not assume that a public clone or a controller package alone reproduces the revision described here.

Use the source guides for the matching checkout. Their install commands use npm ci --ignore-scripts; explicit build, native setup, and packaging commands still execute code. Configure the matching built checkout through the absolute statementLens.engineDirectory path in VS Code User settings. The retained statementLens.* identifiers are compatibility names.

The public lessons can be read without any of this setup. For local assembly, the accepted setup guide excerpt preserves the command sequence and qualifications; the reader contract gives the detailed reading and navigation boundaries.

Generality and formal foundations

The formal foundations already include general structural and exact printable readback results for specified representations of Lean expressions and local source records. A readback result states what can be recovered by decoding an encoding. Two examples in the foundation dependency retained by this revision are:

• ExprReferenceGraph.roundTrip_eq: decoding the reference-graph encoding of a Lean expression recovers that expression after eraseMetadata. This is an explicit normalization boundary; the theorem does not assert preservation of expression metadata or original source text.
• FoundationIntegration.encodeView_readback: when encoding into the scoped view succeeds, decoding recovers the expression after the same metadata erasure. Its coverage result applies under the declared admission conditions.

The recorded axiom dependency of each of these two readback theorems is propext, Lean's propositional extensionality axiom. These are formal results about the named representations and decoders. Separately, browser structural views implement independent reconstruction checks for their supported inputs. Neither fact establishes a Lean proof about the complete browser renderer, authenticates an imported record, or proves a proposition merely because it can be represented.

The goal remains a formally proved general visualization method for any valid Lean mathematical statement. The current application provides bounded structural inspection and selected guided readings; a universal guarantee connecting valid inputs to the rendered interactive view remains unproved. Extending the foundations across the complete application, including its context and scope handling, semantic readings, and renderer, remains open work. Interpreting unfamiliar mathematics, selecting useful abstractions, and demonstrating improvements in human understanding are further research questions.

Supported structures and bounded explicit operations can still be useful now. Judge each reading by the particular expression, context, transformation, evidence, and limitation it preserves.