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
russell@unturf.com
245fb6ead3