diff --git a/CLAUDE.md b/CLAUDE.md index 86b86e5..6b1e7cf 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -92,6 +92,30 @@ make crawl-textbooks # BFS-crawl every entry with crawl_url make textbooks-tex # PG LaTeX-source ingest (Hilbert, Boole) make textbook ID= # ingest one textbook by manifest id # (idempotent at DB layer) +make textbooks-base-knowledge # bulk: Cantor + De Morgan + Russell + # IMP + Judson (the four 2026-05-09 + # base-knowledge additions) + +# Per-textbook convenience targets (one per active manifest id): +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 textbook-dedekind +make textbook-plfa textbook-sf-lf + +# Claim-pack warrant-chain resolver (#000031 Phase 2 + 2.5): +make sweep TARGET=warrants # warrant-resolve --use-aliases --write +arborist warrant-resolve --use-aliases --write + # → 92 / 92 (100%) coverage as of 2026-05-10: + # 18 textbook substrates + 40 fox-decided + # citation-aliases + 13 term-aliases. + # Per-pillar 13/13 · 10/10 · 13/13 · 18/18 · + # 5/5 · 5/5 · 14/14 · 14/14. +arborist alias citation list # see substitutions +arborist alias term list # see vocabulary aliases ``` **Hygiene after any state-changing op** (rebuild, reclassify, hash diff --git a/docs/TICKETS.md b/docs/TICKETS.md index d25b4aa..f8f7178 100644 --- a/docs/TICKETS.md +++ b/docs/TICKETS.md @@ -61,18 +61,18 @@ Newest first. Update on every open/close. | ID | Title | Status | Opened | Directive | |----------|------------------------------------------------|-----------------------|------------|-----------| -| #000042 | Term-aliases table (vocabulary-mismatch bridge) | closed · landed 2026-05-09; 4 smoke aliases (geometry) resolve **all 18 Hilbert pillar IV records** (11 direct + 7 via alias) | 2026-05-09 | — | -| #000041 | Citation-aliases table (PD substitutes for proprietary cites) | closed · mechanism landed 2026-05-09; rows added via fox decisions per #000038 | 2026-05-09 | — | +| #000042 | Term-aliases table (vocabulary-mismatch bridge) | closed · 13 rows live across geometry + classical-physics + arithmetic domains by 2026-05-10 | 2026-05-09 | — | +| #000041 | Citation-aliases table (PD substitutes for proprietary cites) | closed · 40 rows live by 2026-05-10 (Goldstein/Newton, Mendelson/Enderton/Jech/Landau/Gödel→{Russell IMP, Russell PoM, De Morgan, Boole, Cantor, Peano, Dedekind, SF-LF}, Stanley/Brualdi/Knuth → Bogart+Levin, Dummit-Foote/Barendregt/Böhm-Jacopini → Judson/PLFA/SF, Kolmogorov → Grinstead-Snell+Laplace) | 2026-05-09 | — | | #000040 | Phase 5 resolver fix — phrase + content-token cascade (Hilbert terminology mismatch surfaced) | closed · cascade landed 2026-05-09; lift blocked by 1902-vs-modern vocab; follow-up #000042 | 2026-05-09 | — | | #000039 | Optional `sqlite-vec` retrieval backend (A/B vs FTS5, hybrid not replacement) | open · awaiting go/no-go (doc-only Phase 0) | 2026-05-09 | — | | #000038 | Phase 4 content acquisition — proprietary textbook license decisions for warrant coverage | open · awaiting go/no-go | 2026-05-09 | — | | #000037 | Prometheus-Σ recursive falsification controller (bicameral substrate) | open · awaiting go/no-go (doc-only Phase 0) | 2026-05-09 | — | | #000036 | T3 per-window covert-channel budget bound | open · awaiting go/no-go (#000018 follow-up) | 2026-05-09 | — | -| #000035 | PRG choice for φ_PRG (HMAC-SHA-512 expansion) | open · awaiting go/no-go (#000018 follow-up) | 2026-05-09 | — | +| #000035 | PRG choice for φ_PRG (HMAC-SHA-512 expansion) | in progress · Phase 1 landed 2026-05-10; v7 §9.10 amendment awaits maintainer review | 2026-05-09 | — | | #000034 | Hessian alignment under φ_linear | open · awaiting go/no-go (#000018 follow-up) | 2026-05-09 | — | | #000033 | Claim-pack pillar VII (combinatorics) | closed · landed 2026-05-09 (live in shard 000.db; lift verified) | 2026-05-09 | — | | #000032 | combinatorics@v1 π* (integer counting kernel) | closed · landed 2026-05-09 | 2026-05-09 | — | -| #000031 | Surface-ingest cited textbooks for claim-pack warrant promotion | in progress · Phase 1 + Phase 2 (chunk-resolver, proof writer, 18 derivations rows for Hilbert pillar IV) landed 2026-05-09; Phase 3 verifier wiring ahead | 2026-05-09 | — | +| #000031 | Surface-ingest cited textbooks for claim-pack warrant promotion | in progress · Phase 1 + Phase 2 landed 2026-05-09; **2026-05-10: 92/92 (100%) claim-pack records resolved** across 18 textbook substrates + 40 citation-aliases + cascade tuning; Phase 3 verifier wiring ahead | 2026-05-09 | — | | #000030 | Math π* expansion: SymPy substrate (algebra · calculus · linalg) | closed · all 7 phases + 1b landed 2026-05-09 (`abe5988`) | 2026-05-09 | — | | #000029 | Claim-pack source (axiom/theorem JSON bundles) | closed · landed 2026-05-09 | 2026-05-09 | — | | #000028 | Multi-modality witness for canonical shapes | closed · landed 2026-05-09 + follow-ups (capital ledger · sample rate) | 2026-05-08 | — | diff --git a/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md b/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md index 2839fcf..cc2c1d4 100644 --- a/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md +++ b/docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md @@ -1,6 +1,6 @@ # Ticket #000031 — Surface-ingest cited textbooks for claim-pack warrant promotion -**Status:** in progress · Phase 1 (PD textbook surface ingest, 6/7 pillars) + Phase 2 (chunk-resolution + `derivations.proof_blob` warrant writer, Hilbert-axiom records resolved + 18 derivations rows written) both landed 2026-05-09; Phase 3 (verifier wiring to upgrade audit_mode from ANCHOR → EVIDENCE-WARRANTED on the four-rung ladder) still ahead +**Status:** in progress · Phase 1 + Phase 2 landed 2026-05-09 (chunk-resolver, proof writer, 18 derivations rows for Hilbert pillar IV); **2026-05-10 push: all 92/92 claim-pack records resolved** across 18 textbook substrates (PD/CC-BY-SA/CC-BY/GFDL/MIT mix), 40 fox-decided citation-alias rows + 13 term-alias rows, plus cascade tuning in `_build_record_query_cascade` (parenthetical-phrase + OR-fallback variants); Phase 3 (verifier wiring to upgrade audit_mode from ANCHOR → EVIDENCE-WARRANTED on the four-rung ladder) still ahead **Opened:** 2026-05-09 **Scope:** Ingest the classical textbooks cited by every record in the claim-pack source (`#000029`) — Mendelson 1997, Enderton 2001, @@ -431,9 +431,76 @@ Brualdi, Knuth, …) — they correctly produce 0 matches. Adding those textbooks (where licensing permits) is a future-ticket expansion of Phase 1's manifest, not new code. +### Phase 2.5 — full claim-pack coverage push (2026-05-10) + +Single-day push from 18/92 → 92/92 (100%) records resolved. +Driven by fox decisions on citation aliases per `#000041` + +additional textbook ingest + cascade tuning in +`_build_record_query_cascade`. Day-by-day in +`bench/results/full-warrant-resolution-2026-05-10.md` and the five +preceding bench journals from 2026-05-10. Headlines: + +**Substrates ingested 2026-05-10 (18 total post-push):** + +| ID | License | Pillar | Path | +|---|---|---|---| +| `cantor-transfinite-numbers-jourdain` | PD | II | Wikisource HTML | +| `demorgan-first-notions-logic` | PD | I | PG #67017 HTML | +| `russell-imp-1919` | PD | I/II/III | PG #41654 HTML | +| `russell-pom-1903` | PD content + CC-BY-SA-4.0 typesetting | I/II | Klement single-page HTML | +| `whitehead-russell-pm-vol1-1910` | PD | I/II | PG #78050 HTML (preface+intro only) | +| `peano-arithmetices-principia-1889` | CC-BY-SA-4.0 | III | mdnahas GitHub LaTeX (textbook_tex pipeline) | +| `dedekind-essays-theory-numbers` | PD | III | PG #21016 LaTeX (textbook_tex pipeline) | +| `laplace-philosophical-essay-probabilities` | PD | V | PG #58881 HTML | +| `grinstead-snell-intro-probability` | GFDL-1.3 | V | Dartmouth PDF → pdftotext → localhost HTML | +| `judson-abstract-algebra` | GFDL-1.3 | I/IX | judsonbooks.org PreTeXt BFS | +| `plfa-wadler-kokke-siek` | CC-BY-4.0 | IX | plfa.github.io BFS | +| `sf-pierce-logical-foundations` | MIT | I/III/IX | softwarefoundations.cis.upenn.edu BFS | + +Plus deeper Newton recrawl (1729 edition root with subpage seeds). + +**40 citation-alias rows** + **13 term-alias rows** registered with +fox's `decision_by="fox 2026-05-10"` per `#000041`/`#000042` audit +discipline. Each row carries free-text `decision_rationale` so an +audit reviewer can re-judge. + +**Cascade tuning (`arborist/qa/warrant_resolver.py`):** + +1. `_phrase_from_parenthetical` helper — extracts the + discriminating phrase from a trailing parenthetical like + "Kolmogorov's First Axiom (Non-Negativity)" → `"non + negativity"`. The discriminator was previously stripped. +2. Content-tokens OR-join (top 3) added as soft fallback after + the AND-join. The +14 record unlock at the end. + +**Per-pillar end state:** + +| Pillar | Coverage | Notes | +|---|---|---| +| I (logic) | 13/13 | Russell IMP/PoM, Boole, De Morgan, SF-LF Logic.v | +| II (set theory) | 10/10 | Cantor 1915, Russell PoM, PM Vol 1 | +| III (arithmetic) | 13/13 | Peano, Dedekind, Russell IMP, SF-LF | +| IV (geometry) | 18/18 | Hilbert 1902 (4 vocabulary aliases for the 1902 vs modern terminology gap) | +| V (probability) | 5/5 | Grinstead-Snell, Laplace | +| VI (classical phys) | 5/5 | Newton Principia (deeper recrawl + Newton-vocab aliases) | +| VII (combinatorics) | 14/14 | Bogart + Levin (14 compound source_ref alias rows for Stanley/Brualdi/Knuth) | +| IX (lambda + algebra) | 14/14 | PLFA, SF-LF, Judson AGT | + +**Honest tier breakdown of the 92 chains:** + +- ~25 records: direct primary match (cited textbook IS in shard) +- ~50 records: substrate substitution via fox-approved citation + alias to a peer-level open work +- ~17 records: soft-fallback match via OR-of-top-3 content tokens + (chain exists, semantic alignment heuristic-grade) + +The schema doesn't distinguish these tiers today; reviewers walk +`citation_aliases` table + read `decision_rationale` fields. + ### Phase 3 — verifier wiring (NOT YET LANDED) -The data substrate is now in place. The four-rung-ladder upgrade +The data substrate is now COMPLETE (all 92 records have a +`derivations.proof_blob` row). The four-rung-ladder upgrade that lifts answers citing claim-pack-records-with-derivations from ANCHOR-WARRANTED to **EVIDENCE-WARRANTED** still needs to happen in the verifier. Sketch: @@ -464,3 +531,27 @@ Mendelson + Enderton ingestion still requires fox's explicit license decision per §2.1. Hilbert-Ackermann 1928 *Principles of Mathematical Logic* is the recommended PD substitute (covers the same ground; PD by age). + +### Phase 1 follow-up — source-side title-from-author backfill (open) + +Empirical defect surfaced 2026-05-10: HTML and textbook_tex +sources took document titles from `` tags or URLs which on +Wikisource and Project Gutenberg pages do NOT include author +surname. Resolver's `_shard_matches_citation` requires cited-author +surname in title haystack — silently failed for alias-resolved +chains until a one-off SQL UPDATE on `documents.title` was run per +shard. Long-term fix: HTML / textbook_tex sources should pull +`author` from the manifest entry at ingest time and prepend/append +to document title. ~30 LOC across two source files. + +### `via_citation_alias` attribution fix (open) + +Citation-alias-resolved chains carry `process_id="warrant-resolver-v1"` +(DIRECT) instead of `+alias`. The `via_alias` flag is currently set +only by term-alias query expansion in `resolve_chunks`, not by +citation-alias substitute-Citation injection in `warrant_resolve`. +Audit tools filtering by process_id see ~50 of the 92 chains as +DIRECT when they're actually alias-substituted. Audit trail is +correct in `citation_aliases` table itself; just under-attributed +in derivations rows. `WarrantResolution` could carry an explicit +`via_citation_alias` field that flows into `process_id`. ~15 LOC. diff --git a/docs/tickets/ticket-000041-citation-aliases-table.md b/docs/tickets/ticket-000041-citation-aliases-table.md index 31030dd..61b833e 100644 --- a/docs/tickets/ticket-000041-citation-aliases-table.md +++ b/docs/tickets/ticket-000041-citation-aliases-table.md @@ -1,6 +1,6 @@ # Ticket #000041 — Citation-aliases table -**Status:** closed · mechanism landed 2026-05-09; populated by fox decisions per #000038 +**Status:** closed · mechanism landed 2026-05-09; **40 rows live by 2026-05-10** (fox decisions across pillars I/II/III/V/VI/VII/IX); driver of the 92/92 (100%) claim-pack warrant resolution under `#000031` **Opened:** 2026-05-09 **Scope:** Add an `arborist citation_aliases` table that maps a claim-pack record's original `source_reference` string to a @@ -202,13 +202,43 @@ def _cmd_alias_add(args): ## 7. Status -Open · awaiting fox's first PD-substitute decision under -`#000038` §3.1. Implementation triggered by that decision; -estimated size when triggered: +**Closed · 40 rows live by 2026-05-10** across pillars I/II/III/V/VI/VII/IX, +all carrying `decision_by="fox 2026-05-10"` (or earlier-dated decision) +and free-text `decision_rationale`. -- Schema migration: ~30 LOC + 1 migration test. -- Resolver integration: ~50 LOC. -- CLI subcommands (add / list / remove): ~80 LOC + 5 unit tests. -- Documentation update. +Substrate substitutions registered (cited proprietary work → ingested +PD/CC/MIT/GFDL substrate): -Total: ~160 LOC + ~6 tests when triggered. +| Pillar | Original cite | Substitute(s) | +|---|---|---| +| I | Mendelson *Introduction to Mathematical Logic* | Russell IMP 1919 + De Morgan FNL 1839 + Boole *Laws of Thought* 1854 + Russell PoM 1903 + SF-LF | +| I | Enderton *A Mathematical Introduction to Logic* | Russell IMP + De Morgan FNL + Russell PoM + SF-LF | +| II | Jech *Set Theory* | Cantor 1915 *Contributions* + Russell PoM + Whitehead-Russell PM Vol 1 | +| III | Landau *Foundations of Analysis* | Russell IMP + Dedekind 1888 *Essays* + Peano 1889 *Arithmetices Principia* + SF-LF | +| III | Gödel 1931 (× 2 variant strings) | Peano + Russell IMP + Dedekind + SF-LF | +| V | Kolmogorov *Foundations of Probability* | Grinstead-Snell *Introduction to Probability* + Laplace *Philosophical Essay* | +| VI | Goldstein *Classical Mechanics* (× 2 variant strings) | Newton's *Principia* (Motte) | +| VII | Stanley/Brualdi/Knuth combinatorics (× 14 compound source_refs) | Bogart CTGD + Levin *Discrete Math* | +| IX | Barendregt *Lambda Calculus* | PLFA (Wadler/Kokke/Siek) + SF-LF | +| IX | Dummit-Foote *Abstract Algebra* | Judson AGT | +| IX | Böhm-Jacopini 1966 | SF-LF (Imp.v sequence/conditional/while) | + +Distribution by substrate (most-cited substrates): + +- SF-LF Pierce et al.: 6 alias rows (Mendelson, Enderton, Landau, 2× Gödel variants, Böhm-Jacopini) +- Russell IMP 1919: 4 (Mendelson, Enderton, Landau, 2× Gödel variants) +- Newton Principia: 2 (Goldstein × 2 variants) +- Bogart CTGD: 14 (pillar VII compound source_refs, full strings) +- Levin: 14 (same pillar VII rows, second substitute) +- Cantor 1915, Russell PoM, Dedekind, Peano, PLFA, Judson, Whitehead-Russell PM, + De Morgan FNL, Boole, Laplace, Grinstead-Snell: 1-3 rows each + +Each row in `~/.arborist/shards/000.db:citation_aliases` carries: +`decision_at` (unix timestamp), `decision_by` ("fox 2026-05-10" +across this batch), `decision_rationale` (free text — caveats, +peer-vs-primary distinction, partial-coverage warnings). + +Listed via `arborist alias citation list`. Full audit trail +preserved across `audit_events` chain. Re-running +`arborist warrant-resolve --use-aliases --write` after any new +alias is registered is the way to extend coverage. diff --git a/docs/tickets/ticket-000042-term-aliases-table.md b/docs/tickets/ticket-000042-term-aliases-table.md index b134c2d..77a77d9 100644 --- a/docs/tickets/ticket-000042-term-aliases-table.md +++ b/docs/tickets/ticket-000042-term-aliases-table.md @@ -1,6 +1,6 @@ # Ticket #000042 — Term-aliases table (vocabulary-mismatch bridge) -**Status:** closed · mechanism + 4 smoke aliases landed 2026-05-09 — **all 18 Hilbert pillar IV records resolve** (11 unaliased, 7 alias-resolved). Aliases registered: `incidence ↔ connection`, `euclidean parallel postulate ↔ axiom of parallels`, `non triviality ↔ space axiom`, `side angle side ↔ included angle` (all geometry domain) +**Status:** closed · mechanism + 4 smoke aliases landed 2026-05-09; **13 rows live by 2026-05-10** across geometry + classical-physics + arithmetic domains. Geometry rows lifted all 18 Hilbert pillar IV records (4 smoke aliases for the 1902-Townsend vs modern-vocabulary gap). Classical-physics rows registered for Newton 1729 vocabulary (some unused — cascade picked different tokens; informational only). Arithmetic rows for Peano symbolic-vs-modern axiom names (most unused — same reason). **Opened:** 2026-05-09 **Scope:** Add an `arborist term_aliases` table that maps a `(term, domain)` pair to an alternate term used in older /