# Grinstead-Snell ingest + cascade tuning batch — 2026-05-10

**Date:** 2026-05-10 (UTC)
**Author:** blackops + fox
**Method:** under fox's "work all paths" directive: 6 Gödel
multi-substitute aliases, 14 Levin pillar-VII aliases, 2 Mendelson/
Enderton → SF-LF aliases, 7 term aliases (physics + arithmetic),
and Grinstead-Snell ingest via PDF→localhost-HTML pipeline (deep
LibreTexts crawl was too thin).

## Headline

**68 → 77 / 92 records resolve (+9, 84% coverage).** Pillar III went
from 7/13 → 11/13 (+4 from Gödel multi-substitutes), pillar VII 9/14
→ 11/14 (+2 from Levin), pillar I 10/13 → 12/13 (+2 from SF-LF), and
pillar V 1/5 → 2/5 (+1 Inclusion-Exclusion via Grinstead-Snell).

| Pillar | Pre-turn | Post-turn |
|---|---|---|
| I (logic) | 10/13 | **12/13** |
| II (set theory) | 9/10 | 9/10 |
| III (arithmetic) | 7/13 | **11/13** |
| IV (geometry) | 18/18 | 18/18 |
| V (probability) | 1/5 | **2/5** |
| VI (classical phys) | 3/5 | 3/5 |
| VII (combinatorics) | 9/14 | **11/14** |
| IX (lambda + algebra) | 11/14 | 11/14 |
| **Total** | **68/92 (74%)** | **77/92 (84%)** |

## Changes landed

### 14 Levin alias rows for pillar VII

Each compound Stanley/Brualdi/Knuth source_ref now has BOTH `Bogart
CTGD` and `Levin Discrete Mathematics` as substitutes. Levin's
chapter on "Stars and Bars" + "Hockey Stick Identity" + "Inclusion-
Exclusion" covers the intermediate combinatorics Bogart skips.

### 6 Gödel alias rows (3 per Gödel variant × 2 variants)

Each Gödel citation variant now has 4 substitutes total:
- Peano *Arithmetices Principia*
- Russell IMP 1919
- Dedekind *Essays*
- Software Foundations LF

This unblocked the 6 stuck pillar III records that cite Gödel
(Axiom of Zero, Distinctness of Zero, etc.).

### 2 SF-LF alias rows for pillar I formal proof

Mendelson + Enderton → SF-LF. SF Logic.v has 12 hits on "excluded
middle", 1 on "double negation", 40 on "existential" — coverage of
the natural-deduction axioms Russell IMP/Boole/De Morgan leave
informal. Lifted Existential Introduction + Double Negation
Elimination.

### 7 term aliases (classical-physics + arithmetic)

- `third law ↔ lex tertia` (geometry didn't lift; Newton 1729 doesn't use Roman numeral consistently)
- `action reaction ↔ every action` (didn't lift; cascade tokens don't include this phrase)
- `axiom of zero ↔ zero is a number` (didn't lift; cascade strips "axiom of")
- `axiom of successor ↔ successor of every` (didn't lift)
- `axiom schema of induction ↔ principle of induction` (didn't lift)
- `injectivity of successor ↔ two different numbers` (didn't lift)
- `distinctness of zero ↔ zero is not the successor` (didn't lift)

Term aliases registered for completeness but most didn't lift —
cascade is picking different tokens than my aliases target. Cascade
tuning would require code work in `_phrase_for_axiom` /
`_content_tokens` / `_build_record_query_cascade`.

### Grinstead-Snell *Introduction to Probability* ingest

GFDL-licensed Dartmouth CHANCE Project textbook. Initial LibreTexts
BFS crawl produced thin content (24 chunks of navigation skeleton
only — depth=2/max=40 didn't reach chapter pages). Switched to
Dartmouth PDF (math.dartmouth.edu/~prob/prob/prob.pdf): 25K-line
text via `pdftotext -layout`, served as single-page HTML on
localhost:8765, ingested via standard `arborist ingest --source
html`. Result: **1 doc / 339 chunks** of substantive probability
content.

This is a new pattern — PDF→localhost-HTML→html-source — useful
when a textbook has a PDF but no clean HTML edition (Bayes 1763
Royal Society scan, Frege Begriffsschrift, etc. could follow same
path).

## Honest gaps remaining (15 records)

| Pillar | Stuck (count) | Notes |
|---|---|---|
| I (1) | Vacuous Quantification | natural-deduction axiom; SF-LF MAY have it but cascade misses |
| II (1) | Russell's Paradox Resolution | PM Vol 1 *24+ formal types not in PG #78050 |
| III (2) | Injectivity of Successor, Distributivity | Peano + Dedekind + SF have content; cascade tokens not aligned |
| V (3) | Kolmogorov 3 axioms (Non-Negativity, Normalization, Additivity) | Grinstead-Snell HAS the content (339 chunks); cascade phrase doesn't include "kolmogorov" or "axiom" tokens |
| VI (2) | Newton's Third Law, Conservation of Momentum | Newton 1729 vocab; term-aliases registered but cascade misses |
| VII (3) | Empty-Set/Boundary, Vandermonde, Catalan | Bogart + Levin have content; cascade-token miss |
| IX (3) | Turing Completeness, Böhm-Jacopini, Orbit-Stabilizer | Turing/Böhm not in PLFA/SF core; Judson cascade miss for Orbit-Stabilizer |

**Pattern:** the remaining 15 records mostly have content in already-
ingested shards but the FTS5 cascade picks different discriminator
tokens than what the substrate text uses. The fix is cascade tuning
in `_build_record_query_cascade` — particularly less aggressive
title-stripping in `_phrase_for_axiom` and smarter content-token
ranking. Code work, not new ingest.

## Cumulative session — 2026-05-10

| Snapshot | Resolved | % |
|---|---|---|
| Start | 18/92 | 20% |
| 3 high-conf aliases | 33/92 | 36% |
| Newton recrawl | 35/92 | 38% |
| 7 medium-conf aliases | 39/92 | 42% |
| Peano + title backfill | 54/92 | 59% |
| Russell PoM + Laplace + Dedekind | 62/92 | 67% |
| PLFA + SF-LF + PM Vol 1 | 68/92 | 74% |
| **+ Levin + Gödel multi + Grinstead-Snell + cascade-tune attempts** | **77/92** | **84%** |

**Day's lift: 18 → 77 (+59 records, +64 pp absolute).**

## New tools in toolbox

1. **PDF→localhost-HTML→html-source ingest path** — proven on
   Grinstead-Snell. Reusable for any textbook with a PDF but no
   HTML edition.
2. **Multi-substitute aliases per source_ref** — register N
   substitutes per original; resolver tries all, audit trail
   records each independently. Used for Mendelson (3 subs),
   Gödel (4 subs).
3. **Title-haystack backfill discipline** — every new shard needs
   a SQL UPDATE to ensure cited-author surname appears in document
   titles for `_shard_matches_citation` to find it.

## References

- 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`
  - `bench/results/lambda-and-pm-additions-2026-05-10.md`
  - this file: `bench/results/grinstead-snell-and-cascade-tuning-2026-05-10.md`
- `#000041` — citation-aliases (39 rows now live)
- `#000042` — term-aliases (13 rows now live, several unused)
- `#000031` — surface-ingest cited textbooks; Phase 1 follow-up
  (source-side title-from-author) and Phase 3 (cascade tuning for
  symbolic-axiom records) both surfaced this turn
