Release Manifest

This page is the single authoritative snapshot of the current release. Everything that is pinned, every count that is claimed, every known drift between surfaces is stated here in one view. If the registry, the per-book dashboards, and the TauLib docs appear to disagree on a number, this page explains why and which number is load-bearing for which purpose.

Release state and trusted base

↓ Download print master · 1536 × 864 JPG · CC BY 4.0

The Release Manifest records the release state, trusted base, custom axioms, filters, and formalization boundaries. It tells a reviewer exactly which formal surface is being inspected.

Release identity

The TauLib browser under /verify/taulib/docs/ is generated from the Corpus-native TauLib projection pinned to commit cb5e830. To reproduce locally, import the TauLib snapshot into corpus/taulib-sources/project, run lake build, then run the Corpus TauLib projection/export scripts and the site sync.

Formalization Release Lines

This table is the program’s authoritative surface for the formalization release-line picture. Per IA Doctrine §10.3 surface 2, the same data is exposed as right-rail identifier boxes on each TauLib entity page (Wave 6b) and as graph entities at Research Graph.

Proof package states. Each proof package moves through a five-state lifecycle: in_construction → draft → candidate → released → superseded. Released packages are citable as a per-result proof basis; non-released states should not be cited as proof. The state of each package is recorded against the package’s entry in _data/release_lines.yml::proof_package_states.

Citation status enum. Every TauLib-side entity in the Research Graph carries a citation_status field with one of four values: citable (released, immutable), active_working (in development, not citable), private (not yet public), or deprecated (superseded by a newer artifact). The Corpus-side TauLib release line shown above maps to citable; the v3 working library maps to active_working.

The right-rail identifier box on each TauLib + proof-package page renders the relevant row of this table inline, so a reader inspecting a specific module or package can see its release-line status without leaving the page.

Build status — summary

The 3 custom axioms sit outside Mathlib’s trusted base and are specific to the τ-framework’s internal construction; they are named and documented in the per-module TauLib browser. The prior v1 release pinned at commit 181a59e shipped a fourth axiom central_theorem_physical : True in Book IV which was retired in peer-review-fixes-v1 (2026-04-19) as a no-op — an axiom of type True is inhabited by trivial and added nothing to the theory.

Pre-peer-review-fixes-v1, Book VII shipped three theorem X : True := sorry declarations encoding methodological commitments. These were identified as performative (True is provable by trivial) and were retired in favor of inspectable def : Commitment values carrying statement/warrant/registry_id string data. TauLib now contains 0 sorry across all seven books. See TauLib/BookVII/Meta/Commitment.lean and the three commitment defs in BookVII/Logos/Sector.lean and BookVII/Final/Boundary.lean.

Per-book reconciliation

This is the table Assessment #3 asked for. It shows, for each book, what each of the three public surfaces claims — and where they differ. Registry objects and Lean modules are different units of counting (a single module hosts many definitions, theorems, and propositions, each of which is a registry object), so some spread is expected; the drift within the same unit (registry root vs per-book dashboard) is what the honest reader should track.

Each column applies a specific filter rule to the same canonical source. The filter rules are documented on the Filter Rules manifest and summarized here:

Sources: counts sourced from the canonical registry JSONL source, book{1..7}_registry.jsonl, and the pinned TauLib commit cb5e830. Filter-rule definitions, per-book current totals, and cross-surface invariants are on the Filter Rules manifest.

How to read apparent “drift”

The Registry root and Dashboard total columns disagree for four of seven books (II +11, IV +572, V +166, VI +49). This is not a data-integrity bug — it is two different filter rules applied to the same authoritative source:

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 on the Filter Rules manifest), (2) confirm both numbers match the current_totals table on that page. If they do, the apparent drift is the legitimate difference between two filters of the same canonical data. If either surface does NOT match the manifest, that IS a bug — registry_verify.py catches such regressions.

Why this is acceptable: a dashboard rendering every remark and axiom would be 2x longer and harder to scan. A registry that silently dropped “ancillary” object types would lose claim-ID stability. Two filter rules, documented explicitly and cross-checked, give both clarity and completeness.

A follow-up sprint to consolidate the generation pipeline end-to-end (one script, idempotent, with the prose-preservation safeguards already scaffolded) remains on the engineering backlog — but is no longer load-bearing for the drift narrative.

What this release does NOT claim

• Book VII is formalized at methodological depth. The Lean corpus for Book VII contains 7 modules that include three def : Commitment values carrying structural-commitment data (statement, warrant, registry_id). Zero sorry. The Book VII formalization is scaffolded; the monograph’s prose content is the primary substance.
• The physics bridge is not proof-assistant-verified. TauLib verifies the internal τ-framework mathematics; it does not verify that τ-internal statements correspond to the external physics they are interpreted as describing. The 67 predictions surfaced in Predictions Browse and documented in the Numerical Prediction Supplement are derived from the framework’s algebraic structure; their agreement with experiment is empirical, not machine-checked.
• Millennium resolutions are not Clay-valid formulations. Only the Poincaré conjecture aligns with the Clay statement as solved (via Perelman’s proof, re-read in τ-language). The other six Millennium claims are τ-internal formulations with explicit bridge-conjecture gaps; see the Millennium & Langlands briefing.

Reproduction instructions

# Clone at the pinned commit
git clone https://github.com/Panta-Rhei-Research/taulib
cd taulib
git checkout cb5e83015b54dd72eba560953fe2461820078757

# Expected pins (already in lake-manifest.json / lean-toolchain)
# Lean: v4.28.0-rc1
# Mathlib: 85028a6

lake build          # Expect: 0 errors, ~8–12 min on 8-core laptop
rg "sorry" TauLib   # Expect: 0 matches across all 7 books

Continuous integration runs on every push and pull request and reports file count, line count, sorry count, and axiom count to the CI log. A failed build or a regression in sorry count is a merge blocker on main.

Next release targets

• Drift consolidation — one source-of-truth for registry totals across all surfaces.
• Book VI formalization uplift — currently 0 of 168 dashboard objects formalized; Book VI ch22 (Three Domains) and ch31 (Ecosystems) have solid internal theorem structure and are the priority targets.
• Book VII methodological sorry replacement with commitment tags — DONE (landed in peer-review-fixes-v1, 2026-04-19). The three theorem X : True := sorry declarations were replaced with inspectable def : Commitment values in TauLib/BookVII/Meta/Commitment.lean.