v5w2-w8a(release-lines-corpus): Formalization Release Lines on /corpus/taulib/ + Research Code adjacency on /publications/#269
Merged
Conversation
…s/taulib/ + Research Code adjacency on /publications/
Source: atlas/website/v5/panta-rhei-release-lines-formalization-
surfaces-v5-addendum.md §7 (TauLib Release Lines) + §9.1
(Corpus lane TauLib representation) + §9.5 (Publications
lane — Research Code adjacency).
Data: _data/release_lines.yml · formalization_release_lines
(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 8a).
W8b will follow with the Verify-side surfaces — Release Lines
section on /verify/taulib/ + Formalization Release Lines table on
/verify/release-manifest/ — closing out Wave 8 and the v5w2 cycle.
══ What lands ════════════════════════════════════════════════════════
corpus/taulib/index.md (+30 / 0)
────────────────────────────────
New "## Formalization Release Lines" section inserted between
"Compiled Lean projection" and "Entry points". Three-tile grid:
TauLib v2 Snapshot — Frozen Lean projection · Public · pinned ·
citable. Current public docs at taulib.site
render against this snapshot.
TauLib v3 Library — Layered active library · In preparation ·
private repository · not yet citable.
Research Modules / — Per-result proof packages with five-state
Proof Packages lifecycle (in construction · draft · candidate ·
released · superseded).
Doctrine comment block above the section pins both Addendum §7 + §9.1
sources so future editors can re-derive the framing.
Closing sentence makes the "the everything-below-this-section refers
to the v2 Snapshot" boundary explicit — Entry points + Verification
boundary sections are unchanged but now correctly scoped to v2.
publications/index.md (+18 / 0)
───────────────────────────────
New "## Adjacent class — Research Code" section inserted after the
"Reference and provenance" grid and before the Glossary. Two-tile
grid linking to /corpus/taulib/ (Corpus-side) + /verify/taulib/
(Verify-side inspection bridge). Reframes the read-by-running
shape distinction explicitly so the four-class prose taxonomy
shipped in W7a stays clean while making Research Code's
publication-adjacent status visible.
Doctrine comment block pins Addendum §9.5 source.
══ URL preservation posture ═════════════════════════════════════════
Purely additive — no existing URL changes, no existing content
removed or hidden. The Compiled Lean projection counts block,
Entry points grid, and Verification boundary CTAs on corpus/taulib
stay verbatim; the Publications landing's 4-class primary grid +
Reference and provenance grid + Glossary + decision tree 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)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
W8a of the v5 next-wave cycle — first half of the final wave. Surfaces the Corpus-side formalization release lines on
/corpus/taulib/and makes Research Code's publication-adjacent status visible on/publications/.Per Release Lines + Formalization Surfaces v5 Addendum §7 (TauLib Release Lines), §9.1 (Corpus lane TauLib representation), §9.5 (Publications lane — Research Code adjacency). Data ground-truth was shipped in W1 as
_data/release_lines.yml::formalization_release_lines.W8b will follow with the Verify-side surfaces (
/verify/taulib/release-lines section +/verify/release-manifest/Formalization Release Lines table) closing the cycle.What lands
corpus/taulib/index.md(+30 / 0)New "Formalization Release Lines" section inserted between "Compiled Lean projection" and "Entry points". Three-tile grid:
Closing sentence makes the "everything below this section refers to the v2 Snapshot" boundary explicit — Entry points + Verification boundary sections unchanged but now correctly scoped to v2.
publications/index.md(+18 / 0)New "Adjacent class — Research Code" section inserted after the "Reference and provenance" grid and before the Glossary. Two-tile grid:
/corpus/taulib/— the compiled Lean projection/verify/taulib/— what Lean compilation establishes + axiom/sorry policyFrames the read-by-running shape distinction explicitly so the four-class prose taxonomy (W7a) stays clean while making Research Code's publication-adjacent status visible.
URL preservation posture
Purely additive. No existing URL changes, no existing content removed or hidden. The Compiled Lean projection counts block, Entry points grid, and Verification boundary CTAs on
corpus/taulibstay verbatim; the Publications landing's 4-class primary grid + Reference and provenance grid + Glossary + decision tree all preserved.Test plan
/corpus/taulib/renders the new "Formalization Release Lines" section with all three tiles between "Compiled Lean projection" and "Entry points"taulib.site/verify/taulib//verify/release-manifest/#formalization-release-lines(will become a real anchor after W8b)/publications/renders the new "Adjacent class — Research Code" section after Reference & provenanceGates run locally
scripts/check_hardcoded_release_numbers.pyscripts/check_release_manifest_parity.py🤖 Generated with Claude Code