ticket #000031 Phase 2: warrant resolver + 18 derivations rows landed
Closes the warrant-promotion data path: claim-pack records now
bind to surface-ingested textbook chunks via Merkle inclusion
proofs in the existing `derivations` table.
What landed
===========
arborist/qa/warrant_resolver.py — four pure-data steps + one DB
write:
1. parse_citation(s) — regex pipeline turning the claim-pack
`source_reference` string into structured Citation tuples.
Handles "Title by Author" (single + Oxford-comma multi +
et-al), semicolon-separated multi-cite ("Knuth §1.2.6;
Stanley §1.2; Brualdi §3.5"), and compact author-year
("Pascal 1654") forms.
2. resolve_chunks(c, shards_dir) — FTS5 search across sibling
crawl/ dir's textbook-surface shards. Skips the main numbered
shards (Wikipedia content; would be false positives). Per-
shard match filter requires BOTH author last name AND a title
token in the shard's title-haystack — honest "no match" for
textbooks not yet surface-ingested.
3. compute_proof(shard, doc_root, chunk_id) — reads
merkle_nodes, walks layer-by-layer to assemble siblings;
emits deterministic JSON proof_blob compatible with
arborist/merkle.py verification.
4. write_derivation(...) — INSERT OR IGNORE into the existing
derivations table with process_id="warrant-resolver-v1".
Idempotent at the database layer.
CLI surface
===========
- `arborist warrant-status --shards-dir ...` (read-only) —
emits per-record JSON: parsed citations, FTS5 candidates,
whether a derivations row exists.
- `arborist warrant-resolve --shards-dir ... [--write]` —
default dry-run summary; --write actually computes proofs
and inserts rows.
End-to-end verification
=======================
Real-shard run: `arborist warrant-resolve --shards-dir
~/.arborist/shards --write` →
records_total: 92
records_resolved: 18
derivations_written: 18
All 18 are pillar-IV Hilbert axioms citing "The Foundations of
Geometry by David Hilbert" — the only cited textbook fully
surface-ingested by Phase 1. The remaining 74 records cite
textbooks not in our shard cluster (Mendelson, Enderton,
Jech, Goldstein, Barendregt, Stanley, Brualdi, Knuth, …) and
correctly produce 0 matches; they stay at ANCHOR-WARRANTED
until those textbooks land via future Phase-1 manifest
expansions.
Re-running the writer is a no-op (PK collision on (core_root,
src_root, process_id) = INSERT OR IGNORE).
Drive-by fix
============
arborist/sources/textbook_tex.py — _extract_title now also
parses PG's plain-text `Author:` line and appends "by Author"
to the title, so the warrant resolver's author-last-name match
works against PG-ingested textbooks (Hilbert "The Foundations
of Geometry by David Hilbert" instead of just "The Foundations
of Geometry").
Test suite
==========
tests/test_warrant_resolver.py — 14 unit tests for the citation
parser (no DB / network). Full suite: 1588 passed / 28 skipped.
Phase 3 (verifier wiring)
=========================
NOT in this commit. The data substrate is in place; the
audit_mode upgrade path that lifts answers citing
claim-pack-records-with-derivations from ANCHOR-WARRANTED to
EVIDENCE-WARRANTED requires a verifier change — touches well-
tested code, worth its own ticket so the regression risk is
bounded.
This commit is contained in:
parent
9c42a133e7
commit
f0e6baf907
6 changed files with 1067 additions and 24 deletions
|
|
@ -66,7 +66,7 @@ Newest first. Update on every open/close.
|
|||
| #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 (8 textbooks, 6/7 pillars) landed 2026-05-09; Phase 2 chunk-resolution ahead | 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 | — |
|
||||
| #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 | — |
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# Ticket #000031 — Surface-ingest cited textbooks for claim-pack warrant promotion
|
||||
|
||||
**Status:** in progress · Phase 1 (PD textbook surface ingest) landed 2026-05-09 covering 6/7 g4 pillars; Phase 2 (chunk-resolution + `derivations.proof_blob` warrant promotion) still ahead
|
||||
**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
|
||||
**Opened:** 2026-05-09
|
||||
**Scope:** Ingest the classical textbooks cited by every record in
|
||||
the claim-pack source (`#000029`) — Mendelson 1997, Enderton 2001,
|
||||
|
|
@ -386,27 +386,71 @@ tests; full suite: 1574 passed / 28 skipped.
|
|||
yellow-light pending license decision per §2.1. Manifest entry
|
||||
kept as a license-fail placeholder.
|
||||
|
||||
### Phase 2 — chunk-resolution + warrant promotion (NOT YET LANDED)
|
||||
### Phase 2 — chunk-resolution + warrant writer (LANDED 2026-05-09)
|
||||
|
||||
The data substrate is in place; the warrant promotion itself
|
||||
requires:
|
||||
Implemented in `arborist/qa/warrant_resolver.py`:
|
||||
|
||||
1. **Citation parser** — `source_reference` string ("A
|
||||
Mathematical Introduction to Logic by Herbert B. Enderton")
|
||||
→ structured `(authors, title, year, section?)` tuple.
|
||||
2. **Chunk resolver** — given a citation, FTS5-search candidate
|
||||
surface shards for theorem name + key terms, return top
|
||||
chunk(s).
|
||||
3. **Merkle inclusion proof writer** — for each (claim_pack
|
||||
record, surface chunk) match, compute the per-chunk inclusion
|
||||
proof using `arborist/merkle.py`, serialize to JSON.
|
||||
4. **`derivations` row writer** — `(core_root,
|
||||
src_root, proof_blob, process_id="warrant-resolver-v1",
|
||||
distilled_at)`.
|
||||
5. **Verifier wiring** — `audit_mode` upgrade path so claims
|
||||
with a `derivations` row tying back to a real surface get
|
||||
**EVIDENCE-WARRANTED** instead of ANCHOR-WARRANTED on the
|
||||
four-rung ladder.
|
||||
1. **Citation parser** (`parse_citation`) — pure regex pipeline.
|
||||
Handles three observed source-reference patterns: ``"Title by
|
||||
Author"`` (single + multi-author Oxford comma + ``et al.``
|
||||
tail), semicolon-separated multi-citation, and compact
|
||||
``"Author Year"`` / ``"Author §section"`` form. 14 unit tests.
|
||||
2. **Chunk resolver** (`resolve_chunks`) — searches sibling
|
||||
``crawl/`` dir's textbook-surface shards (skipping the main
|
||||
numbered shards which hold Wikipedia content). Per-shard
|
||||
``_shard_matches_citation`` filter requires both author last
|
||||
name AND a title token to appear in the shard's title-haystack
|
||||
— produces honest "no match" for cited textbooks not yet
|
||||
surface-ingested, exactly the records that should stay at
|
||||
ANCHOR-WARRANTED.
|
||||
3. **Merkle inclusion proof writer** (`compute_proof`) — reads
|
||||
``merkle_nodes`` for the document_root, walks layer by layer
|
||||
to assemble siblings; emits deterministic JSON. Compatible
|
||||
with the existing ``arborist/merkle.py`` proof verification.
|
||||
4. **derivations row writer** (`write_derivation`) — INSERT OR
|
||||
IGNORE into the existing schema-table with
|
||||
``process_id="warrant-resolver-v1"``. Idempotent at the
|
||||
database layer (PK is `(core_root, src_root, process_id)`).
|
||||
5. **CLI surface** — ``arborist warrant-status`` (read-only,
|
||||
shows resolver matches per record as JSON) +
|
||||
``arborist warrant-resolve [--write]`` (default dry-run
|
||||
summary; ``--write`` actually computes proofs + inserts rows).
|
||||
|
||||
**Verified end-to-end** against the real shard cluster:
|
||||
``arborist warrant-resolve --shards-dir ~/.arborist/shards
|
||||
--write`` resolved **18 of 92 claim-pack records** (all the
|
||||
Hilbert-pillar-IV axiom records that cite *The Foundations of
|
||||
Geometry by David Hilbert* — the only cited textbook fully
|
||||
surface-ingested in this iteration). 18 ``derivations`` rows
|
||||
written, each carrying a valid Merkle proof blob. Re-running
|
||||
the writer is a no-op (idempotent by PK).
|
||||
|
||||
The remaining 74 records cite textbooks not in our shard cluster
|
||||
(Mendelson, Enderton, Jech, Goldstein, Barendregt, Stanley,
|
||||
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 3 — verifier wiring (NOT YET LANDED)
|
||||
|
||||
The data substrate is now in place. 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:
|
||||
|
||||
- The Q&A verifier currently produces `audit_mode` + `violations`
|
||||
per answer. The four-rung ladder is computed in
|
||||
`arborist.cli._render_audit_label._ladder_rung_for_lattice`
|
||||
from those two.
|
||||
- For each cited claim-pack record, look up whether it has a
|
||||
``derivations.process_id='warrant-resolver-v1'`` row. If yes,
|
||||
REMOVE any `WARRANT_MISSING` violation it would have triggered
|
||||
(or add a positive `WARRANT_PROVEN` annotation).
|
||||
- Display label upgrades to EVIDENCE-WARRANTED automatically per
|
||||
the existing ladder logic.
|
||||
|
||||
This is a verifier change — touches well-tested code. Worth its
|
||||
own ticket so the regression risk is bounded.
|
||||
6. **Bench** — verify a known case (e.g., Modus Tollens
|
||||
claim-pack record → Aristotle Prior Analytics chapter)
|
||||
actually promotes from ANCHOR to EVIDENCE.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue