diff --git a/CLAUDE.md b/CLAUDE.md index 6b1e7cf..d6edfb3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -386,6 +386,11 @@ North-star: - `docs/seven-point-program.md` — the architectural directive distilled 2026-05-01. Every new ticket / feature / prompt edit walks past this. Bench harness reports per-mode directive coverage. +- `docs/warrant-substrate-cookbook.md` — per-pillar map of the 18 + open-licensed textbook substrates that back every claim-pack + record. Ingest patterns (HTML / textbook_tex / PDF→localhost), + alias discipline, cascade tuning, honest tier breakdown. + Read first when extending substrate coverage. Architecture / ongoing work: diff --git a/docs/TICKETS.md b/docs/TICKETS.md index 90d7122..80b72e5 100644 --- a/docs/TICKETS.md +++ b/docs/TICKETS.md @@ -51,6 +51,11 @@ proposing change. Examples that stay un-numbered: provenance layer downstream of `final_label`. Captured pre-ticket per the 2026-05-07 arborist-vs-donto comparison; promotes to a ticket when an actual agent use case surfaces) +- `warrant-substrate-cookbook.md` (architecture reference for the + 18 open-licensed textbook substrates backing every claim-pack + record, written 2026-05-10 after the 18/92 → 92/92 push under + `#000031`. Per-pillar substrate map, ingest patterns, alias + discipline, cascade tuning, honest tier breakdown.) If a doc proposes change AND awaits a decision AND has scoped implementation cost, it's a ticket. Otherwise it's reference. diff --git a/docs/warrant-substrate-cookbook.md b/docs/warrant-substrate-cookbook.md new file mode 100644 index 0000000..b370e1f --- /dev/null +++ b/docs/warrant-substrate-cookbook.md @@ -0,0 +1,436 @@ +# Warrant substrate cookbook + +Architecture reference for the open-licensed textbook substrate +that backs every claim-pack record in arborist. Written +2026-05-10 after the day-long push from 18/92 → 92/92 claim-pack +warrant-chain coverage. Intended for future blackops shifts so +they don't have to re-derive the substrate map from bench +journals. + +## What this cookbook is + +When a Q&A answer cites a claim-pack record (axiom or theorem), +the runtime walks a chain: + +``` +answer cite + ↓ +claim-pack record_root (g4-generated 2025) + ↓ +derivations row (process_id, citation, src_root, proof_blob) + ↓ +surface chunk_root (open-licensed textbook) + ↓ +Merkle inclusion proof → document_root + ↓ +audit_events chain entry (sha256-linked) +``` + +The "open-licensed textbook" at the second-to-last step is the +**substrate**. This document maps which substrate covers which +pillar, what license + ingest path each uses, and the discipline +patterns that keep the chains audit-clean. + +## Pillar-by-pillar substrate map + +Eight pillars in the claim-pack source (`#000029`); 92 records +total. As of 2026-05-10, every record resolves to at least one +substrate in `~/.arborist/crawl/textbook_*.db`. + +### Pillar I — Logic (13 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Russell *Introduction to Mathematical Philosophy* (1919) | PD | PG #41654 single-page HTML | natural numbers, classes, descriptions, types, propositional functions | +| Russell *Principles of Mathematics* (1903) | PD content + CC-BY-SA-4.0 typesetting | Klement single-page HTML | class theory, relations, paradox derivation, magnitudes | +| De Morgan *First Notions of Logic* (1839) | PD | PG #67017 single-page HTML | AEIO propositions, syllogism, hypothetical reasoning | +| Boole *Investigation of the Laws of Thought* (1854) | PD | PG #15114 LaTeX-source via `textbook_tex` | propositional Boolean algebra, "elective symbols" | +| Software Foundations Vol 1 *Logical Foundations* | MIT | softwarefoundations.cis.upenn.edu BFS | natural deduction (Logic.v): excluded middle, double negation, existential introduction, vacuous quantification | +| Whitehead-Russell *Principia Mathematica Vol 1* (1910, partial) | PD | PG #78050 single-page HTML | preface + intro + chs I-III; theory of types in narrative form | + +Modern citations (Mendelson, Enderton) are aliased per #000041 to +combinations of these substrates depending on the specific axiom. + +### Pillar II — Set theory (10 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Cantor *Contributions to the Founding of the Theory of Transfinite Numbers* (Jourdain 1915) | PD | Wikisource Article 1 only | cardinal arithmetic, equivalence, addition / multiplication / exponentiation, finite cardinals | +| Russell *Principles of Mathematics* (1903) | PD content + CC-BY-SA-4.0 typesetting | Klement HTML | Russell's Paradox derivation, class theory | +| Whitehead-Russell *PM Vol 1* (partial) | PD | PG #78050 | type theory narrative | + +Modern Jech citations alias to these. Note: Cantor's Article 2 +(operations on ordered sets) is not transcribed on Wikisource; the +Article 1 transcription covers cardinal-arithmetic axioms but not +ordinal axioms. PM *24+ formal type theory is not in PG #78050 +(only preface + intro + chs I-III), so the **Russell's Paradox +Resolution** record matches via lexical fallback against narrative +discussion rather than the actual *24 formalism — honest soft +match, not a strict primary binding. + +### Pillar III — Arithmetic (13 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Peano *Arithmetices Principia, Nova Methodo Exposita* (1889) | CC-BY-SA-4.0 (Verheyen + Nahas English transl.) | mdnahas/Peano_Book GitHub LaTeX via `textbook_tex` | Peano arithmetic axioms (zero, successor, induction) | +| Dedekind *Essays on the Theory of Numbers* (Beman 1901) | PD | PG #21016 LaTeX via `textbook_tex` | Dedekind cuts construction of reals + chains-and-induction definition of natural numbers | +| Russell *Introduction to Mathematical Philosophy* (1919) | PD | PG #41654 HTML | natural numbers, definition of number, induction (informal) | +| Software Foundations Vol 1 *Logical Foundations* | MIT | upenn BFS | Coq induction proofs, lists, polymorphism | + +Landau + Gödel citations alias to these. Note: Peano writes +symbolically (`0 ∈ N`); the cascade's parenthetical-phrase variant ++ OR-fallback variant land hits via SF-LF / Russell IMP / +Dedekind for axiom records that cite "Axiom of Zero" / +"Distinctness of Zero" / "Injectivity of Successor" / etc. (the +direct phrase doesn't appear in Peano's text). + +### Pillar IV — Geometry (18 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Hilbert *Foundations of Geometry* (Townsend 1902) | PD | PG #17384 LaTeX via `textbook_tex` | every Hilbert axiom (incidence, betweenness, congruence, parallels, continuity) | + +This pillar resolves directly — the Hilbert citation in claim-pack +records IS the textbook in shard. 11/18 match unaliased; 7/18 +match via term-aliases (#000042) bridging the 1902 Townsend +vocabulary vs modern ("connection" vs "incidence", "Group III: +Axiom of Parallels" vs "Euclidean Parallel Postulate", "space +axiom" vs "Non-Triviality", "first theorem of congruence" vs +"Side-Angle-Side"). Pillar IV is the cleanest demonstration that +the substrate-binding works end-to-end. + +### Pillar V — Probability (5 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Grinstead-Snell *Introduction to Probability* | GFDL-1.3 | Dartmouth PDF → `pdftotext -layout` → localhost-HTML → `arborist ingest --source html` | Kolmogorov axiomatized probability spaces, sample spaces, conditional probability, Bayes, expected value, large numbers | +| Laplace *A Philosophical Essay on Probabilities* (Truscott + Emory 1902) | PD | PG #58881 single-page HTML | pre-Kolmogorov narrative treatment: expected value, conditional probability, additivity | + +Kolmogorov 1933 itself is URAA-blocked in US until 2058 +(Kolmogorov d.1987 → life+70). Grinstead-Snell is the closest +open-licensed equivalent. The PDF→localhost-HTML pipeline (see +Ingest patterns below) was first proven on this textbook. + +### Pillar VI — Classical mechanics (5 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Newton *Principia* (Motte 1729) | PD | Wikisource HTML BFS depth=3 max=120 from /1729/ root | three laws of motion + universal gravitation | + +Goldstein-Poole-Safko citations alias to Newton. Newton 1729 vocab +(`Lex Tertia`, `quantity of motion`, `every action`) differs from +modern; 4 term-aliases registered in #000042 for completeness +(some lift via cascade, some don't matter — cascade picks other +discriminators). + +The shard was rebuilt 2026-05-10 — the original `crawl_url` at +`/The_Mathematical_Principles_of_Natural_Philosophy` (no edition +specifier) followed Wikisource sidebar links instead of book +content. New manifest entry pins the (1729) edition root + +explicit `urls` for Axioms / Definitions / Rules of Reasoning +subpages. Recrawl produced 120 docs / 779 chunks (was 60 / 289 of +mostly nav cruft). + +### Pillar VII — Combinatorics (14 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Bogart *Combinatorics Through Guided Discovery* | GFDL-1.3 | bogart.openmathbooks.org BFS | introductory: sum/product, binomial, inclusion-exclusion, pigeonhole | +| Levin *Discrete Mathematics: An Open Introduction* (3rd ed) | CC-BY-SA-4.0 | discrete.openmathbooks.org BFS | intermediate: stars-and-bars, hockey-stick, generating functions intro | +| Keller-Trotter *Applied Combinatorics* | CC-BY-SA-4.0 | appliedcombinatorics.org BFS (38-min crawl-delay) | advanced: generating functions, partitions, Polya enumeration | + +Stanley + Brualdi + Knuth combinatorics citations alias to all +three substrates per source_ref string (14 unique compound strings +each get three substitute rows; pillar VII has 42 alias rows total +of the 54 in `citation_aliases`). + +Note: Keller-Trotter has `Crawl-Delay: 20` in robots.txt, so a +full BFS at depth=2 max=80 takes ~27-38 minutes. Background-task +the crawl with a generous timeout. + +### Pillar IX — Lambda calculus + abstract algebra (14 records) + +| Substrate | License | Source | Covers | +|---|---|---|---| +| Programming Language Foundations in Agda (PLFA — Wadler/Kokke/Siek) | CC-BY-4.0 | plfa.github.io BFS | untyped + simply-typed lambda calculus, β/α/η reduction, Confluence/Church-Rosser, fixed point | +| Software Foundations Vol 1 *Logical Foundations* | MIT | upenn BFS | Coq induction, lambda calculus, Imp.v sequence/conditional/while-loop | +| Judson *Abstract Algebra: Theory and Applications* | GFDL-1.3 | judsonbooks.org PreTeXt BFS | groups, rings, fields, Galois theory, Boolean lattices, Cayley + orbit-stabilizer | + +Barendregt + Dummit-Foote + Böhm-Jacopini citations alias to +these. PLFA is the lambda-calculus core; SF-LF doubles as a logic +substrate (pillar I) AND a structured-programming substrate +(Böhm-Jacopini Imp.v); Judson is the abstract-algebra primary +substitute. + +## Ingest patterns + +Five proven patterns. Pick whichever matches your source. + +### A. HTML single URL (`urls` in manifest) + +For PG eBooks with a single-page HTML edition (Russell IMP, De +Morgan, Laplace) or Wikisource transcriptions (Cantor Article 1). +Manifest entry: + +```jsonl +{"id":"foo","urls":["https://...html"], ...} +``` + +Make target: `make textbook ID=foo`. Calls `arborist ingest +--source html --urls-from `. + +### B. HTML BFS crawl (`crawl_url` + `crawl_depth` + `crawl_max`) + +For multi-chapter HTML books (PreTeXt: Bogart, Levin, KT, Judson; +Wikisource book-length texts: Newton, Aristotle Prior/Posterior; +LibreTexts: Grinstead-Snell). Manifest entry: + +```jsonl +{"id":"foo","crawl_url":"https://...","crawl_depth":2,"crawl_max":80, ...} +``` + +Make target: `make textbook ID=foo`. Calls `arborist crawl --seed-url +... --depth ... --max-pages ... --ingest`. + +Robots.txt `crawl-delay` is honored. Plan timeouts: appliedcombinatorics +20s × 80 pages = 27-38 min; plfa.github.io ~5 min; opendatastructures +~1 min. + +### C. LaTeX-source (`tex_url`) + +For PG eBooks with no HTML edition (Hilbert, Boole, Dedekind) or +GitHub-hosted LaTeX (Peano). Manifest entry: + +```jsonl +{"id":"foo","tex_url":"https://.../foo.tex","license":"PD", ...} +``` + +Make target: dedicated per-book like `make textbook-hilbert` (the +generic `make textbook` route doesn't handle `tex_url`). Calls +`arborist ingest --source textbook_tex --url ...`. Pipeline strips +PG-style preamble + tabular/figure envs; substitutes `\to` → →, +`\neg` → ¬, `\forall` → ∀. + +Limitation: `paracol` multi-column macros (Peano) leak some +residue (`gobble 1cm`, `0.5cm`, `paracol3`) but substantive prose +extracts cleanly. If the source uses heavy custom macros, expect +some noise. + +### D. PDF → localhost-HTML → html-source + +For sources that have a PDF but no clean HTML (Grinstead-Snell +Dartmouth PDF; Bayes 1763 Royal Society scan; Frege Begriffsschrift +Internet Archive). Pattern: + +```bash +curl -sLo /tmp/foo.pdf https://... +pdftotext -layout /tmp/foo.pdf /tmp/foo.txt +mkdir -p /tmp/serve +{ echo '...
';
+  cat /tmp/foo.txt;
+  echo '
'; } > /tmp/serve/foo.html + +cd /tmp/serve && python3 -m http.server 8765 & +SRV_PID=$! +sleep 2 +arborist --db ~/.arborist/crawl/textbook_foo.db ingest \ + --source html --url "http://localhost:8765/foo.html" +kill $SRV_PID +``` + +Then run the title backfill (see Discipline patterns below). + +### E. Direct chunk insertion (Python API) + +For one-off cases where none of A-D fit. Walk +`arborist.document.Document` + `arborist.store.connect` to insert +manually. Used when wrapping non-standard sources. + +## Discipline patterns + +### Title-from-author backfill + +**Empirical defect:** HTML and `textbook_tex` ingest pipelines +take document titles from `` tags or URLs. Wikisource and +Project Gutenberg HTML pages do NOT include author surname in +`<title>`. Resolver's `_shard_matches_citation` REQUIRES the +cited author's surname to appear in the shard's title-haystack; +silently fails for alias-resolved chains where the substitute +author isn't self-evident in the shard. + +**Workaround until source-side fix lands** (#000031 Phase 1 +follow-up): SQL UPDATE on `documents.title` after every ingest: + +```python +import sqlite3 +c = sqlite3.connect(shard_path) +c.execute( + "UPDATE documents SET title = title || ', by <author surname>' " + "WHERE title NOT LIKE '%<author surname>%'" +) +c.commit() +``` + +For HTML BFS shards with many docs (Judson 39, Bogart 51, Levin +51, KT 79, PLFA 58, SF-LF 33), append-suffix pattern. For +single-doc shards (Russell IMP, Russell PoM, Cantor, Dedekind, +Peano, Laplace, Grinstead-Snell), full title overwrite. + +### Audit discipline on aliases + +Per #000041 / #000042: every alias row carries `decision_by` +(non-empty, audit-fail-closed) + `decision_rationale` (free +text — caveats, peer-vs-primary distinction, partial-coverage +warnings). + +CLI refuses to register without `--by`. Format convention: + +``` +arborist alias citation add ORIGINAL \ + --substitute SUB --author AUTHOR --title TITLE \ + --by "fox 2026-05-10" \ + --rationale "honest sentence about WHY this substitute covers the cited axioms" +``` + +The rationale is the load-bearing field for an audit reviewer. +"Russell IMP covers Mendelson's propositional axioms but not +his incompleteness chapters" is honest. "Russell IMP covers +Mendelson" is not. + +### Multi-substitute aliases + +When one cited proprietary work is best covered by N peer +substrates, register N rows (same `original_ref`, different +`substitute_ref`). Resolver tries each; first hit wins. +Examples: Mendelson → {Russell IMP, De Morgan, Boole, Russell +PoM, SF-LF}. Stanley/Brualdi/Knuth (per source_ref) → {Bogart, +Levin, KT}. + +### Cascade tuning (`_build_record_query_cascade`) + +Two helpers added 2026-05-10: + +1. `_phrase_from_parenthetical(theorem_name)` — extracts + discriminator from trailing parenthetical when one exists. + "Kolmogorov's First Axiom (Non-Negativity)" → `"non + negativity"`. The original `_phrase_for_axiom` was stripping + parentheticals; many substrates used the parenthetical content + as the actual term. +2. **Content-tokens OR-join (top 3)** — soft fallback after the + AND-join (top 5). When AND zeroes out (substrate doesn't have + all 5 tokens together), OR-of-3 reliably surfaces matching + chunks. The +14 record unlock at 84% → 100%. + +Full cascade order, tightest → loosest: + +1. title-phrase +2. parenthetical-phrase (NEW) +3. content-tokens AND-join (top 5) +4. content-tokens OR-join (top 3) (NEW) +5. legacy single-token / discriminating-token query + +## Honest tier breakdown + +The 92 chains have three quality tiers: + +- **Direct primary (~25 records)** — citation matches the literal + textbook ingested. Hilbert pillar IV (18), Goldstein → Newton + (3), Stanley → Bogart for the records Bogart genuinely covers. + Chain is "the cited primary IS in the shard." +- **Substrate substitution (~50 records)** — citation alias to a + peer-level open work that covers overlapping axioms. Audit row + carries `decision_rationale` explaining honesty. Reviewer can + re-judge. +- **Soft-fallback match (~17 records)** — OR-of-top-3 content + tokens surfaced *some* chunk in the substrate that shares + vocabulary. The chunk *contains* relevant terms; whether it + *proves* the axiom is a separate, weaker claim. Heuristic-grade. + +The schema doesn't currently distinguish these tiers. Audit +reviewers walk `citation_aliases` (54 rows) + read +`decision_rationale` fields to grade each chain. If tier +distinction becomes load-bearing, add a `tier ∈ {primary, +substitute, soft}` column to `derivations`. + +## Audit-trail integrity + +Every alias row + every derivation insertion writes one row in +`audit_events` with `event_hash = sha256(prev || canonical(body))`. +Verify chain integrity: + +```bash +make chain-check-shards # 0 per shard = intact +``` + +The `audit_events` chain ensures: if any alias row is later +modified or removed, the chain breaks at that point and downstream +verification fails. Tampering is detectable. + +## What this doesn't yet do + +The substrate is in place; the **render layer doesn't read it**. +Q&A answers citing claim-pack records still display +`ANCHOR-WARRANTED` on the four-rung ladder. #000031 Phase 3 wires +the render layer to consult `derivations` and promote to +`EVIDENCE-WARRANTED`. ~50-100 LOC in +`arborist.cli._render_audit_label`. Not done. + +The `process_id` on alias-resolved derivations is currently +`warrant-resolver-v1` (DIRECT) rather than `warrant-resolver-v1+alias`. +The `via_alias` flag is set only by term-alias query expansion in +`resolve_chunks`, not by citation-alias substitute-Citation +injection in `warrant_resolve`. Audit trail is correct in +`citation_aliases` table itself; just under-attributed in +derivation rows. ~15 LOC fix. + +Per-record tier classification (primary / substitute / soft) +isn't in the schema. Reviewers infer from `citation_aliases` rows ++ `decision_rationale` text. Could be promoted to a column if the +distinction becomes load-bearing for downstream consumers. + +## Re-running the substrate build + +Most steps are idempotent at the DB layer (content-addressed +inserts; same source content → same `document_root` → no-op). +Network refetches happen but inserts dedupe. + +```bash +# Bulk: all four 2026-05-09 base-knowledge additions +make textbooks-base-knowledge + +# Per-book convenience targets +make textbook-bogart textbook-keller-trotter textbook-levin +make textbook-aristotle-prior textbook-aristotle-posterior +make textbook-newton textbook-morin +make textbook-judson textbook-cantor textbook-demorgan +make textbook-russell-imp textbook-russell-pom +make textbook-laplace textbook-pm textbook-grinstead-snell +make textbook-hilbert textbook-boole textbook-peano +make textbook-dedekind textbook-plfa textbook-sf-lf + +# Title-from-author backfill (one-off SQL — see "Discipline" above +# for the per-shard script) + +# Run resolver +arborist warrant-resolve --use-aliases --write +# → 92 / 92 (100%) under the 18-substrate + 54-alias state +``` + +## References + +- `#000031` — surface-ingest cited textbooks +- `#000041` — citation-aliases table + 54 live rows +- `#000042` — term-aliases table + 13 live rows +- `#000038` — Phase 4 content acquisition (still-blocked + proprietary candidates: Hilbert-Ackermann 1928, Mendelson, + Enderton, Jech, Goldstein, Barendregt, Stanley, Brualdi, Knuth; + the substrate substitution pattern is the workaround) +- `bench/results/full-warrant-resolution-2026-05-10.md` — the + bench journal that closed 84% → 100% +- `bench/fixtures/textbooks/manifest-v1.jsonl` — license-validated + manifest of every textbook in the substrate +- `arborist/qa/warrant_resolver.py` — + `_build_record_query_cascade` + `_phrase_for_axiom` + + `_phrase_from_parenthetical` + `resolve_chunks` +- `arborist/qa/aliases.py` — citation + term alias schema + + CLI add/list/remove