docs: update #000031 status + CLAUDE.md textbook layer pointers

Reflects today's surface-ingest landings — Phase 1 (PD + open-licensed textbooks across 6/7 g4 pillars) is in progress; Phase 2 (chunk-resolution + derivations.proof_blob warrant promotion) is the next substantial commit. #000031 ticket file =================== - Status flipped from "open · awaiting go/no-go" to "in progress · Phase 1 landed 2026-05-09". - §8 rewritten with the landed scope: 8 textbooks ingested across 3 license-validated manifest paths (HTML, BFS crawl, PG TeX), total ~351 docs / ~1597 chunks. - Coverage table per g4 pillar. - Phase 2 scope explicit: citation parser, chunk resolver, Merkle inclusion proof writer, derivations row writer, verifier wiring, bench. ~300-500 LOC estimate. - Phase 3 (Mendelson + Enderton license decision) still deferred; Hilbert-Ackermann 1928 noted as PD substitute. docs/TICKETS.md =============== Index row updated to reflect "in progress · Phase 1 landed". CLAUDE.md ========= - sources/ comment lists the new textbook_tex source. - Added textbook-layer make-target block to the build/test/run section — make crawl-textbooks, make textbooks-tex, make textbook ID=<id>, with the idempotency callout. No source-code changes — pure documentation refresh aligned to what shipped this session (commits b38f4b8 → 514e07d).
2026-05-09 16:13:31 -04:00 · 2026-05-09 16:13:31 -04:00 · 056dda2fd7
commit 056dda2fd7
parent 514e07d7c2
3 changed files with 125 additions and 12 deletions
--- a/CLAUDE.md
+++ b/CLAUDE.md
@ -49,7 +49,8 @@ arborist/
 ├── ingest.py        # batched normalize → chunk → merkle → upsert
 ├── evict.py         # hot↔cold + rehydrate (v9.8 falsification on drift)
 ├── search/          # SearchBackend ABC + AuditMode + FTS5
-├── sources/         # one file per corpus (wikipedia, html_page)
+├── sources/         # one file per corpus (wikipedia, html_page,
+│                   # claim_pack, textbook_tex, grok, vcs, …)
 ├── distill/         # surface → core distillation (tfidf, first_sentence)
 ├── qa/              # Q&A: 8-dim cache_key + Merkle-bound answers
 │   ├── client.py    #   ChatClient + StubClient + OpenAICompat
@ -82,6 +83,15 @@ make analyze-shards      # cross-shard compression + audit integrity
 make chain-check-shards  # audit-chain break count per shard (0 = intact)
 make query Q="..." [JSON=1 BURN=1 K="extra retrieval keywords" ANSWER_MODE=…]
 make bench-qa            # QA-quality sweep (live LLM)
+
+# Textbook surface-ingest layer (#000031 — PD/open-licensed
+# math/logic/CS textbooks for warrant promotion):
+make textbooks-summary   # license + URL counts per manifest entry
+make crawl-textbooks     # BFS-crawl every entry with crawl_url
+                         #   → ~/.arborist/crawl/textbook_<id>.db
+make textbooks-tex       # PG LaTeX-source ingest (Hilbert, Boole)
+make textbook ID=<id>    # ingest one textbook by manifest id
+                         # (idempotent at DB layer)
 ```

 **Hygiene after any state-changing op** (rebuild, reclassify, hash
--- a/docs/TICKETS.md
+++ b/docs/TICKETS.md
@ -66,7 +66,7 @@ Newest first. Update on every open/close.
 | #000034  | Hessian alignment under φ_linear               | open · awaiting go/no-go (#000018 follow-up) | 2026-05-09 | —         |
 | #000033  | Claim-pack pillar VII (combinatorics)          | closed · landed 2026-05-09 (live in shard 000.db; lift verified) | 2026-05-09 | —         |
 | #000032  | combinatorics@v1 π* (integer counting kernel) | closed · landed 2026-05-09 | 2026-05-09 | —         |
-| #000031  | Surface-ingest cited textbooks for claim-pack warrant promotion | open · awaiting go/no-go | 2026-05-09 | —         |
+| #000031  | Surface-ingest cited textbooks for claim-pack warrant promotion | in progress · Phase 1 (8 textbooks, 6/7 pillars) landed 2026-05-09; Phase 2 chunk-resolution ahead | 2026-05-09 | —         |
 | #000030  | Math π* expansion: SymPy substrate (algebra · calculus · linalg) | closed · all 7 phases + 1b landed 2026-05-09 (`abe5988`) | 2026-05-09 | —         |
 | #000029  | Claim-pack source (axiom/theorem JSON bundles) | closed · landed 2026-05-09 | 2026-05-09 | —         |
 | #000028  | Multi-modality witness for canonical shapes    | closed · landed 2026-05-09 + follow-ups (capital ledger · sample rate) | 2026-05-08 | —         |
--- a/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md
+++ b/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md
@ -1,6 +1,6 @@
 # Ticket #000031 — Surface-ingest cited textbooks for claim-pack warrant promotion

-**Status:** open · awaiting go/no-go
+**Status:** in progress · Phase 1 (PD textbook surface ingest) landed 2026-05-09 covering 6/7 g4 pillars; Phase 2 (chunk-resolution + `derivations.proof_blob` warrant promotion) still ahead
 **Opened:** 2026-05-09
 **Scope:** Ingest the classical textbooks cited by every record in
 the claim-pack source (`#000029`) — Mendelson 1997, Enderton 2001,
@ -306,14 +306,117 @@ After both sources ingest:

 ## 8. Status

-Open · awaiting go/no-go.
+**Phase 1 landed 2026-05-09 — PD + open-licensed textbook surface
+ingest with manifest + idempotent make targets.**

-Estimated size:
+### Phase 1 — landed scope

- Phase 1 — green-light textbook ingest (PD only): ~250 LOC for
-  `TextbookSource` + ~50 LOC manifest + tests + small data files.
-  Plus ~3 MB of textbook plain-text data (not committed; downloaded
-  via fetcher).
- Phase 2 — Mendelson/Enderton license decision + ingest if
-  green-lit: design pending.
- Phase 3 — chunk-resolution layer: separate ticket entirely.
+License-validated manifest at `bench/fixtures/textbooks/manifest-v1.jsonl`
+with allow-list (`PD`, `CC0`, `CC-BY-*`, `CC-BY-SA-*`, `GFDL-*`,
+`AGPL-3.0`, `Apache-2.0`, `MIT`). Fail-closed validator
+(`bench/scripts/textbooks_manifest.py`) refuses to emit URLs from
+entries with disallowed license tokens. **Excluded:** any
+`CC-BY-NC` (incompatible with arborist's AGPLv3 distribution
+profile), any `CC-BY-ND` (no-derivatives prevents chunking),
+proprietary.
+
+Two ingest paths, idempotent at the database layer:
+
+```
+make fetch-textbooks      # shallow URL list → single shard
+make crawl-textbooks      # deep BFS via existing crawler →
+                          #   one shard per textbook id
+make textbook ID=<id>     # per-book convenience target
+make textbook-bogart      # convenience for individual book
+make textbook-keller-trotter  # (slow ~25min crawl-delay)
+make textbook-levin
+make textbook-aristotle-prior
+make textbook-aristotle-posterior
+make textbook-newton
+make textbook-morin
+make textbooks-tex        # TeX-source ingest path for PG eBooks
+make textbook-hilbert     # PG #17384 (LaTeX source only)
+make textbook-boole       # PG #15114 (LaTeX source only)
+```
+
+Idempotency: every ingest path is content-addressed. Same content
+→ same `document_root` → no-op insert. Re-running any target on
+the same network state is safe at the DB layer. HTTP refetch
+happens every run; pair with `make recrawl-check` for HEAD-only
+freshness probe.
+
+Eight textbooks landed across six g4 pillars:
+
+| Pillar | Source | License | Format | Docs / Chunks |
+|---|---|---|---|---|
+| I  Logic | Aristotle Prior Analytics | PD | HTML/Wikisource | 30 / 110 |
+| I  Logic | Aristotle Posterior Analytics | PD | HTML/Wikisource | 20 / 71 |
+| I  Logic | Boole *Laws of Thought* | PD | TeX/PG #15114 | 1 / 273 |
+| I,II,III,VII | Levin *Discrete Math* 3rd | CC-BY-SA-4.0 | HTML/PreTeXt | 51 / 376 |
+| IV Geometry | Hilbert *Foundations* | PD | TeX/PG #17384 | 1 / 65 |
+| VI Physics | Newton *Principia* (Motte) | PD | HTML/Wikisource | 60 / 289 |
+| VII Combin. | Bogart *CTGD* | GFDL-1.3 | HTML/openmathbooks | 44 / 161 |
+| VII Combin. | Keller-Trotter *Applied* | CC-BY-SA-4.0 | HTML/PreTeXt | 80 / 168 |
+| VII Combin. | Morin *Open Data Structures* | CC-BY-2.5 | HTML/opendatastructures | 64 / 84 |
+
+**Total surface coverage: ~351 documents, ~1597 chunks** in the
+crawl-shard cluster at `~/.arborist/crawl/textbook_*.db`.
+
+New ingest source landed: `arborist/sources/textbook_tex.py`
+(`TextbookTexSource`) — fetches `.tex` URL, runs PG-aware regex
+strip pipeline (drops preamble + comments + tabular/figure envs;
+keeps args of `\textbf`/`\emph`/`\section`/`\rfa`; substitutes
+`\to` → →, `\neg` → ¬, `\forall` → ∀, etc.). Pandoc fails on
+PG's custom preamble macros; the regex stripper is the right
+amount of machinery for the well-known PG TeX format. 20 unit
+tests; full suite: 1574 passed / 28 skipped.
+
+### Phase 1 gaps (still open)
+
+- **Pillar V (Probability)** — Kolmogorov *Foundations of the
+  Theory of Probability* license analysis pending. German
+  original PD-by-age in EU; US copyright restored via URAA
+  through 2058 (Kolmogorov d.1987 → life+70). Morrison 1956
+  English translation Chelsea-copyrighted. Manifest entry kept
+  with empty urls field for citation traceability.
+- **Pillar IX (λ-Calculus)** — Church 1936 + Turing 1936 are
+  paper-length, not book-length. Awaits a paper-ingest helper
+  (separate scope).
+- **Mendelson + Enderton (Pillar I logic)** — proprietary,
+  yellow-light pending license decision per §2.1. Manifest entry
+  kept as a license-fail placeholder.
+
+### Phase 2 — chunk-resolution + warrant promotion (NOT YET LANDED)
+
+The data substrate is in place; the warrant promotion itself
+requires:
+
+1. **Citation parser** — `source_reference` string ("A
+   Mathematical Introduction to Logic by Herbert B. Enderton")
+   → structured `(authors, title, year, section?)` tuple.
+2. **Chunk resolver** — given a citation, FTS5-search candidate
+   surface shards for theorem name + key terms, return top
+   chunk(s).
+3. **Merkle inclusion proof writer** — for each (claim_pack
+   record, surface chunk) match, compute the per-chunk inclusion
+   proof using `arborist/merkle.py`, serialize to JSON.
+4. **`derivations` row writer** — `(core_root,
+   src_root, proof_blob, process_id="warrant-resolver-v1",
+   distilled_at)`.
+5. **Verifier wiring** — `audit_mode` upgrade path so claims
+   with a `derivations` row tying back to a real surface get
+   **EVIDENCE-WARRANTED** instead of ANCHOR-WARRANTED on the
+   four-rung ladder.
+6. **Bench** — verify a known case (e.g., Modus Tollens
+   claim-pack record → Aristotle Prior Analytics chapter)
+   actually promotes from ANCHOR to EVIDENCE.
+
+Estimated size: ~300-500 LOC across the resolver + proof writer
+ verifier wiring + bench fixtures. Single substantial commit.
+
+### Phase 3 — proprietary-textbook decision (deferred)
+
+Mendelson + Enderton ingestion still requires fox's explicit
+license decision per §2.1. Hilbert-Ackermann 1928 *Principles of
+Mathematical Logic* is the recommended PD substitute (covers the
+same ground; PD by age).