Filter Rules — Which Count Means What

A reader looking at three surfaces — the Registry, the per-book Dashboards, and the TauLib Status — may see three different numbers for the same book. Book VI, for example, appears as 217, 168, and 30 across these three places.

This is not a data-integrity bug. It is three different filter rules applied to the same canonical source. This page names each rule, specifies what it includes, and pins down the current counts so a reader can always reconcile.

Canonical source of truth. All counts derive from the canonical registry JSONL source, book{1..7}_registry.jsonl — one JSONL line per registry object. Every number on this site descends from that source via one of the filter rules below.

The five filter rules

Rule	What it counts	Book VI example
registry_total	All objects regardless of type or status — axioms, constructions, corollaries, definitions, lemmas, propositions, remarks, theorems	217
dashboard_display	Only the five display types (D + L + P + R + T) — the types per-book dashboards enumerate	168
formalized_count	dashboard_display restricted to formalization_status == formalized	0
planned_count	dashboard_display restricted to formalization_status == planned	143
taulib_modules	Lean 4 module count — different unit from registry objects (one module hosts many objects)	31

Why two registry filters, not one? A dashboard that rendered every remark, axiom, and corollary would be 2× longer and harder to scan. A registry root that silently dropped “ancillary” object types would lose claim-ID stability across releases. The two rules — one complete, one display-filtered — give both clarity and completeness. The column-mapping in the Release Manifest makes the choice explicit at every surface.

Why taulib_modules sits apart. Lean modules and registry objects are different units. A single Lean module can host dozens of registry objects (definitions, theorems, propositions side by side). The module count (512 total) and the object count (4,547 total) are both correct for their respective units; they are not comparable quantities.

Current totals — per book

Counts sourced from canonical book{1..7}_registry.jsonl (2026-04-18) and the pinned TauLib commit.	Book	registry_total	dashboard_display	formalized_count	planned_count	not_applicable_count	taulib_modules
	I — Foundations	254	254	221	7	26	147
	II — Holomorphy	230	219	184	2	33	66
	III — Spectrum	289	289	231	0	58	71
	IV — Microcosm	1864	1292	973	41	278	90
	V — Macrocosm	1419	1253	884	66	303	81
	VI — Life	217	168	0	143	25	31
	VII — Metaphysics	274	273	182	0	91	9
	Meta / Tour / root modules	—	—	—	—	—	17
	Total	4547	—	2675	259	814	512

Rule definitions — in detail

registry_total

What it counts. The count of every registry object regardless of type or status — axioms, constructions, corollaries, definitions, lemmas, propositions, remarks, and theorems, including deprecated entries. This is the authoritative JSONL line count per book.

• Includes types: ALL types (A, C, Cor, D, L, P, R, T, Con, …)
• Includes statuses: ALL statuses (formalized, planned, not_applicable, deprecated)
• Grand total: 4547 objects

Displayed on:

• registry/index.md (line 33)
• registry/books/book-{i..vii}.md (frontmatter: object_count)
• verify/release-manifest.md (per-book reconciliation table, 'Registry root' column)
• verify/filter-rules.md (authoritative public manifest)

dashboard_display

What it counts. The count filtered to the five display types that the per-book dashboards render: definition, lemma, proposition, remark, theorem. This is a DISPLAY filter, not a count correction — it omits axioms, constructions, and corollaries because those object types receive dedicated treatment elsewhere in the book narrative rather than dashboard-style enumeration. The filter is content-driven, not omission-driven.

• Includes types: D + L + P + R + T (definition, lemma, proposition, remark, theorem)
• Includes statuses: ALL statuses except ‘deprecated’

Displayed on:

• registry/dashboards/book-{i..vii}.md ('Total objects' line in Statistics section)
• registry/dashboards/book-{i..vii}.md (filter-rule attribution banner, via _layouts/registry-dashboard.html)
• verify/release-manifest.md (per-book reconciliation table, 'Dashboard total' column)
• verify/filter-rules.md (authoritative public manifest)

taulib_modules

What it counts. The count of Lean 4 source modules per book in the TauLib repository at the pinned commit. This is a DIFFERENT UNIT from registry_total or dashboard_display — one Lean module hosts many registry objects (typically 5-50). Do not compare taulib_modules to registry counts as if they were the same quantity.

• Unit: Lean 4 modules
• Source: pinned TauLib commit cb5e830 (Apr 29 2026)
• Grand total: 512 Lean 4 modules

Displayed on:

• verify/taulib/status.md (Per-Book Breakdown)
• verify/release-manifest.md (per-book reconciliation table, 'TauLib modules' column)
• verify/filter-rules.md (authoritative public manifest)
• _data/verify/build.yml (indirect, via description field)

formalized_count

What it counts. The count of registry objects with formalization_status == ‘formalized’ in the canonical JSONL. These are objects that have a corresponding Lean theorem or definition in TauLib with a stable identifier and the docstring links back to the registry ID.

• Includes types: D + L + P + R + T (following dashboard_display convention)
• Grand total: 2675 formalized objects

Displayed on:

• registry/dashboards/book-{i..vii}.md (Statistics: Formalization line)
• verify/release-manifest.md (per-book reconciliation table, 'Formalized' column)
• verify/filter-rules.md (authoritative public manifest)

planned_count

What it counts. The count of registry objects tagged formalization_status == ‘planned’: a Lean theorem is expected but not yet written. This is the forward formalization backlog.

• Grand total: 259 planned objects

not_applicable_count

What it counts. The count of registry objects tagged formalization_status == ‘not_applicable’: prose-level entries (remarks, conjectures) that are not intended to have a Lean formalization. These are intentionally outside the Lean corpus.

• Grand total: 814 not-applicable objects

Cross-surface invariants

Every count on this site must satisfy these invariants, which scripts/registry_verify.py checks on every CI run:

• registry_total ≥ dashboard_display for every book (filter is subsumptive)
• formalized_count + planned_count + not_applicable_count ≤ dashboard_display for every book
• SUM(registry_total per book) = grand_total = 4547
• SUM(taulib_modules per book + meta_tour_root_modules) = 512 total
• TauLib module count and registry object count use DIFFERENT UNITS and are not directly comparable

A violation of any invariant is a merge blocker on main. See scripts/registry_verify.py for the implementation.

Reconciliation protocol

If a reader sees two different numbers for the same book on different pages: (1) identify which filter_rule each surface applies (visible in this manifest); (2) confirm the numbers are consistent with that filter rule’s current_totals section here; (3) if they are, the apparent drift is a legitimate difference between filters, not a bug. If a number on a page does NOT match the current_totals in this manifest, that IS a bug — file it and the registry_verify.py harness will catch the regression.

Update protocol

This manifest is CANONICAL for per-book counts as displayed on the site. After any change to the canonical registry JSONL source (book*_registry.jsonl), run scripts/registry_verify.py to detect divergence between this manifest and the site data files; update current_totals here to match the new canonical counts; then regenerate the Release Manifest table.

What this page is NOT

• Not a dashboard. For per-book enumerations, see the dashboards.
• Not a registry browser. For navigation to individual objects, see the registry index.
• Not a TauLib map. For Lean module architecture, see Formalization Status and Architecture.

This page’s single job is to make the filter rules legible and to let a reader reconcile any two count claims on the site without leaving the public surface.