Candidate syntax-count annotations

The existing occurrence reader can show Syntax use counts in source cuts and in typed introduction/local-definition interfaces. The layer is optional; counts=syntax retains that presentation choice in the occurrence URL. It adds one annotation to each retained source binder. There is no additional proof viewer or article-specific diagram.

The label reports expanded syntactic occurrences of the binder in its original body. A forallE is still a source type binder, not a proof introduction. The annotation keeps the packet hash, original binder route, original body field, algorithm identifier, implementation hash and resource units. Count provenance exposes those fields. The graph scene, source partition, binding links and recorded native judgments remain unchanged. The annotation contributes zero source occurrences.

Recorded typed-use counts stay separate. While the new layer is enabled, the existing variable-use panel shows its recorded count beside the new syntax annotation. Turning the layer off restores its previous scalar count display, including that method’s seven unavailable counts. The two methods do not reuse the same state/resource field. A failed or missing new count is marked unavailable; it is never zero and does not assign a type.

Coverage and data

build-proof-atlas-syntax-counts.cjs reads the public compiled indexes only. Its current delivery has 44,887 stored-binder rows across 2,118 library/AI packets: the existing 2,098 library packets and twenty publisher-attributed AI packets. There are no unavailable rows in this frozen delivery. Owned calibration profiles remain reference tests and are not added to this public catalogue. This counts binder syntax; it is not complete Lean surface/tactic coverage.

The metadata are available for both source loading modes. Source paging is a separate, inherited boundary: the existing source-page inventory has 35 profiles. Other declarations use the complete source reader. The count layer does not silently load a complete source archive when paged source is missing. A complete reader keeps its source packet resident under its existing bounds; a count query itself loads only count metadata. Missing native type profiles do not prevent source-syntax annotations.

Each count manifest is at most 64 KiB and names at most 256 ordered pages. A page has at most 128 rows and 64 KiB; one numeric count has at most 16,384 digits. The producer refuses oversized rows/manifests instead of truncating counts. The consumer keeps one page, serializes reads and accepts at most 64 pending requests. Disposal releases its cache and refuses pending work. A page is bound to the compiled index hash and verified against its expected decoded size/hash before use. A selected source point must match the original constructor and body node/port. Counts cannot exceed the body’s expanded occurrence count. Inputs needed after an asynchronous read are copied first.

The global catalogue is separately resident (1,004,633 bytes in this snapshot). All 4,232 immutable compressed assets total 2,021,044 bytes; they are not loaded together by the reader. The observed largest resident count page was 9,717 bytes. These are count-transport units, not total browser or source-table RAM. The coefficient-table limits in the manifest describe the offline computation, including its scratch vector and retained outputs. They are not scalar states.

The publisher retains existing compressed bytes and authenticates canonical decoded metadata, avoiding dependence on a platform’s gzip encoding. Existing source/type/variable-use archives are unchanged. The package contains no original private mathematical source or raw private verification log.

Checks

node scripts/build-proof-atlas-syntax-counts.cjs
node scripts/test-proof-atlas-syntax-counts.cjs
node scripts/test-proof-atlas-syntax-count-coverage.cjs

The consumer audit compares every delivered row against the separately checked multiplicity engine, attaches all 44,887 rows to actual original binder routes and verifies unchanged source scenes. It also checks source/body/hash/method and resource refusals, the pending-request bound, input mutation and disposal. A separate bridge checks the sparse native-use catalogue against these syntax counts: 152 source uses, 304 observations and 113 original binder routes. In 103 of those routes the syntactic count exceeds the recorded-use count. The cached Linux Node 22 runtime passes the publisher and consumer checks.

After the normal production site build, run node scripts/test-proof-atlas-syntax-counts-browser.cjs with the existing ATLAS_ORIGIN and Playwright/axe environment. Its complete scope includes all 269 public mixed-frame starts, original route/body/count comparisons, source and dedicated definition views, source forall binders, a declaration without a native type profile, all seven prior scalar refusals, the unsupported paged boundary, sharing changes, recorded-use compatibility, accessibility and failure/retirement controls. The optional ATLAS_SYNTAX_COUNTS_FOCUSED=1 run has fullCorpus: false and is not a substitute for that corpus audit. Inspect the emitted report to establish a pass.

Source sharing and compression, general kernel correctness, semantic necessity and measured proof comprehension are separate questions. This is a candidate integration; public deployment requires its own merge, Pages and hosted-interaction checks. The general research goal remains active, and the blog is unchanged.