warrant resolver: cascade tuning lifts 77 -> 92/92 (100%)

The +14-record close-out: most stuck records had substrate content in already-ingested shards but the FTS5 cascade picked discriminator tokens the substrate text didn't use as titles. Two surgical additions to _build_record_query_cascade: (1) parenthetical-phrase variant via new _phrase_from_parenthetical helper. The discriminating term often lives INSIDE a trailing parenthetical that _phrase_for_axiom was stripping: "Kolmogorov's First Axiom (Non-Negativity)" -> '"non negativity"' "Newton's First Law (Law of Inertia)" -> '"inertia"' "Axiom of Side-Angle-Side (SAS)" -> '"sas"' (already had this via prior path) (2) content-tokens OR-join (top 3) as soft fallback after the AND join. Most stuck records had top-5-AND scoring 0 hits even when substrate had clear content; OR-of-top-3 surfaces relevant chunks reliably without sacrificing precision (citation + title-haystack guards remain). Plus one final citation-alias row: Boehm-Jacopini -> Software Foundations LF (decision_by="fox 2026-05-10"). SF-LF Imp.v formalizes the structured-program theorem in Coq with sequence / conditional / while-loop — same theorem as Boehm-Jacopini 1966 CACM in modern formal-verification dress. Per-pillar: I: 12/13 -> 13/13 II: 9/10 -> 10/10 III: 11/13 -> 13/13 IV: 18/18 stable V: 2/5 -> 5/5 VI: 3/5 -> 5/5 VII: 11/14 -> 14/14 IX: 11/14 -> 14/14 Total: 92/92 (100%) Cumulative day-of-2026-05-10 lift: 18/92 -> 92/92 (+74 records, +80 pp absolute). Started the day with only Hilbert pillar IV resolved; ended with all 8 pillars fully resolved across 13 textbook substrates (Hilbert, Boole, Cantor, De Morgan, Russell IMP/PoM, PM Vol 1, Peano, Dedekind, Newton, Laplace, Grinstead- Snell, PLFA, SF-LF, Bogart, Levin, Judson, Aristotle). 40 citation-alias rows + 13 term-alias rows, all audit-disciplined per #000041/#000042 (decision_by + decision_rationale per row). All 1623 tests pass.
2026-05-10 08:33:19 -04:00 · 2026-05-10 08:33:19 -04:00 · b7a172cb04
commit b7a172cb04
parent 37cc2f7a58
2 changed files with 245 additions and 10 deletions
--- a/arborist/qa/warrant_resolver.py
+++ b/arborist/qa/warrant_resolver.py
@ -507,6 +507,42 @@ def _phrase_for_axiom(theorem_name: str) -> str:
    return '"' + " ".join(toks) + '"'


+def _phrase_from_parenthetical(theorem_name: str) -> str:
+    """Extract a phrase from a trailing parenthetical when one
+    exists, e.g.
+
+      "Kolmogorov's First Axiom (Non-Negativity)"  → '"non negativity"'
+      "Newton's First Law (Law of Inertia)"        → '"inertia"' (single tok kept here — paren content is high-signal)
+      "Axiom of Side-Angle-Side (SAS)"             → '"sas"' (acronym retained)
+
+    Used as a SECOND-CHANCE phrase when `_phrase_for_axiom` produces
+    something like "kolmogorov first" that doesn't appear verbatim
+    in the substrate. The parenthetical often carries the actual
+    discriminating term the substrate uses.
+    """
+    if not theorem_name:
+        return ""
+    m = re.search(r"\(([^)]+)\)", theorem_name)
+    if not m:
+        return ""
+    inner = m.group(1)
+    # Drop "Law of " / "Axiom of " etc. INSIDE the parenthetical too.
+    inner = re.sub(
+        r"^(?:Axiom\s+of\s+|Theorem\s+of\s+|Law\s+of\s+|Principle\s+of\s+)",
+        "",
+        inner,
+        flags=re.IGNORECASE,
+    )
+    toks = [
+        t.lower() for t in re.findall(r"[A-Za-z]{2,}", inner)
+        if t.lower() not in _GENERIC_THEOREM_TERMS
+        and t.lower() not in _FTS_STOPWORDS
+    ]
+    if not toks:
+        return ""
+    return '"' + " ".join(toks) + '"'
+
+
 def _content_tokens(chunk_content: str, max_n: int = 8) -> list[str]:
    """Extract discriminating tokens from a claim-pack chunk's
    content. Used as the FTS5 query when phrase + title-token
@ -554,22 +590,35 @@ def _build_record_query_cascade(
    non-empty query that yields a result wins (caller handles the
    cascade in :func:`resolve_chunks`).

-    Order: phrase → content-tokens → discriminating-tokens →
-    existing OR fallback.
+    Order, tightest → loosest:
+      1. title-phrase (e.g. '"line incidence"')
+      2. parenthetical-phrase (e.g. '"non negativity"' from
+         "Kolmogorov's First Axiom (Non-Negativity)")
+      3. content-tokens AND-join (top 5)
+      4. content-tokens OR-join (top 3) — softer fallback when AND
+         is too restrictive
+      5. legacy single-token / discriminating-token query
    """
    out: list[str] = []
-    phrase = _phrase_for_axiom(theorem_name)
-    if phrase:
-        out.append(phrase)
+    seen: set[str] = set()
+
+    def _push(q: str) -> None:
+        if q and q not in seen:
+            seen.add(q)
+            out.append(q)
+
+    _push(_phrase_for_axiom(theorem_name))
+    _push(_phrase_from_parenthetical(theorem_name))
    if record_content:
        ctoks = _content_tokens(record_content)
        if ctoks:
-            # Cap to top 5 for the AND-query; more = too restrictive.
-            out.append(" AND ".join(ctoks[:5]))
+            # Tight: top-5 AND-join.
+            _push(" AND ".join(ctoks[:5]))
+            # Looser: top-3 OR-join — fallback when AND zeroes out.
+            if len(ctoks) >= 2:
+                _push(" OR ".join(ctoks[:3]))
    # Existing strategy as last resort.
-    legacy = _build_fts_query(citation, theorem_name=theorem_name)
-    if legacy and legacy not in out:
-        out.append(legacy)
+    _push(_build_fts_query(citation, theorem_name=theorem_name))
    return out


--- a/bench/results/full-warrant-resolution-2026-05-10.md
+++ b/bench/results/full-warrant-resolution-2026-05-10.md
@ -0,0 +1,186 @@
+# 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)
+- 40 citation-alias rows + 13 term-alias rows, 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 (40 rows live)
+- `#000042` — term-aliases mechanism (13 rows live)
+- `#000040` — Phase 5 cascade fix (this turn lands cascade tuning
+  with parenthetical phrase + OR fallback)