From 32bf81f16be72be2f53c012ae9cc0690c7b17e50 Mon Sep 17 00:00:00 2001 From: Thorsten Fuchs Date: Sat, 23 May 2026 20:54:46 +0200 Subject: [PATCH 1/2] v5w2-w8b(release-lines-verify): Release Lines section on /verify/taulib/ + Formalization Release Lines table on /verify/release-manifest/ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Source: atlas/website/v5/panta-rhei-release-lines-formalization- surfaces-v5-addendum.md §7 (TauLib Release Lines) + §9.2 (Verify lane TauLib representation) + §9.3 (Release Manifest representation) + §8.4 (Proof Package States). Data: _data/release_lines.yml · formalization_release_lines + proof_package_states + citation_status enum (shipped W1). Roadmap: atlas/website/briefings/v5/v5-next-wave-roadmap-2026-05-23/ README.md (W8 · Release lines + TauLib v2/v3 + cross-links — PR 8b). Closes Wave 8 and the v5 next-wave cycle. ══ What lands ════════════════════════════════════════════════════════ verify/taulib/index.md (+35 / 0) ──────────────────────────────── New "## Release Lines" section inserted between "TauLib inside the verification matrix" and "What Verify still owns". Three-tile grid framed as the inspection-bridge view (parallels W8a's Corpus-side framing but from the trust-boundary angle): TauLib v2 Snapshot — Citable as a proof basis. Reproduction instructions clear (clone pinned commit, re-run lake build). TauLib v3 Library — Active restructure · not yet citable. Current Results cite v2. Proof Packages — Per-result · 5-state lifecycle. Released packages are citable per result. Closing block re-states the IA §9.2 core warning verbatim: Lean compilation checks formal obligations; it does not establish empirical truth, bridge adequacy, or external scientific acceptance. Cross-links to /verify/verification-framework/ + /verify/how-to-verify/ for the broader inspection questions. Doctrine comment block above the section pins both §7 + §9.2. verify/release-manifest.md (+36 / 0) ──────────────────────────────────── New "## Formalization Release Lines" section inserted between "Release identity" and "Build status — summary". Canonical four- row table per Addendum §9.3: | Surface | Corpus Relation | Status | Public | Citable | |----------------------|-----------------------------------|-------------------|---------|------------| | TauLib v2 snapshot | Corpus v2 / Second-Edition comp. | frozen | ✓ | ✓ | | TauLib v3 library | Corpus v3 working line | active restructure | not yet | no | | Proof packages | per-result | per package | varies | per package| | Citation status enum | cross-cutting | enum: 4 values | ✓ | per artifact | Two explanatory paragraphs below the table: · Proof package states — five-state lifecycle (in_construction → draft → candidate → released → superseded), only released is citable. · Citation status enum — four values per Addendum §3 vocabulary (citable · active_working · private · deprecated), surfaced on every Research Graph entry. Anchor: — used by deep- links from the Corpus + Verify TauLib pages and by W8a's Research Modules / Proof Packages tile. Cross-links to Research Graph §rg-software (W6a) where the same data appears as graph entities, and to the right-rail identifier boxes (W6b) which render the relevant table row inline on every TauLib + proof-package page. ══ Three-surface model now fully realised for formalization ═════════ Per IA §10.3, the program's authority/provenance layer is exposed through three surfaces. Wave 8 closes the formalization slice of this model: Surface 1 (machine-readable JSON-LD): Already shipping per-page (W6a Schema.org per page-type) + the JSON projection at /assets/research-graph.json (W6a). Surface 2 (human-visible identifiers): Identifier boxes on every TauLib entity page (W6b — auto- match against the research-graph manifest). Surface 3 (authoritative page): This PR — /verify/release-manifest/#formalization-release- lines is now the authoritative table for the formalization release-line picture; the Corpus + Verify TauLib pages (W8a + W8b) link here. ══ URL preservation posture ═════════════════════════════════════════ Purely additive — no existing URL changes, no existing content removed or hidden on either page. Build status / Per-book reconciliation / Reproduction instructions / Next release targets on the Release Manifest all preserved; What Verify still owns / Inspection routes on /verify/taulib/ all preserved. ══ Gates run locally ════════════════════════════════════════════════ ✓ scripts/check_hardcoded_release_numbers.py ✓ scripts/check_release_manifest_parity.py ✓ Forbidden-strings pre-commit hook · Jekyll build deferred to CI (local Ruby mismatch) ══ Cycle close ══════════════════════════════════════════════════════ Wave 8b closes the v5 next-wave cycle. Eight waves · 12 PRs · shipped over a single working session. All three v5 doctrine documents (IA Doctrine v5, Publication Taxonomy v5 Supplement, Release Lines + Formalization Surfaces v5 Addendum) are now realised on the public site. Co-Authored-By: Claude Opus 4.7 (1M context) --- verify/release-manifest.md | 36 ++++++++++++++++++++++++++++++++++++ verify/taulib/index.md | 35 +++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+) diff --git a/verify/release-manifest.md b/verify/release-manifest.md index a613874c3..bf948093e 100644 --- a/verify/release-manifest.md +++ b/verify/release-manifest.md @@ -48,6 +48,42 @@ The Release Manifest records the release state, trusted base, custom axioms, fil The TauLib browser under `/verify/taulib/docs/` is generated from the Corpus-native TauLib projection pinned to commit `{{ build.taulib.commit_short }}`. 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](../../atlas/website/v5/panta-rhei-ia-doctrine-v5.md), the same data is exposed as right-rail identifier boxes on each TauLib entity page (Wave 6b) and as graph entities at [Research Graph]({{ '/research-graph/' | relative_url }}#rg-software). + + + +| Formalization Surface | Corpus Relation | Status | Public? | Citable? | +|---|---|:-:|:-:|:-:| +| **TauLib v2 snapshot** | Corpus v2 / Second-Edition companion | frozen | ✓ | ✓ | +| **TauLib v3 library** | Corpus v3 working line | active restructure | not yet | no | +| **Proof packages** | per-result | per package | varies | per package | +| **Citation status enum** | cross-cutting | enum: `citable · active_working · private · deprecated` | ✓ | per artifact | + +**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]({{ '/research-graph/' | relative_url }}#rg-software) 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 | Metric | Value | diff --git a/verify/taulib/index.md b/verify/taulib/index.md index f72cda715..dc57a6d07 100644 --- a/verify/taulib/index.md +++ b/verify/taulib/index.md @@ -50,6 +50,41 @@ The current projection contains **{{ summary.module_count }} modules** and **{{ TauLib is one formalization surface inside the broader verification matrix. Lean compilation checks formalized obligations; it does not by itself establish empirical truth. +## Release Lines + + + +TauLib is published through two release lines plus a per-result proof-package layer. From an inspection standpoint, each line is a distinct trust-boundary surface: + + + +> **Trust boundary.** Lean compilation checks encoded formal obligations. It does not by itself establish empirical truth, bridge adequacy, or external scientific acceptance. The release-line distinction above is about formalization status; the [Verification Framework]({{ '/verify/verification-framework/' | relative_url }}) and [How to Verify]({{ '/verify/how-to-verify/' | relative_url }}) cover the broader inspection questions. + ## What Verify still owns Verify does not stop at “the Lean code compiles.” It asks the higher-level inspection questions: From 4d6c710f75cc5100fff32dd57ee62ba1a17f7ded Mon Sep 17 00:00:00 2001 From: Thorsten Fuchs Date: Sat, 23 May 2026 20:58:26 +0200 Subject: [PATCH 2/2] v5w2-w8b(release-lines-verify): regenerate release-manifest section baseline for new Formalization Release Lines MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #270 verify gate failed: registry_verify --full ❌ 1 error(s): • RELEASE MANIFEST NEW UNBASELINED SECTION: 'Formalization Release Lines' scripts/registry_verify.py:117 enforces that every section heading in verify/release-manifest.md appears in the saved baseline at _data/registry/release_manifest_sections.yml. The baseline is auto- extracted by registry_preserve_prose.py and stores section text + SHA-256 checksums to catch stale or accidentally edited prose. The new "Formalization Release Lines" section shipped in the parent W8b commit (32bf81f16) is doctrine-prescribed (Release Lines + Forma- lization Surfaces v5 Addendum §9.3) — the baseline needs to learn about it, not the section to be reverted. Ran: python3 scripts/registry_preserve_prose.py The script re-extracted all 11 sections (was 10) of the release manifest including the new "Formalization Release Lines" section, recomputed all SHA-256 checksums, and rewrote the baseline file. Co-Authored-By: Claude Opus 4.7 (1M context) --- _data/registry/release_manifest_sections.yml | 38 ++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/_data/registry/release_manifest_sections.yml b/_data/registry/release_manifest_sections.yml index a255a4ee0..c3aeefaa2 100644 --- a/_data/registry/release_manifest_sections.yml +++ b/_data/registry/release_manifest_sections.yml @@ -58,6 +58,43 @@ sections: The TauLib browser under `/verify/taulib/docs/` is generated from the Corpus-native TauLib projection pinned to commit `{{ build.taulib.commit_short }}`. 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': | + ## Formalization Release Lines + + + + This table is the program's authoritative surface for the formalization release-line picture. Per [IA Doctrine §10.3 surface 2](../../atlas/website/v5/panta-rhei-ia-doctrine-v5.md), the same data is exposed as right-rail identifier boxes on each TauLib entity page (Wave 6b) and as graph entities at [Research Graph]({{ '/research-graph/' | relative_url }}#rg-software). + + + + | Formalization Surface | Corpus Relation | Status | Public? | Citable? | + |---|---|:-:|:-:|:-:| + | **TauLib v2 snapshot** | Corpus v2 / Second-Edition companion | frozen | ✓ | ✓ | + | **TauLib v3 library** | Corpus v3 working line | active restructure | not yet | no | + | **Proof packages** | per-result | per package | varies | per package | + | **Citation status enum** | cross-cutting | enum: `citable · active_working · private · deprecated` | ✓ | per artifact | + + **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]({{ '/research-graph/' | relative_url }}#rg-software) 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': | ## Build status — summary @@ -164,6 +201,7 @@ sha256_checksums: '__preamble__': '077bd63d09631831' 'Release state and trusted base': '5645da445738eed8' 'Release identity': 'ed67f7af74c0b89a' + 'Formalization Release Lines': '27559b87769ebcb3' 'Build status — summary': '09d9861eac53e827' 'Per-book reconciliation': '27daae2d0b703370' 'How to read apparent "drift"': '8aa7ff8b50e9bef3'