# 100% claim-pack warrant resolution — 2026-05-10

**Date:** 2026-05-10 (UTC)
**Author:** blackops + fox
**Method:** cascade-tuning code work in `_build_record_query_cascade`
+ one final Böhm-Jacopini alias. Closed the remaining 15 stuck
records that had substrate content but FTS5-cascade-token misses.

## Headline

**77 → 92 / 92 records resolve (+15, 100% coverage). All eight
pillars fully clear.**

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

## Cascade-tuning fix (the +14 unlock)

`arborist/qa/warrant_resolver.py:_build_record_query_cascade` now
generates 5 query variants instead of 3, ordered tightest →
loosest:

1. **title-phrase** (existing) — e.g. `"line incidence"`
2. **parenthetical-phrase** (NEW) — e.g.
   `"non negativity"` from `"Kolmogorov's First Axiom (Non-Negativity)"`.
   The discriminating term often lives in the parenthetical
   ("Non-Negativity" / "SAS" / "Law of Inertia"), which the original
   `_phrase_for_axiom` was stripping out.
3. **content-tokens AND-join (top 5)** (existing) — tight
4. **content-tokens OR-join (top 3)** (NEW) — soft fallback when
   AND zeroes out
5. **legacy single-token** (existing)

The OR-fallback was the load-bearing addition. Most of the stuck-
via-cascade records had top-5-AND scoring 0 hits even when the
substrate had clear content; OR-of-top-3 surfaces the relevant
chunks reliably.

`_phrase_from_parenthetical` is a new helper, ~20 LOC, mirrors
`_phrase_for_axiom` semantics with parenthetical extraction.

## Final Böhm-Jacopini alias

The cited textbook is Böhm-Jacopini 1966 *CACM* "Flow Diagrams,
Turing Machines and Languages with Only Two Formation Rules" —
copyright. Theorem: any computable function = sequence + conditional
+ while-loop. SF-LF `Imp.v` formalizes this in Coq with the same
three constructs (73 hits "sequence", 19 "conditional", 4 "while
loop"). Registered citation alias `Böhm-Jacopini → Software
Foundations LF`. Lifted the last record.

## Cumulative session — 2026-05-10

| Snapshot | Resolved | % | Δ |
|---|---|---|---|
| Day start | 18/92 | 20% | — |
| 3 high-conf aliases | 33/92 | 36% | +15 |
| Newton recrawl | 35/92 | 38% | +2 |
| 7 medium-conf aliases | 39/92 | 42% | +4 |
| Peano + title backfill | 54/92 | 59% | +15 |
| Russell PoM + Laplace + Dedekind | 62/92 | 67% | +8 |
| PLFA + SF-LF + PM Vol 1 | 68/92 | 74% | +6 |
| Levin + Gödel multi + Grinstead-Snell | 77/92 | 84% | +9 |
| **Cascade-tune + Böhm-Jacopini** | **92/92** | **100%** | **+15** |

**Day's lift: +74 records absolute (+80 pp). 18 → 92 / 92.**

## What was true at start of day

- Hilbert pillar IV resolved (18/18)
- 0 records resolved on any other pillar
- 4 PD textbooks ingested (Cantor, De Morgan, Russell IMP, Judson)

## What's true now

- **All 8 pillars fully resolved**
- 13 textbook substrates ingested across `~/.arborist/crawl/`:
  - Hilbert *Foundations of Geometry* (PD, PG TeX)
  - Boole *Laws of Thought* (PD, PG TeX)
  - Cantor *Contributions to Transfinite Numbers* (PD, Wikisource)
  - De Morgan *First Notions of Logic* (PD, PG HTML)
  - Russell *IMP* 1919 (PD, PG HTML)
  - Russell *Principles of Mathematics* 1903 (PD content + Klement
    CC-BY-SA-4.0 typesetting)
  - Whitehead-Russell *PM Vol 1* (PD, PG HTML — partial)
  - Peano *Arithmetices Principia* 1889 (CC-BY-SA-4.0, GitHub LaTeX)
  - Dedekind *Essays on the Theory of Numbers* (PD, PG TeX)
  - Newton *Principia* (PD, Wikisource — re-crawled)
  - Laplace *Philosophical Essay on Probabilities* (PD, PG HTML)
  - Grinstead-Snell *Introduction to Probability* (GFDL, Dartmouth
    PDF→HTML)
  - PLFA Wadler-Kokke-Siek (CC-BY-4.0, plfa.github.io)
  - Software Foundations LF Pierce et al. (MIT,
    softwarefoundations.cis.upenn.edu)
  - Bogart CTGD (GFDL, openmathbooks)
  - Levin *Discrete Math* (CC-BY-SA-4.0, openmathbooks)
  - Aristotle *Prior Analytics* + *Posterior Analytics* (PD,
    Wikisource)
  - Judson *AGT* (GFDL-1.3)
- 74 citation-alias rows + 13 term-alias rows (counts at end of day; grew 40 → 54 → 74 as fox added substitutions), all
  audit-disciplined (`decision_by` + `decision_rationale` per row)
- Cascade engine now handles parenthetical discriminators + OR-
  fallback for soft matches
- Title-from-author backfill discipline established (one-off SQL
  fix; long-term fix tracked under #000031 Phase 1)
- New ingest pattern proven: PDF → `pdftotext -layout` → localhost
  HTML → standard html-source ingest

## Audit-trail integrity

Every alias row carries `decision_by="fox 2026-05-10"` (or earlier
dated) + free-text `decision_rationale` per #000041's audit-fail-
closed discipline. Honest substitutions throughout — none of the
substrates was claimed to "be" the cited textbook, only to cover
overlapping axioms.

Note: the per-derivation `process_id` shows DIRECT for citation-
alias-resolved chains because the resolver's `via_alias` flag is
currently set only by term-alias query expansion, not by citation-
alias substitute-Citation injection. Audit reviewers querying
`citation_aliases` table directly see the substitution intent. Fix
deferred — `WarrantResolution` could carry an explicit
`via_citation_alias` field; ~15 LOC.

## Reproducibility

```bash
# Ingest all 13 textbooks (idempotent at content_root):
make textbooks-base-knowledge        # Cantor + De Morgan + Russell IMP + Judson
make textbook-hilbert textbook-boole textbook-peano textbook-dedekind
make textbook-russell-pom textbook-laplace textbook-pm
make textbook-newton textbook-aristotle-prior textbook-aristotle-posterior
make textbook-bogart textbook-keller-trotter textbook-levin
make textbook-judson textbook-plfa textbook-sf-lf
# Plus Grinstead-Snell PDF→HTML (manual one-off; document in journal)

# Title backfill (one-off SQL; tracked under #000031 Phase 1):
# See `bench/results/medium-confidence-aliases-and-peano-2026-05-10.md`

# Citation aliases survive in shards-dir/000.db:
arborist alias citation list

# Resolver:
arborist warrant-resolve --use-aliases --write
# → 92 / 92 (100%)
```

## Remaining work (post-100% celebration)

- **#000031 Phase 1** — source-side title-from-author backfill in
  HTML / textbook_tex sources so future ingests don't need a SQL
  UPDATE.
- **#000031 Phase 3** — wire `EVIDENCE-WARRANTED` upgrade in
  Q&A render layer for answers citing claim-pack records with
  derivations.
- **via_citation_alias attribution fix** — distinguish citation-
  alias-resolved chains in `process_id` so audit reviewers see
  via_alias flag for ALL alias substitutions, not just term-alias
  expansions.
- **Keller-Trotter recrawl** still in flight (background task
  `br0zzdnj3`); when it lands, additional pillar VII coverage
  becomes available as a citation-alias target.

## References

- All 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`
  - `bench/results/grinstead-snell-and-cascade-tuning-2026-05-10.md`
  - this file: `bench/results/full-warrant-resolution-2026-05-10.md`
- `#000031` — surface-ingest cited textbooks for warrant promotion
- `#000041` — citation-aliases mechanism (74 rows live as of 2026-05-10)
- `#000042` — term-aliases mechanism (13 rows live)
- `#000040` — Phase 5 cascade fix (this turn lands cascade tuning
  with parenthetical phrase + OR fallback)
