diff --git a/docs/TICKETS.md b/docs/TICKETS.md index e01940f..428790c 100644 --- a/docs/TICKETS.md +++ b/docs/TICKETS.md @@ -61,6 +61,8 @@ Newest first. Update on every open/close. | ID | Title | Status | Opened | Directive | |----------|------------------------------------------------|-----------------------|------------|-----------| +| #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 | — | | #000034 | Hessian alignment under φ_linear | open · awaiting go/no-go (#000018 follow-up) | 2026-05-09 | — | @@ -100,4 +102,4 @@ Newest first. Update on every open/close. ## Next ID -`000037` +`000039` diff --git a/docs/tickets/ticket-000038-phase-4-content-acquisition.md b/docs/tickets/ticket-000038-phase-4-content-acquisition.md new file mode 100644 index 0000000..094ebf0 --- /dev/null +++ b/docs/tickets/ticket-000038-phase-4-content-acquisition.md @@ -0,0 +1,223 @@ +# Ticket #000038 — Phase 4 content acquisition for warrant coverage + +**Status:** open · awaiting go/no-go +**Opened:** 2026-05-09 +**Scope:** Widen warrant-resolver coverage from 11/92 records +(Hilbert pillar IV) to a substantively larger fraction of the +claim-pack corpus by ingesting the cited textbooks the substrate +itself flagged as priorities. License-gated per textbook; +proprietary works require fox's explicit decision and a clear +acquisition path (purchased PDF / library e-book / written +permission / PD substitute). +**Audience:** fox (license decisions); future blackops shifts +running the next round of warrant promotion. +**Hard constraint:** **same fail-closed license discipline as +#000031 §2.1.** Allow-list: PD, CC0, CC-BY-*, CC-BY-SA-*, GFDL-*, +AGPL-3.0, Apache-2.0, MIT. Anything CC-BY-NC, CC-BY-ND, or +proprietary requires explicit fox approval AND a documented +acquisition path before it enters the manifest with a non-empty +URL set. + +--- + +## 1. Problem statement + +`#000031` Phase 1+2+3 landed today with **11 of 92 claim-pack +records** bound by Merkle proof to a primary-source surface +chunk — all pillar-IV Hilbert axioms citing *The Foundations of +Geometry by David Hilbert* (PG #17384, PD via age, ingested +through the new `textbook_tex` source). + +The remaining 81 records sit at ANCHOR-WARRANTED because their +cited textbooks are not in our shard cluster. The warrant +resolver correctly returns no match, no derivations row, no +upgrade. Adding those textbooks (where licensing permits) is +the path to widen coverage. + +The substrate produced its own priority list: walking every +unresolved record's parsed citation and counting which authors ++ titles appear most frequently tells us EXACTLY which +acquisitions would move the dial most. + +## 2. Substrate-derived priority list (2026-05-09 measurement) + +Top unresolved authors by record-count impact: + +| Author | Records | Pillar(s) | License status | +|---|---|---|---| +| Stanley *Enumerative Combinatorics* | 11 | VII | proprietary (Cambridge) | +| Jech *Set Theory* | 10 | II | proprietary (Springer) | +| Brualdi *Introductory Combinatorics* | 9 | VII | proprietary (Pearson) | +| Knuth *TAOCP* | 9 | VII | proprietary (Addison-Wesley) | +| Mendelson *Introduction to Mathematical Logic* | 7 | I | proprietary (CRC) | +| Landau *Foundations of Analysis* | 7 | III | **PD-by-age** (1930; English translation 1951 still in copyright) | +| Hilbert *Foundations of Geometry* | 7 | IV | **PD ingested**, but resolver fails on records whose discriminating token (`Incidence`, `Plane`, `Line`) is too common in the text — see §6 | +| Barendregt *Lambda Calculus* | 7 | IX | proprietary (Elsevier) | +| Enderton *Mathematical Introduction to Logic* | 6 | I | proprietary (Academic) | +| Gödel *On Formally Undecidable Propositions* | 6 | III | **PD-by-age** (1931; van Heijenoort 1967 translation in copyright) | +| Dummit + Foote *Abstract Algebra* | 6 | (algebra) | proprietary (Wiley) | +| Kolmogorov *Foundations of Probability* | 5 | V | German PD-by-age; Morrison 1956 English in copyright | +| Goldstein *Classical Mechanics* | 5 | VI | proprietary (Pearson) | + +**Three buckets:** + +1. **PD originals** (Landau German 1930, Gödel German 1931, + Kolmogorov German 1933, Hilbert German 1899). All + foreign-language; ingestion would be in the original + language. Possibly useful for some kinds of retrieval but + our claim-pack records cite ENGLISH titles, so the + resolver's title-matching would need a multilingual + extension OR we'd need PD English translations (often the + binding constraint). +2. **Proprietary modern textbooks** (Stanley, Jech, Brualdi, + Knuth, Mendelson, Enderton, Barendregt, Dummit-Foote, + Goldstein). License-gated per text; require fox's decision. +3. **Already-ingested but resolver-misses** (the 7 Hilbert + records). A resolver fix, not a content acquisition. + See §6. + +## 3. Design choices + +### 3.1 License-decision matrix + +For each proprietary textbook, fox needs to pick: + +| Option | What it means | Cost | Provenance | +|---|---|---|---| +| **A. Skip** | Stay at ANCHOR-WARRANTED for those records permanently | Zero | Honest; substrate stays under-warranted | +| **B. Personal-copy ingest, single machine** | Ingest a purchased / library-checked-out PDF as a private surface; record never leaves fox's machine | Cost of book(s); acquisition time | Strong (we own/borrow the source) | +| **C. PD substitute** | Find a comparable PD work; ingest that; rewrite claim-pack `source_reference` to point at it | Authoring effort; loses fidelity to original cite | Weakened (substituted source is similar but not identical to what claim-pack records cite) | +| **D. Negotiate redistribution rights** | Get explicit permission from rights-holder | Months; only viable for a few specific works | Strongest | + +**Recommended path per textbook:** + +- **Knuth TAOCP** — option **B** (Knuth's known-to-permit + educational redistribution; contact the rights holder). +- **Mendelson + Enderton** — option **C** (PD substitute: + Hilbert-Ackermann 1928 *Principles of Mathematical Logic*, + PD by age, covers the same ground). +- **Stanley + Brualdi** — option **B** (purchase or library; + these are in college library e-book catalogs almost + universally). +- **Jech** — option **B** (library e-book) or option **C** + (Halmos *Naive Set Theory* PD if 1960; needs verification). +- **Barendregt** — option **A** (defer; pillar IX is + paper-level not book-level anyway). +- **Goldstein** — option **C** (Newton's *Principia* via Motte + is already ingested; add a citation-rewrite step for pillar + VI records). +- **Dummit + Foote** — option **C** if a PD substitute exists; + otherwise **A**. + +### 3.2 Citation-rewrite mechanism (for option C) + +The claim-pack `source_reference` is currently a string field. +Rewriting it requires either: + +(a) **Re-author the bundle** — produce a new +`axiomsclaude-vii-v2.json` (and v2 of the other Claude bundles) +with substituted citations; re-ingest. Old records stay in +shard 000.db unless explicitly burned. +(b) **Add an alias table** — `arborist citation_aliases` +table mapping `"Original Cite by X" → "Substitute Cite by Y"`, +read at warrant-resolve time. Cleaner — original citations stay +intact; resolver knows which surface to look in. + +→ **(b)** is the cleaner architectural fit. Proposal: add to +the existing `arborist concept` family or as a new top-level +table `citation_aliases(original_ref, substitute_ref, +substitute_authors, substitute_title, decision_at, decision_by)`. + +### 3.3 What this ticket does NOT do + +- **Does not buy textbooks.** That's a fox-decision-driven + acquisition outside the codebase. +- **Does not implement the Hilbert resolver fix** (§6) — the + warrant resolver's discriminating-token strategy is too strict + for axioms whose discriminating words ("Incidence", "Plane") + are common in the text. That's a #000031 Phase 5 follow-up. +- **Does not add multilingual support** for ingesting PD + German originals. Same scope rationale. + +## 4. Recommendation + +Sequence: + +1. **Fox picks an acquisition path per textbook from the table + above.** Single message; low blackops effort. +2. For each fox-approved textbook: + - Land in `bench/fixtures/textbooks/manifest-v1.jsonl` with + `license` token + `tex_url` / `urls` populated, OR + - Land in a private `manifest-private-v1.jsonl` (gitignored) + for personal-copy ingest. +3. Run `make textbook-` per the existing per-book + convention; let `arborist warrant-resolve --write` re-run. +4. Each iteration: track derivations-rows count and the warrant + tail's appearance rate on the bench questions. + +Targets: each bucket of acquisitions should bring 5-10 more +records into warrant coverage. End state after all "B" options +ingest: ~50/92 records resolved (vs 11 today). + +## 5. Out of scope + +- Resolver fix for too-generic discriminating tokens (Hilbert §6 + case) — separate Phase 5 ticket. +- Ingesting the 1899 German Hilbert original or 1933 German + Kolmogorov — multilingual scope. +- Citation-aliases schema implementation — depends on §3.2 + decision; separate ticket. +- The 6 records citing Gödel's *On Formally Undecidable + Propositions* — original 1931 paper is 25 pages, paper-level + not book-level; depends on a paper-ingest helper that's + out of scope for any current ticket. + +## 6. The Hilbert resolver-miss issue (footnote) + +7 of the 18 Hilbert pillar-IV axiom records currently fail to +resolve, even though the textbook IS in the shard. The records +are: + + Axiom of Line Incidence + Axiom of Plane Incidence + Axiom of Point-Line Incidence + Axiom of Point-Plane Incidence + Axiom of Non-Triviality + Axiom of Side-Angle-Side (SAS) + Euclidean Parallel Postulate + +The discriminating-token strategy filters out generic terms +("axiom", "theorem", "principle") then AND-joins the rest. For +"Axiom of Line Incidence" the discriminating tokens are +"Line" + "Incidence". Both are ALL OVER Hilbert's geometry +text — so FTS5 returns too many candidate chunks and BM25 +ranking can't pin a winning one. The matcher backs off and +returns no match. + +This is a known limitation noted in the bench journal. Fix +candidates: + +- Use TF-IDF instead of BM25 over the whole textbook for + ranking — favors discriminating CHUNKS, not just discriminating + tokens. +- Boost chunks that contain the EXACT axiom name as a phrase + ("Axiom I,1" or "Group I" labels in Hilbert). +- Use the CLAIM-PACK record's chunk content (the Δ formula or + ∇verbose prose) as the FTS5 query, not just the title. + +That's a Phase 5 follow-up. Folding into this ticket would +overload its scope. + +## 7. Status + +Open · awaiting fox's per-textbook acquisition decisions. + +Estimated size: + +- Per-textbook ingest: ~5 min if license-clean and HTML/TeX + available; up to 1 hour if PDF→text conversion is needed and + pandoc fails. +- Citation-aliases mechanism (§3.2 option b): ~150 LOC + tests + + small migration; separate ticket if approved. +- Resolver fix for Hilbert misses (§6): ~80 LOC + targeted + bench; separate ticket.