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' 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: