# 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`
