From 056dda2fd7318ff020a97eeefbde1e3a7df139fd Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Sat, 9 May 2026 16:13:31 -0400 Subject: [PATCH] docs: update #000031 status + CLAUDE.md textbook layer pointers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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=, with the idempotency callout. No source-code changes — pure documentation refresh aligned to what shipped this session (commits b38f4b8 → 514e07d). --- CLAUDE.md | 12 +- docs/TICKETS.md | 2 +- ...t-000031-surface-ingest-cited-textbooks.md | 123 ++++++++++++++++-- 3 files changed, 125 insertions(+), 12 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index c58fd45..86b86e5 100644 --- 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_.db +make textbooks-tex # PG LaTeX-source ingest (Hilbert, Boole) +make textbook ID= # ingest one textbook by manifest id + # (idempotent at DB layer) ``` **Hygiene after any state-changing op** (rebuild, reclassify, hash diff --git a/docs/TICKETS.md b/docs/TICKETS.md index dbb2102..4850fac 100644 --- 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 | — | diff --git a/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md b/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md index aeb4595..a8a068c 100644 --- 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= # 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).