Hidden regions and proof-premise coverage

Hidden regions and proof-premise coverage

A closed proof-premise frontier does not mean that every proof-valued subterm has been inspected. Boundary roles describe roots. A value or type region can contain proofs below that root, and terminal declaration references remain opaque.

Native counterexample

The existing assistant-authored ProjectionControls.lean fixture constructs an Expr.proj of the proof field in a dependent structure. A compact display is:

(Pack.mk Nat s (Eq.refl s)).proof

Here s is generated by eighty shared Nat.add doublings of an enclosing n. This display explains the constructed expression; it does not reconstruct tactic history. The projection is proof-valued; its structure operand is value-valued; the operand contains a proof-valued application Eq.refl s.

With only the projection as a seed, the proof-premise policy examines zero proof premises and produces an empty frontier. Adding the structure operand as a seed reveals the proof application at route 1:1.0.1. An independent native query checks that application in the same one-binder context, and its type matches the earlier parent-premise observation structurally.

The source packet has 177 stored nodes and the selected projection has 9,671,406,556,917,033,397,649,412 expanded occurrences. At a one-vertex cut, the retained projection contributes one and the value boundary contributes 9,671,406,556,917,033,397,649,411. No expanded tree is materialized.

This is a counterexample to treating an empty proof-premise frontier as coverage of every proof-valued subterm. It does not establish that the omitted reflexivity proof is mathematically important, or that every type/value boundary contains a proof. Both fresh native reproductions agree on source graphs, contextual judgments and the witness query. Environment and request digests are retained separately; raw logs and original private mathematical scripts are not published.

Boundary rule

The reader’s Hidden source regions disclosure accounts for the complement of the displayed source cut. Each row retains an exact occurrence route, source-root count and, where recorded, its native root role and type reference. Source children of an opaque unrecorded root are split along literal kernel fields and remain untyped. Stored-node sharing does not identify different occurrence routes.

The rows form a source antichain. Their counts sum to the hidden source count; adding the retained constructors recovers the selected source count. These are source occurrences, not numbers of proof steps. Type/value boundaries remain accessible. The list does not infer roles for their descendants or supply missing construction judgments.

The disclosure is prepared on demand, limited to 4,096 boundary roots and shown sixteen at a time (API pages at most 32). It traverses the finite scene and root paths, not hidden subtrees. Source paths retain their existing 512-slot bound. An exceeded bound withholds this disclosure and preserves the diagram. Paged source access uses the existing source cache; late preparation cannot restore an older source selection. No total-browser memory or comprehension result follows.

The finite source audit covers 612 initial cuts across 34 proof inventories and 150 cuts at the fifty current replay-query roots: 9,177 boundary appearances. Independent checks resolve source routes, root roles, counts and non-overlap; twenty changed-data or bound controls reject. A separate source-only syntactic stress fixture checks a 212-digit occurrence count without claiming a typed proof. The native counterexample also checks that unrecorded descendants acquire no type roles.

Reproduction

python3 research/proof-atlas/frontier-boundary/verify.py \
  --lean /absolute/path/to/lean-4.33.1/bin/lean \
  --workdir /absolute/path/to/new-private-workdir
node research/proof-atlas/frontier-boundary/publish.cjs /absolute/path/to/new-private-workdir
node scripts/test-proof-atlas-boundary-control.cjs
node scripts/test-proof-atlas-boundary-ledger.cjs
node scripts/test-proof-atlas-boundary-ledger-browser.cjs

Only core Lean and the existing own fixture are compiled. Native invocations keep the 120-second, 8-GiB RSS, 64-MiB output and 30-GiB local free-space bounds. The published complete control artifacts retain the existing 16-MiB evidence cap; each individual query is checked against the existing 2-MiB limit. The four-query package contains 2.36 MB of serialized evidence, mostly generated presentation text, while its shared type table occupies about 7.4 kB. The UI list does not render that large generated text.

The public control packet uses the extractor’s minimal structural-packet format; it is validated as a closed expression DAG and contextual evidence, rather than claiming the additional ownership metadata of a full library edition.