v5w2-w8b(release-lines-verify): Release Lines on /verify/taulib/ + Formalization Release Lines table on /verify/release-manifest/

_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
+
+    <!--
+      v5 next-wave W8b · IA Doctrine v5 §9.3 + Release Lines Addendum §7.
+      Source: atlas/website/v5/panta-rhei-release-lines-formalization-
+              surfaces-v5-addendum.md §7 (TauLib Release Lines) + §9.3
+              (Release Manifest representation).
+      Data:   _data/release_lines.yml · formalization_release_lines
+              + proof_package_states + citation_status enum.
+
+      Canonical four-row table per Addendum §9.3. This is the
+      authoritative surface for the formalization release-line picture
+      across the program — Corpus-side at /corpus/taulib/ (W8a) and
+      Verify-side at /verify/taulib/ (W8b) both link here.
+
+      Anchor id: formalization-release-lines (used by deep-links from
+      the Corpus + Verify TauLib pages).
+    -->
+
+    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).
+
+    <a id="formalization-release-lines"></a>
+
+    | 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'

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
+
+<!--
+  v5 next-wave W8b · IA Doctrine v5 §9.3 + Release Lines Addendum §7.
+  Source: atlas/website/v5/panta-rhei-release-lines-formalization-
+          surfaces-v5-addendum.md §7 (TauLib Release Lines) + §9.3
+          (Release Manifest representation).
+  Data:   _data/release_lines.yml · formalization_release_lines
+          + proof_package_states + citation_status enum.
+
+  Canonical four-row table per Addendum §9.3. This is the
+  authoritative surface for the formalization release-line picture
+  across the program — Corpus-side at /corpus/taulib/ (W8a) and
+  Verify-side at /verify/taulib/ (W8b) both link here.
+
+  Anchor id: formalization-release-lines (used by deep-links from
+  the Corpus + Verify TauLib pages).
+-->
+
+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).
+
+<a id="formalization-release-lines"></a>
+
+| 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 |

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
+
+<!--
+  v5 next-wave W8b · IA Doctrine v5 §9.2 + Release Lines Addendum §7.
+  Source: atlas/website/v5/panta-rhei-release-lines-formalization-
+          surfaces-v5-addendum.md §7 (TauLib Release Lines) + §9.2
+          (Verify lane TauLib representation).
+  Data:   _data/release_lines.yml · formalization_release_lines.
+
+  Inspection-bridge view of the same release lines that /corpus/
+  taulib/ surfaces (Corpus side, W8a). Each line is read here as
+  a trust-boundary surface: which line is citable as a proof basis,
+  which is active and therefore not yet citable, and which packages
+  are released per-result.
+-->
+
+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:
+
+<ul class="v2-grid v2-card-list">
+  <li><article class="v2-tile">
+    <h3>TauLib v2 Snapshot</h3>
+    <p><strong>Citable as a proof basis.</strong> Frozen Lean projection of the Second-Edition Corpus; pinned commit and Lean toolchain are stamped in the <a href="{{ '/verify/release-manifest/' | relative_url }}">Release Manifest</a>. Reviewers can clone the pinned commit, re-run <code>lake build</code>, and reproduce the compilation result that this page reports.</p>
+  </article></li>
+  <li><article class="v2-tile">
+    <h3>TauLib v3 Library</h3>
+    <p><strong>Active restructure · not yet citable.</strong> Layered library — import-isolated kernel, Mathlib-facing bridges, community-readable module structure — currently in private development. Not a proof basis for any cited Result until it ships publicly; current Results cite the v2 Snapshot.</p>
+  </article></li>
+  <li><article class="v2-tile">
+    <h3>Proof Packages</h3>
+    <p><strong>Per-result · per-package state.</strong> Isolated reproducibility bundles for specific formal results. Each package moves through five states: <em>in construction · draft · candidate · released · superseded</em>. Released packages are citable as a per-result proof basis; non-released states should not be cited as proof.</p>
+  </article></li>
+</ul>
+
+> **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: