arborist/docs/warrant-substrate-cookbook.md

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:

{"id":"foo","urls":["https://...html"], ...}

Make target: make textbook ID=foo. Calls arborist ingest --source html --urls-from <file>.

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:

{"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:

{"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:

curl -sLo /tmp/foo.pdf https://...
pdftotext -layout /tmp/foo.pdf /tmp/foo.txt
mkdir -p /tmp/serve
{ echo '<html><head><title>...</title></head><body><pre>';
  cat /tmp/foo.txt;
  echo '</pre></body></html>'; } > /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 <title> 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:

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 (74 rows live as of 2026-05-10) + 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:

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.

# 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