PLFA + SF-LF + PM Vol 1 ingest: 62 -> 68/92 (74%) — pillar IX nearly closed

Three new substrates targeting the lambda-calculus gap (pillar IX
was 5/14 stuck) and the type-theoretic Russell's Paradox Resolution
record (last pillar II straggler):

  PLFA - Programming Language Foundations in Agda
    (Wadler/Kokke/Siek, Edinburgh CS, CC-BY-4.0)
    plfa.github.io BFS depth=2 max=60 -> 58 docs / 413 chunks
    Untyped + simply-typed lambda calculus, Confluence/Church-Rosser,
    progress + preservation, de Bruijn, beta/alpha/eta reduction.

  Software Foundations Vol 1 - Logical Foundations
    (Pierce et al., Penn CIS, MIT-licensed)
    softwarefoundations.cis.upenn.edu/lf-current/ BFS depth=2 max=40
    -> 33 docs / 367 chunks. Coq induction proofs, lambda calculus.

  Whitehead-Russell Principia Mathematica Vol 1
    (1910 Cambridge, PD by age, PG #78050 single-page HTML)
    -> 1 doc / 231 chunks. Preface + intro + chs I-III only;
    formal type theory body (*24 onwards) not transcribed.

Plus 4 new citation-alias rows per #000041 (decision_by="fox 2026-05-10"):
  Barendregt -> PLFA (+5 pillar IX)
  Barendregt -> Software Foundations LF (+1 pillar IX, supplementary)
  Jech       -> PM Vol 1 (cascade miss; 0 lift)
  Landau     -> Software Foundations LF (cascade miss; 0 lift)

Per-pillar:
  IX:  5/14 -> 11/14 (+6 — beta/alpha/eta + Church-Rosser + extensionality + fixed-point)
  Others stable.

Title-haystack hack reverted: initial backfill appended ", Barendregt
substrate" to PLFA + SF docs, which would have let the resolver match
Barendregt citations directly via the haystack (mis-labeling chains
as DIRECT instead of via_alias). Now uses clean citation-alias
substitution; audit trail preserves substitution.

Cumulative day-of-2026-05-10: 18 -> 68 / 92 (+50 records, +54pp).
24 records still stuck. Top blockers:
  - Pillar I formal proof axioms (3) — Hilbert-Ackermann needed
  - Pillar III symbolic-axiom cascade misses (6) — Peano/Dedekind/SF
    have content; FTS5 token cascade doesn't surface
  - Pillar V Kolmogorov axioms (4) — Laplace narrative not enough,
    Kolmogorov 1933 URAA-blocked until 2058
  - Pillar VII advanced identities (5) — Bogart skews intro
  - Pillar IX (3) — Turing/Bohm-Jacopini/Orbit-Stabilizer cascade misses
  - Pillar VI (2) — Newton 1729 vocab mismatch
  - Pillar II Russell's Paradox Resolution (1) — PM Vol 1 *24+ not transcribed

Makefile

@@ -892,6 +892,15 @@ textbook-dedekind: ## Dedekind Essays on the Theory of Numbers 1901 (PD, PG #210
 	$(ARBORIST) --db "$(CRAWL_SHARDS_DIR)/textbook_dedekind-essays-theory-numbers.db" \
 	  ingest --source textbook_tex --url "$$url"
 
+textbook-plfa: ## PLFA - Programming Language Foundations in Agda (CC-BY-4.0)
+	$(MAKE) textbook ID=plfa-wadler-kokke-siek
+
+textbook-sf-lf: ## Software Foundations Vol 1 Logical Foundations (MIT, Pierce et al.)
+	$(MAKE) textbook ID=sf-pierce-logical-foundations
+
+textbook-pm: ## Whitehead-Russell Principia Mathematica Vol 1 (PD, PG #78050 — preface+intro only)
+	$(MAKE) textbook ID=whitehead-russell-pm-vol1-1910
+
 test-crawler: bootstrap-crawler ## run only the lifted crawler tests
 	$(VENV)/bin/pytest -q tests/crawler
 

bench/fixtures/textbooks/manifest-v1.jsonl

@@ -18,3 +18,6 @@
 {"id":"russell-pom-1903","title":"The Principles of Mathematics","author":"Bertrand Russell (Klement HTML typesetting 2024)","year":"1903 (orig.); 2024 (Klement HTML reformat)","license":"CC-BY-SA-4.0","license_url":"https://creativecommons.org/licenses/by-sa/4.0/","domain":"logic-foundations","pillar_targets":["I","II"],"urls":["https://people.umass.edu/klement/pom/pom.html"],"home_url":"https://people.umass.edu/klement/pom/","notes":"Kevin C. Klement's HTML typesetting of Russell's 1903 *Principles of Mathematics*. Russell's text is PD (1903 + URAA expired); Klement's typesetting is CC-BY-SA-4.0. Single-page HTML (~25K lines / ~1MB). Russell PoM is more class-theoretic and ZFC-foundational than IMP 1919 (PoM was the precursor to Principia Mathematica). Pillar I/II coverage extension: contains Russell's Paradox derivation, class theory, relations, magnitudes — what IMP and PM leave for the technical reader. Cited by claim-pack as Mendelson/Enderton substrate."}
 {"id":"laplace-philosophical-essay-probabilities","title":"A Philosophical Essay on Probabilities","author":"Pierre-Simon Laplace (Truscott + Emory transl. 1902)","year":"1814 (French orig.); 1902 (English Truscott-Emory)","license":"PD","license_url":"https://en.wikipedia.org/wiki/Public_domain","domain":"probability","pillar_targets":["V"],"urls":["https://www.gutenberg.org/cache/epub/58881/pg58881-images.html"],"home_url":"https://www.gutenberg.org/ebooks/58881","notes":"PG eBook #58881, single-page HTML. Laplace 1814 *Essai philosophique sur les probabilités* is the foundational popular treatise on probability — predates Kolmogorov 1933 by 119 years but covers expected value, conditional probability, additive law, large-numbers reasoning, applications to natural philosophy. PD by age (Truscott-Emory English 1902 = pre-1929 US PD). Pillar V substrate; Kolmogorov 1933 axiomatizes what Laplace introduces narratively."}
 {"id":"dedekind-essays-theory-numbers","title":"Essays on the Theory of Numbers (I. Continuity and irrational numbers, II. The nature and meaning of numbers)","author":"Richard Dedekind (Wooster Woodruff Beman, transl. 1901)","year":"1872 + 1888 (German orig.); 1901 (English Beman)","license":"PD","license_url":"https://en.wikipedia.org/wiki/Public_domain","domain":"arithmetic","pillar_targets":["III"],"urls":[],"home_url":"https://www.gutenberg.org/ebooks/21016","tex_url":"https://www.gutenberg.org/files/21016/21016-t/21016-t.tex","notes":"PG eBook #21016 — TeX-only (no HTML edition); ingest via textbook_tex pipeline (proven against Hilbert + Boole + Peano). Dedekind is the OTHER pillar III primary alongside Peano: 'Was sind und was sollen die Zahlen?' (1888) introduced the chains-and-induction definition of natural numbers; 'Stetigkeit und irrationale Zahlen' (1872) is the cuts construction of the reals. Beman 1901 English. PD by age. Closes the induction / completeness side of Landau citations that Peano alone misses."}
+{"id":"plfa-wadler-kokke-siek","title":"Programming Language Foundations in Agda","author":"Philip Wadler, Wen Kokke, Jeremy G. Siek","year":"2018+ (continuously revised)","license":"CC-BY-4.0","license_url":"https://creativecommons.org/licenses/by/4.0/","domain":"lambda-calculus","pillar_targets":["IX"],"urls":[],"home_url":"https://plfa.github.io/","crawl_url":"https://plfa.github.io/","crawl_depth":2,"crawl_max":60,"notes":"Open-source Agda + lambda calculus textbook from University of Edinburgh; CC-BY-4.0 explicit. Covers introduction to lambda calculus, untyped lambda calculus with full normalisation, Confluence/Church-Rosser, simply-typed lambda calculus, properties (progress + preservation), de Bruijn representation. Pillar IX substrate for the 7-record Barendregt block (β/α/η-conversion, Church-Rosser theorem, fixed-point, Turing completeness)."}
+{"id":"sf-pierce-logical-foundations","title":"Software Foundations Volume 1: Logical Foundations","author":"Benjamin C. Pierce et al. (Penn)","year":"2007+ (continuously revised)","license":"MIT","license_url":"https://opensource.org/licenses/MIT","domain":"logic-foundations","pillar_targets":["I","III","IX"],"urls":[],"home_url":"https://softwarefoundations.cis.upenn.edu/lf-current/","crawl_url":"https://softwarefoundations.cis.upenn.edu/lf-current/toc.html","crawl_depth":2,"crawl_max":40,"notes":"Coq-based open textbook on logical foundations of programming languages from UPenn; MIT-licensed (verified against included LICENSE file in lf-current/lf.tgz). Covers basic functional programming, induction, lists, polymorphism + higher-order functions, propositional logic, indexed propositions, total + partial relations, lambda calculus, simply-typed lambda calculus. Pillar III substrate (induction primary) + pillar IX substrate (lambda calculus). Caveat: heavy Coq syntax; the prose-to-code ratio is lower than PLFA."}
+{"id":"whitehead-russell-pm-vol1-1910","title":"Principia Mathematica, Volume 1 (Preface + Introduction + Chapters I-III)","author":"Alfred North Whitehead + Bertrand Russell","year":"1910 (Cambridge)","license":"PD","license_url":"https://en.wikipedia.org/wiki/Public_domain","domain":"logic-foundations","pillar_targets":["I","II"],"urls":["https://www.gutenberg.org/cache/epub/78050/pg78050-images.html"],"home_url":"https://www.gutenberg.org/ebooks/78050","notes":"PG eBook #78050, single-page HTML — Volume 1 Preface + Introduction + Chapters I-III only (~20-25% of full Vol 1; the *1 through *97 numbered propositions / type theory formalization not in this excerpt). Includes discussion of paradox resolution + theory of types in narrative form. Pillar I/II — supplementary substrate; the formal type-theoretic Russell's Paradox Resolution lives in the missing body, but the conceptual treatment is here. PD by age (1910 + URAA = 95 years = 2005)."}

bench/results/lambda-and-pm-additions-2026-05-10.md

@@ -0,0 +1,133 @@
+# PLFA + Software Foundations + PM Vol 1 ingest — 2026-05-10
+
+**Date:** 2026-05-10 (UTC)
+**Author:** blackops + fox
+**Method:** added 3 more substrates targeting the lambda-calculus
+gap (pillar IX) + the type-theoretic Russell's Paradox Resolution
+record (pillar II), under fox's "yes, continue" directive.
+
+## Headline
+
+**62 → 68 / 92 records resolve (+6, 74% coverage).** Pillar IX
+nearly closed; PLFA + Software Foundations between them caught all
+the β/α/η-conversion + Church-Rosser + extensionality + fixed-point
+records.
+
+| Pillar | Pre-turn | Post-turn |
+|---|---|---|
+| I (logic) | 10/13 | 10/13 |
+| II (set theory) | 9/10 | 9/10 |
+| III (arithmetic) | 7/13 | 7/13 |
+| IV (geometry) | 18/18 | 18/18 |
+| V (probability) | 1/5 | 1/5 |
+| VI (classical phys) | 3/5 | 3/5 |
+| VII (combinatorics) | 9/14 | 9/14 |
+| IX (lambda + algebra) | 5/14 | **11/14** |
+| **Total** | **62/92 (67%)** | **68/92 (74%)** |
+
+## Three new ingests
+
+### PLFA — Programming Language Foundations in Agda
+
+- Manifest `id: plfa-wadler-kokke-siek`, license `CC-BY-4.0`
+- Author: Philip Wadler, Wen Kokke, Jeremy G. Siek (Edinburgh CS)
+- Source: `https://plfa.github.io/` (BFS depth=2 max=60)
+- Landed: **58 docs / 413 chunks**
+- Coverage: untyped lambda calculus, Confluence/Church-Rosser,
+  simply-typed lambda calculus, properties (progress + preservation),
+  de Bruijn representation, β/α/η reduction. Pillar IX core.
+
+### Software Foundations Vol 1 — Logical Foundations
+
+- Manifest `id: sf-pierce-logical-foundations`, license `MIT`
+  (verified against `lf-current/lf.tgz` LICENSE file)
+- Author: Benjamin C. Pierce et al. (Penn CIS)
+- Source: `https://softwarefoundations.cis.upenn.edu/lf-current/toc.html`
+  (BFS depth=2 max=40)
+- Landed: **33 docs / 367 chunks**
+- Coverage: Coq induction proofs, lists, polymorphism, propositional
+  logic, lambda calculus, simply-typed lambda calculus. Pillar III
+  + IX dual substrate.
+
+### Whitehead-Russell *Principia Mathematica* Volume 1
+
+- Manifest `id: whitehead-russell-pm-vol1-1910`, license `PD`
+- Source: PG eBook #78050 single-page HTML
+- Landed: **1 doc / 231 chunks**
+- Coverage: Preface + Introduction + Chapters I-III only (~20-25%
+  of full Vol 1). The *1-*97 numbered propositions / formal type
+  theory not in this excerpt; narrative discussion of paradox + types
+  is. Pillar II — supplementary substrate for Russell's Paradox
+  Resolution citation.
+
+## Four new citation aliases (decision_by="fox 2026-05-10")
+
+| Original | Substitute | Records lifted |
+|---|---|---|
+| Barendregt — Lambda Calculus Syntax & Semantics | PLFA (Wadler/Kokke/Siek) | +5 |
+| Barendregt — Lambda Calculus Syntax & Semantics | Software Foundations LF (Pierce) | +1 |
+| Jech — Set Theory | Whitehead-Russell PM Vol 1 | 0 (cascade miss) |
+| Landau — Foundations of Analysis | Software Foundations LF (Pierce) | 0 (cascade miss) |
+
+## Title-haystack hack reverted
+
+Initial title backfill on PLFA + SF-LF appended `, Barendregt
+substrate` to document titles — a haystack hack that would let the
+resolver match Barendregt citations DIRECTLY against PLFA without
+the alias mechanism, masking the substitution as DIRECT in audit
+logs. Reverted to clean alias-driven matching: aliases register the
+substitution explicitly, audit trail preserves who/why, and the
+shard's title carries only its actual author signature
+(`Wadler Kokke Siek` / `Pierce et al.`).
+
+## Honest gaps remaining (24 records)
+
+| Pillar | Stuck | Blocker |
+|---|---|---|
+| I (3) | Existential Introduction, Vacuous Quantification, Double Negation Elimination | natural-deduction proof-theory; Hilbert-Ackermann 1928 would close (no PD HTML found) |
+| II (1) | Russell's Paradox Resolution | PM Vol 1 PG #78050 has only intro material; *24 onward (formal types) not transcribed |
+| III (6) | Axiom of Zero / Distinctness / Injectivity of Successor / Induction Schema / Commutativity / Distributivity | Peano + Dedekind + SF-LF cascades all miss; symbolic axioms vs prose-keyword cascade mismatch |
+| V (4) | Kolmogorov 3 axioms + Inclusion-Exclusion | Laplace 1814 doesn't axiomatize σ-algebras; Kolmogorov 1933 itself URAA-blocked until 2058 |
+| VI (2) | Newton's Third Law, Conservation of Momentum | 1729 vocab mismatch; term-aliases registered but cascade tokens miss |
+| VII (5) | Empty-Set/Boundary, Hockey-Stick, Vandermonde, Catalan, Stars-and-Bars | Bogart skews intro; advanced enumerative identities not named |
+| IX (3) | Turing Completeness of λ-Calculus, Böhm-Jacopini Theorem, Orbit-Stabilizer | Turing/Böhm not in PLFA core; Orbit-Stabilizer cascade miss in Judson |
+
+## Cumulative session — 2026-05-10
+
+| Snapshot | Resolved | % | Drivers |
+|---|---|---|---|
+| Start | 18/92 | 20% | Hilbert pillar IV only |
+| 3 high-conf aliases | 33/92 | 36% | Goldstein/Newton, Stanley/Bogart, Dummit-Foote/Judson |
+| Newton recrawl | 35/92 | 38% | deeper Principia text |
+| 7 medium-conf aliases | 39/92 | 42% | Mendelson/Enderton/Jech/Landau |
+| Peano + title backfill | 54/92 | 59% | Peano + author-surname haystack fix |
+| 3 new textbooks (Russell PoM + Laplace + Dedekind) | 62/92 | 67% | pillar I/II jumped |
+| **PLFA + SF-LF + PM Vol 1** | **68/92** | **74%** | **this turn — pillar IX** |
+
+**Day's lift: +50 records absolute (+54 pp).**
+
+## Reproducibility
+
+```bash
+make textbook-plfa     # CC-BY-4.0 BFS crawl, ~58 docs
+make textbook-sf-lf    # MIT BFS crawl, ~33 docs
+make textbook-pm       # PG #78050 single-page HTML
+arborist warrant-resolve --use-aliases --write
+# → 68 / 92 (74%)
+```
+
+## References
+
+- `#000041` — citation-aliases mechanism (19 rows live total)
+- `#000042` — term-aliases mechanism (6 rows live total)
+- `#000031` — surface-ingest cited textbooks; Phase 1 follow-up
+  (source-side title-from-author backfill) deferred
+- `#000038` — Phase 4 content acquisition; remaining acquisition
+  candidates without HTML editions: Hilbert-Ackermann 1928,
+  Whitehead-Russell PM Vol 1 *24-*97 (full), Kolmogorov 1933
+  (URAA-blocked)
+- Today's bench journals (chronological):
+  - `bench/results/citation-aliases-batch-2026-05-10.md`
+  - `bench/results/medium-confidence-aliases-and-peano-2026-05-10.md`
+  - `bench/results/three-more-textbooks-2026-05-10.md`
+  - this file: `bench/results/lambda-and-pm-additions-2026-05-10.md`