[Reference] Collaborative textbook workflow implementation

[Deicyde]

Moved from #8. Its head branch lived on VivienCabannes/autoform-bot, which is being deleted, so this PR uses the same-named branch in facebookresearch/autoform-bot (same commits, head 1cf2ca8). Earlier review and discussion are on #8.

---

Reference implementation

Frozen full implementation at 1cf2ca825fec5e6d3303e24374e218bf3e8ab5c1. The smaller PRs below are the review and landing path.

Replacement PRs

Lean runtime:

• Harden Lean REPL transport and response handling #13 REPL transport and response protocol
• Share bounded Lean runtime state #29 Shared runtime lifecycle and CI gates (closed, superseded by Migrate the Lean LSP backend to Lean Beam #41)
• Resolve project-scoped Lean imports safely #30 Project-scoped import resolution and freshness validation (closed, superseded by Replace custom Lean servers with managed Lean Beam #76)
• Execute structured Lean imports in isolated REPLs #31 One-shot structured-import execution (closed, superseded by Replace custom Lean servers with managed Lean Beam #76)
• Make public Lean REPL calls disposable #37 Disposable public REPL lifecycle (closed, superseded by Migrate the Lean LSP backend to Lean Beam #41)

Project lifecycle:

• Add bounded Lean project inspection #14 Project inspection and tested release catalog
• Verify installed plugin provenance #16 Verified plugin provenance (closed, design deprecated)
• Create Lean projects atomically with catalog-backed defaults #96 Atomic project creation (replaces Create Lean projects atomically #26, without the provenance dependency)
• Conservative project repair (Repair incomplete Autoform projects conservatively #71 closed: it depended on Verify installed plugin provenance #16 and Create Lean projects atomically #26; a rebuild should start from Create Lean projects atomically with catalog-backed defaults #96)

Collaborative textbook workflow:

• Scale roadmap graph traversal #15 Graph scaling
• Bind Lean source snapshots to filesystem generations #95 Descriptor-bound, bounded source snapshots (replaces Bind Lean source snapshots to filesystem generations #28)
• Publish blueprint sites transactionally #73 Transactional publication
• Add session-fenced collaborative claims #72 Collaborative claim leases
• Verify local Lean artifacts before publication #69 Local artifact-integrity gate
• Verify Mathlib artifact provenance #74 Mathlib provenance gate
• Coverage v2 source-unit contract
• Immutable execution input
• Workspace read model
• Atomic workspace registry
• Atomic blueprint creation
• Ready-work CLI, orchestration skill, README, and final integration

Each PR is reconstructed from this final tree, independently reviewed, and validated with focused tests, the complete suite, and relevant Lean or bundled-example checks. The cumulative result will be compared with this reference, excluding reviewed hardening fixes and metadata-only changes.

[Deicyde]

Closing this draft as a historical reference, not as a rejection of every product goal.

The exact prototype remains available at 1cf2ca825fec5e6d3303e24374e218bf3e8ab5c1, with the earlier discussion on #8. It should not be merged or restacked wholesale.

This PR is no longer a reliable roadmap:

• current main has diverged substantially and this 98-file frozen tree is conflicting;
• the checklist conflates merged, superseded, deprecated, and abandoned work;
• Bind Lean source snapshots to filesystem generations #95 and Create Lean projects atomically with catalog-backed defaults #96 have landed, while Verify local Lean artifacts before publication #69 is closed and replaced by Rebuild artifact verification on bound project evidence #145;
• the product surface moved from ready/orchestrate and a custom controller to autoform work, the formalize skill, and native agents;
• exact-head review found integration defects, including workspace verification auditing a literal blueprint path and newly created vaults lacking the coverage/identity contract that ready required.

The surviving outcomes are now tracked from current main in the rewritten roadmap issue #25 and focused successors: #105, #106, #107, and #110 for REPL safety; #119 and #145 for artifact integrity; #120, #121, #122, #123, and #130 for claims/publication integrity; #17, #19, #22, and #23 for evidence and collaboration contracts; and #18, #20, #21, and #24 for the conditional multi-project workspace direction.

Old draft branches #72-#74 are sources of ideas and tests only; any surviving narrower goal must be rebuilt on current foundations. No future change should be accepted merely to reproduce this frozen tree.