docs/warrant-substrate-cookbook.md: architecture reference for 18-substrate map

Internal architecture reference written 2026-05-10 after the day's
18/92 -> 92/92 push under #000031. Covers:

  - per-pillar substrate map (which open textbook covers which
    pillar; license + ingest path for each of the 18 substrates)
  - five proven ingest patterns (HTML single-URL, HTML BFS,
    textbook_tex LaTeX-source, PDF -> localhost-HTML, direct
    Python API)
  - discipline patterns: title-from-author backfill workaround
    (until the source-side fix in #000031 Phase 1 lands), alias
    audit-fail-closed (decision_by + decision_rationale per row),
    multi-substitute pattern, cascade tuning
  - honest tier breakdown of the 92 chains (~25 direct primary,
    ~50 substrate substitution, ~17 soft-fallback OR-of-3 match)
  - what the substrate doesn't yet do (render layer doesn't read
    derivations, process_id under-attributes alias chains as DIRECT,
    no per-record tier classification in the schema)
  - re-running steps for future shifts (idempotent at DB layer)

Format follows other docs/ references (cti-architecture,
concept-relations-design, tool-action-dag-design) — describes
state of the world, not proposing change.

CLAUDE.md and TICKETS.md updated to point at the cookbook from
the docs index.

No undefect/whitepaper publication — this stays internal as
requested. Future blackops shifts re-discovering the substrate
map shouldn't have to walk five bench journals.
This commit is contained in:
russell@unturf.com 2026-05-10 08:50:40 -04:00
parent e82968baad
commit 4d4e4d4249
No known key found for this signature in database
3 changed files with 446 additions and 0 deletions

View file

@ -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:

View file

@ -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.

View file

@ -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 <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:
```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 '<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:
```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