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

```lean
(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

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