ticket #000040 Phase 5: phrase + content-token resolver cascade
Implements the layered cascade strategy from #000040 §3.1 (originally drafted as #000039 — renumbered after collision with parallel-shift's sqlite-vec ticket). What landed =========== arborist/qa/warrant_resolver.py: - _phrase_for_axiom(theorem_name) — strips leading categorical prefix ("Axiom of " / "Theorem " / "Principle ") and trailing parenthetical, returns FTS5 phrase syntax ('"line incidence"', '"plane incidence"', '"side angle side"', etc.) when the theorem name has 2+ tokens. - _content_tokens(chunk_content, max_n=8) — extract discriminating tokens from a claim-pack chunk's body. Drops stopwords / generic theorem terms / common-English (small hand-curated set). Requires count >= 2 to ditch typo / LaTeX residue singletons. Sorts by length DESC then first-position ASC. - _build_record_query_cascade(c, theorem_name, content) — returns ordered list of FTS5 queries to try: 1. Phrase from title 2. Content-tokens AND-joined 3. Existing discriminating-tokens AND-join (legacy) 4. Existing OR-fallback (legacy) - resolve_chunks gains a `record_content` parameter; tries each cascade query in order, first hit wins. - iter_claim_pack_records yields a 5-tuple including content so callers can thread it through. Tests: 6 new unit tests for the cascade helpers (phrase extraction, parenthetical stripping, single-token fallback, content-token filtering, count-2 minimum, cascade ordering). 20 total in test_warrant_resolver.py. Full suite: 1603 passed / 28 skipped. End-to-end honest result ======================== Re-running warrant-resolve on the existing shard cluster: records_total=92, records_resolved=11 (unchanged from Phase 4). The cascade is correct; the lift didn't materialize for Hilbert pillar IV's 7 missing records because of TERMINOLOGY MISMATCH, not query strategy: - claim-pack records (g4 2025) use modern post-1950s names: "Axiom of Line Incidence", "Group I: Axioms of Incidence". - Hilbert's 1902 Townsend translation uses the original "Verknüpfung" / "axioms of connection". - Empirically: the literal token "incidence" appears ZERO times in the ingested Hilbert TeX surface; "connection" is the relevant synonym. No matter how clever the query, you can't find a word that isn't there. The cascade is preserved for any future textbook where cited vocabulary matches textbook prose (modern Stanley / Brualdi / Knuth, etc.). Next-link follow-up: file #000042 term-aliases table (("incidence", "geometry") → ("connection", "geometry")). Sibling design to the citation-alias proposal at #000041. Renumbering note: the Phase 5 ticket file was renumbered 000039 → 000040 mid-session because parallel-shift took 000039 for sqlite-vec at nearly the same time. Internal references in the file follow the post-rename numbering (#000041 = citation-alias, #000042 = term-alias).
This commit is contained in:
parent
7f9bf606dc
commit
b9e5bbdb13
4 changed files with 517 additions and 25 deletions
|
|
@ -414,10 +414,160 @@ def _build_fts_query(citation: Citation, theorem_name: str = "") -> str:
|
|||
return " OR ".join(p.lower() for p in parts) if parts else ""
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Phase 5 — phrase-first + content-token fallback (#000039)
|
||||
#
|
||||
# Problem: discriminating tokens like "Line", "Plane", "Incidence" are
|
||||
# ubiquitous in Hilbert's geometry text, so the AND-joined query
|
||||
# returns too many candidates and BM25 can't pick a winner. Layered
|
||||
# cascade strategy:
|
||||
# 1. Phrase match on the discriminating multi-word phrase from the
|
||||
# theorem name (FTS5 phrase syntax `"line incidence"`).
|
||||
# 2. Content-token AND-join from the claim-pack record's chunk
|
||||
# content (∇verbose prose has more discriminating language than
|
||||
# the categorical title).
|
||||
# 3. Existing discriminating-token AND-join (the current strategy).
|
||||
# 4. Existing OR-fallback (title + author).
|
||||
# Each query is tried in order; first non-empty result wins.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
# Common English words to filter out of content-token candidates.
|
||||
# Hand-picked from the top-100 most frequent English words; small
|
||||
# enough to keep in source. The full FTS5 stopword list lives in the
|
||||
# tokenizer config; this is for our DISCRIMINATING-token heuristic.
|
||||
_COMMON_ENGLISH = {
|
||||
"this", "that", "with", "from", "have", "been", "were", "they",
|
||||
"their", "there", "which", "would", "could", "should", "these",
|
||||
"those", "where", "when", "what", "than", "then", "what", "such",
|
||||
"into", "more", "most", "other", "another", "some", "each",
|
||||
"every", "many", "much", "only", "even", "also", "still",
|
||||
"just", "very", "well", "make", "take", "give", "find",
|
||||
"good", "great", "same", "first", "last", "next", "prior",
|
||||
"case", "form", "term", "kind", "part", "side", "type",
|
||||
"thus", "hence", "must", "shall", "will", "does", "doing",
|
||||
"between", "above", "below", "without", "within", "through",
|
||||
"shown", "given", "because", "however", "therefore",
|
||||
"respectively", "namely", "particular", "particularly",
|
||||
"general", "generally", "specific", "specifically",
|
||||
"expression", "verbosely", "shorthand", "spelt", "denoted",
|
||||
"states", "stating", "stated", "provides", "providing",
|
||||
"logically", "logical", "mathematical", "system", "systems",
|
||||
}
|
||||
|
||||
|
||||
def _phrase_for_axiom(theorem_name: str) -> str:
|
||||
"""Pick a multi-word discriminating phrase from a theorem name.
|
||||
|
||||
Strips a leading "Axiom of " / "Theorem " / "Principle " prefix,
|
||||
then keeps the rest as a phrase if it has at least 2 tokens of
|
||||
length >= 3 (otherwise returns "" — single-token theorems use
|
||||
the existing AND-join strategy).
|
||||
|
||||
"Axiom of Line Incidence" → '"line incidence"'
|
||||
"Axiom of Plane Incidence" → '"plane incidence"'
|
||||
"Axiom of Side-Angle-Side (SAS)" → '"side angle side"'
|
||||
"Pasch's Axiom" → ""
|
||||
"Pythagorean Theorem" → ""
|
||||
"""
|
||||
if not theorem_name:
|
||||
return ""
|
||||
# Strip leading "Axiom of " / "Theorem " / "Principle " etc.
|
||||
text = re.sub(
|
||||
r"^(?:Axiom\s+(?:of\s+|Schema\s+of\s+)?|"
|
||||
r"Theorem\s+(?:of\s+)?|"
|
||||
r"Principle\s+(?:of\s+)?|"
|
||||
r"Law\s+of\s+|"
|
||||
r"Rule\s+of\s+|"
|
||||
r"Definition\s+of\s+)",
|
||||
"",
|
||||
theorem_name,
|
||||
flags=re.IGNORECASE,
|
||||
)
|
||||
# Drop trailing parenthetical (e.g., "(SAS)" or "(SQD §14.1)").
|
||||
text = re.sub(r"\s*\([^)]*\)\s*$", "", text).strip()
|
||||
# Tokenize on non-letter chars (handles hyphens, apostrophes,
|
||||
# numbers, etc.). Lower-case for FTS5.
|
||||
toks = [
|
||||
t.lower() for t in re.findall(r"[A-Za-z]{3,}", text)
|
||||
if t.lower() not in _GENERIC_THEOREM_TERMS
|
||||
and t.lower() not in _FTS_STOPWORDS
|
||||
]
|
||||
if len(toks) < 2:
|
||||
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
|
||||
strategies don't find a match.
|
||||
|
||||
Filters: length >= 5; not in stopword / generic / common-English
|
||||
sets; not pure-digits; appears at least twice in the content
|
||||
(rare-singleton tokens are likely typos or LaTeX residue).
|
||||
Returns top ``max_n`` by length-then-position (longer first;
|
||||
ties broken by earlier appearance — body content beats footers).
|
||||
"""
|
||||
if not chunk_content:
|
||||
return []
|
||||
raw = re.findall(r"[A-Za-z]{5,}", chunk_content)
|
||||
counts: dict[str, int] = {}
|
||||
first_pos: dict[str, int] = {}
|
||||
for i, tok in enumerate(raw):
|
||||
low = tok.lower()
|
||||
if low in _FTS_STOPWORDS:
|
||||
continue
|
||||
if low in _GENERIC_THEOREM_TERMS:
|
||||
continue
|
||||
if low in _COMMON_ENGLISH:
|
||||
continue
|
||||
counts[low] = counts.get(low, 0) + 1
|
||||
if low not in first_pos:
|
||||
first_pos[low] = i
|
||||
# Keep tokens with count >= 2 (ditch typo / LaTeX-residue
|
||||
# singletons); sort by length DESC then first-position ASC.
|
||||
candidates = [
|
||||
(low, n, first_pos[low])
|
||||
for low, n in counts.items()
|
||||
if n >= 2
|
||||
]
|
||||
candidates.sort(key=lambda x: (-len(x[0]), x[2]))
|
||||
return [c[0] for c in candidates[:max_n]]
|
||||
|
||||
|
||||
def _build_record_query_cascade(
|
||||
citation: Citation,
|
||||
theorem_name: str,
|
||||
record_content: str = "",
|
||||
) -> list[str]:
|
||||
"""Build a cascade of FTS5 queries to try in order. First
|
||||
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.
|
||||
"""
|
||||
out: list[str] = []
|
||||
phrase = _phrase_for_axiom(theorem_name)
|
||||
if phrase:
|
||||
out.append(phrase)
|
||||
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]))
|
||||
# Existing strategy as last resort.
|
||||
legacy = _build_fts_query(citation, theorem_name=theorem_name)
|
||||
if legacy and legacy not in out:
|
||||
out.append(legacy)
|
||||
return out
|
||||
|
||||
|
||||
def resolve_chunks(
|
||||
citation: Citation,
|
||||
shards_dir: Path | str,
|
||||
theorem_name: str = "",
|
||||
record_content: str = "",
|
||||
limit: int = 5,
|
||||
) -> list[ResolutionMatch]:
|
||||
"""Search every surface shard under ``shards_dir`` for chunks that
|
||||
|
|
@ -430,6 +580,13 @@ def resolve_chunks(
|
|||
Wikipedia's "Mendelson" article is *about* Mendelson, not the
|
||||
cited textbook itself, and including the main shards both bloats
|
||||
runtime (3.4 M docs per shard) and produces false positives.
|
||||
|
||||
``record_content`` (Phase 5 / #000039) is the claim-pack chunk's
|
||||
body. When provided, the resolver tries a phrase + content-token
|
||||
cascade that produces tighter per-axiom matches than the
|
||||
title-only AND-join — load-bearing for axioms whose titles use
|
||||
ubiquitous-in-the-textbook tokens like "Line" / "Plane" /
|
||||
"Incidence".
|
||||
"""
|
||||
if citation.is_empty():
|
||||
return []
|
||||
|
|
@ -445,29 +602,35 @@ def resolve_chunks(
|
|||
continue
|
||||
candidate_shards.append(db)
|
||||
|
||||
fts_query = _build_fts_query(citation, theorem_name=theorem_name)
|
||||
if not fts_query:
|
||||
queries = _build_record_query_cascade(
|
||||
citation, theorem_name=theorem_name, record_content=record_content
|
||||
)
|
||||
if not queries:
|
||||
return []
|
||||
|
||||
matches: list[ResolutionMatch] = []
|
||||
for shard in candidate_shards:
|
||||
if not _shard_matches_citation(str(shard), citation):
|
||||
continue
|
||||
rows = _fts5_search(str(shard), fts_query, limit=limit)
|
||||
for chunk_id, idx, doc_root, doc_uri, title, snippet, rank in rows:
|
||||
matches.append(
|
||||
ResolutionMatch(
|
||||
citation=citation,
|
||||
shard_path=str(shard),
|
||||
document_root=doc_root,
|
||||
document_uri=doc_uri,
|
||||
document_title=title or "",
|
||||
chunk_id=chunk_id,
|
||||
chunk_idx=idx,
|
||||
score=-float(rank or 0.0),
|
||||
snippet=snippet or "",
|
||||
)
|
||||
)
|
||||
# Try queries in cascade order; first to yield rows wins.
|
||||
for q in queries:
|
||||
rows = _fts5_search(str(shard), q, limit=limit)
|
||||
if rows:
|
||||
for chunk_id, idx, doc_root, doc_uri, title, snippet, rank in rows:
|
||||
matches.append(
|
||||
ResolutionMatch(
|
||||
citation=citation,
|
||||
shard_path=str(shard),
|
||||
document_root=doc_root,
|
||||
document_uri=doc_uri,
|
||||
document_title=title or "",
|
||||
chunk_id=chunk_id,
|
||||
chunk_idx=idx,
|
||||
score=-float(rank or 0.0),
|
||||
snippet=snippet or "",
|
||||
)
|
||||
)
|
||||
break
|
||||
matches.sort(key=lambda m: m.score, reverse=True)
|
||||
return matches[:limit]
|
||||
|
||||
|
|
@ -648,9 +811,15 @@ def _decompress_chunk(content) -> str:
|
|||
|
||||
def iter_claim_pack_records(
|
||||
shards_dir: Path | str,
|
||||
) -> Iterator[tuple[str, str, str, str]]:
|
||||
"""Yield ``(shard_path, record_root, title, source_reference)`` for
|
||||
every claim_pack record across the shards-dir.
|
||||
) -> Iterator[tuple[str, str, str, str, str]]:
|
||||
"""Yield ``(shard_path, record_root, title, source_reference,
|
||||
chunk_content)`` for every claim_pack record across the shards-dir.
|
||||
|
||||
Phase 5 (#000039) added the ``chunk_content`` element so the
|
||||
warrant resolver can use the record's ∇verbose body as a
|
||||
content-token signal — the title alone often shares
|
||||
ubiquitous-in-the-textbook tokens; the prose has more
|
||||
discriminating language.
|
||||
"""
|
||||
shards_dir = Path(shards_dir).expanduser()
|
||||
for db in sorted(shards_dir.glob("*.db")):
|
||||
|
|
@ -671,7 +840,7 @@ def iter_claim_pack_records(
|
|||
text = _decompress_chunk(content)
|
||||
m = _SOURCE_RE.search(text)
|
||||
source_ref = m.group(1).strip() if m else ""
|
||||
yield (str(db), doc_root, title or "", source_ref)
|
||||
yield (str(db), doc_root, title or "", source_ref, text)
|
||||
finally:
|
||||
conn.close()
|
||||
|
||||
|
|
@ -782,12 +951,20 @@ def warrant_status(shards_dir: Path | str, limit: int = 5) -> list[WarrantStatus
|
|||
citation resolver finds. Read-only — no DB writes.
|
||||
"""
|
||||
out: list[WarrantStatus] = []
|
||||
for shard_path, record_root, title, source_ref in iter_claim_pack_records(shards_dir):
|
||||
for shard_path, record_root, title, source_ref, content in iter_claim_pack_records(
|
||||
shards_dir
|
||||
):
|
||||
citations = parse_citation(source_ref)
|
||||
all_matches: list[ResolutionMatch] = []
|
||||
for c in citations:
|
||||
all_matches.extend(
|
||||
resolve_chunks(c, shards_dir, theorem_name=title, limit=limit)
|
||||
resolve_chunks(
|
||||
c,
|
||||
shards_dir,
|
||||
theorem_name=title,
|
||||
record_content=content,
|
||||
limit=limit,
|
||||
)
|
||||
)
|
||||
all_matches.sort(key=lambda m: m.score, reverse=True)
|
||||
out.append(
|
||||
|
|
@ -820,7 +997,7 @@ def warrant_resolve(
|
|||
# Build a record_root → shard_path map once so we don't iterate
|
||||
# again per record.
|
||||
record_shards: dict[str, str] = {}
|
||||
for shard_path, record_root, _, _ in iter_claim_pack_records(shards_dir):
|
||||
for shard_path, record_root, _, _, _ in iter_claim_pack_records(shards_dir):
|
||||
record_shards[record_root] = shard_path
|
||||
|
||||
for status in statuses:
|
||||
|
|
|
|||
|
|
@ -61,6 +61,8 @@ Newest first. Update on every open/close.
|
|||
|
||||
| ID | Title | Status | Opened | Directive |
|
||||
|----------|------------------------------------------------|-----------------------|------------|-----------|
|
||||
| #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 | — |
|
||||
|
|
@ -102,4 +104,4 @@ Newest first. Update on every open/close.
|
|||
|
||||
## Next ID
|
||||
|
||||
`000039`
|
||||
`000041`
|
||||
|
|
|
|||
236
docs/tickets/ticket-000040-phase-5-resolver-content-tokens.md
Normal file
236
docs/tickets/ticket-000040-phase-5-resolver-content-tokens.md
Normal file
|
|
@ -0,0 +1,236 @@
|
|||
# Ticket #000040 — Phase 5 resolver fix (content-token strategy)
|
||||
|
||||
**Status:** closed · cascade landed 2026-05-09; expected lift blocked by terminology mismatch (Hilbert 1902 says "connection", claim-pack says "incidence") — see §6; follow-up tracked as #000042 term-aliases
|
||||
**Opened:** 2026-05-09
|
||||
**Scope:** Fix `arborist.qa.warrant_resolver` for the failure
|
||||
mode noted in `#000038` §6: 7 of the 18 Hilbert pillar-IV axiom
|
||||
records fail to resolve because their discriminating tokens
|
||||
("Incidence", "Plane", "Line") are too common in the cited
|
||||
textbook for BM25 to pick a winning chunk. Add a phrase-first
|
||||
+ content-token-fallback strategy so the resolver finds
|
||||
per-axiom chunks even when the title's individual tokens are
|
||||
ubiquitous.
|
||||
**Audience:** future blackops shifts running warrant promotion
|
||||
on more textbooks.
|
||||
**Hard constraint:** **same fail-closed honesty as #000031.**
|
||||
A failed match still produces no derivations row. The fix
|
||||
expands what counts as a SUCCESSFUL match; it doesn't lower
|
||||
the threshold for false positives.
|
||||
|
||||
---
|
||||
|
||||
## 1. Problem statement
|
||||
|
||||
After `#000031` Phase 1+2+3 landed, 11 of 18 Hilbert pillar-IV
|
||||
axiom records resolved cleanly. The 7 misses 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 current resolver (commit `69e0a95`) extracts discriminating
|
||||
tokens from the theorem name (drops categorical "axiom" /
|
||||
"theorem" / "principle"), AND-joins them as the FTS5 query.
|
||||
For "Axiom of Line Incidence" → tokens `Line` + `Incidence`.
|
||||
|
||||
Both tokens occur on virtually every page of Hilbert's
|
||||
*Foundations of Geometry* — the entire Group I chapter is
|
||||
"Axioms of Incidence" naming straight lines and points.
|
||||
FTS5 returns dozens of candidate chunks; BM25 ranks by IDF
|
||||
weight; no clear winner emerges; the matcher backs off and
|
||||
returns no match.
|
||||
|
||||
This is the false-negative case. The textbook IS in the shard.
|
||||
The axiom IS in the textbook. The resolver just can't find the
|
||||
right chunk because its query is too generic.
|
||||
|
||||
## 2. Design choices
|
||||
|
||||
### 2.1 Strategy options
|
||||
|
||||
**A. Phrase-match first.** Many axiom names have a literal
|
||||
discriminating phrase: "Line Incidence", "Plane Incidence",
|
||||
"Point-Line Incidence". FTS5 phrase syntax `"line incidence"`
|
||||
ranks chunks that contain those exact two words adjacently.
|
||||
Fast, cheap, deterministic.
|
||||
|
||||
Limitation: "Side-Angle-Side" and "Euclidean Parallel
|
||||
Postulate" might not appear verbatim either. Need a fallback.
|
||||
|
||||
**B. Use claim-pack chunk content as the query.** Each claim-
|
||||
pack record's chunk has the Δ formula + ∇verbose prose, which
|
||||
collectively contain WAY more discriminating language than the
|
||||
title. Extract the most-distinctive 5-10 tokens from that
|
||||
content (TF-IDF against a corpus baseline, or just
|
||||
length-based + uniqueness heuristics) and use those as the
|
||||
FTS5 query.
|
||||
|
||||
Limitation: requires reading the claim-pack chunk content
|
||||
per resolver call. Cheap in practice (1 SQL query per record).
|
||||
|
||||
**C. TF-IDF over BM25 ranking.** Replace BM25 with TF-IDF that
|
||||
weights tokens by their rarity within the textbook itself, not
|
||||
just within the global corpus. "Incidence" is rare even within
|
||||
Hilbert's text once you consider it discriminates Group I
|
||||
chapters from Group V chapters.
|
||||
|
||||
Limitation: requires a per-shard token-frequency index.
|
||||
More machinery than warranted; defer.
|
||||
|
||||
**D. Match on Δ-formula tokens.** The Δ field of an axiom is
|
||||
a LaTeX formula like `A \to B \to A`. Most chunks won't
|
||||
contain `\to` at FTS5 token level (LaTeX backslash + `to`).
|
||||
This is too narrow — the cited textbook prose typically
|
||||
DOES NOT have the same LaTeX formulas as the curriculum-shaped
|
||||
claim-pack record.
|
||||
|
||||
→ Recommended: **A then B** as a layered cascade. Phrase match
|
||||
first; if no result, content-token match. Skip C and D for
|
||||
this iteration.
|
||||
|
||||
### 2.2 What "discriminating" means in the content-token path
|
||||
|
||||
For option B, "discriminating" is heuristic. Reasonable rules:
|
||||
|
||||
- Token length ≥ 5 (drops short common words).
|
||||
- Drop generic theorem terms (already in `_GENERIC_THEOREM_TERMS`).
|
||||
- Drop top-50 most common English words (we can hardcode a
|
||||
small list).
|
||||
- Prefer proper nouns (capitalized in original; lowercased for
|
||||
FTS5).
|
||||
- Cap to top-N tokens by some uniqueness score; AND-join.
|
||||
|
||||
A cheap uniqueness signal: token's frequency within the chunk
|
||||
content vs. its frequency across all claim-pack chunks. Tokens
|
||||
that appear in ONE claim-pack record but not in others are
|
||||
discriminating per-record. Pre-compute this.
|
||||
|
||||
### 2.3 What this doesn't change
|
||||
|
||||
- The author-last-name + title-token shard match
|
||||
(`_shard_matches_citation`) stays as-is; this ticket only
|
||||
changes the per-record FTS5 query inside resolved shards.
|
||||
- The fail-closed allow-list and threshold logic stays.
|
||||
- The proof-blob writer stays.
|
||||
|
||||
## 3. Recommendation
|
||||
|
||||
Implement **A then B** in a new helper `_build_record_query`
|
||||
that takes the claim-pack record's title AND chunk content
|
||||
(plus the citation), tries phrase-match on the most
|
||||
discriminating 2-3-word phrase, falls back to content-token
|
||||
AND-join when phrase yields zero.
|
||||
|
||||
Re-run `arborist warrant-resolve --shards-dir ~/.arborist/shards
|
||||
--write` after the fix. Expected: 7 more Hilbert records
|
||||
resolve → 18 of 92 chains.
|
||||
|
||||
## 4. Implementation sketch
|
||||
|
||||
```python
|
||||
def _phrase_for_axiom(theorem_name: str) -> str:
|
||||
"""Pick a 2-3 word discriminating phrase from the theorem name.
|
||||
|
||||
"Axiom of Line Incidence" → "line incidence"
|
||||
"Axiom of Plane Incidence" → "plane incidence"
|
||||
"Pasch's Axiom" → "" (no multi-word phrase; falls through to
|
||||
single-token AND)
|
||||
"""
|
||||
# Strip leading "Axiom of " / "Theorem " / etc.
|
||||
# Take what's left; lowercase + drop generic terms.
|
||||
...
|
||||
|
||||
|
||||
def _content_tokens(chunk_content: str, max_n: int = 8) -> list[str]:
|
||||
"""Pull discriminating tokens from a claim-pack chunk content.
|
||||
|
||||
Uses (a) lengths >= 5, (b) drop generic + stopword lists,
|
||||
(c) prefer proper nouns. Returns top-N uniquely-ranked.
|
||||
"""
|
||||
...
|
||||
|
||||
|
||||
def _build_record_query(
|
||||
citation: Citation,
|
||||
record_title: str,
|
||||
record_content: str,
|
||||
) -> list[str]:
|
||||
"""Returns a list of FTS5 queries to try in order.
|
||||
First non-empty match wins.
|
||||
|
||||
Order:
|
||||
1. Phrase from title (e.g., '"line incidence"')
|
||||
2. Discriminating tokens from chunk content (AND-joined)
|
||||
3. Existing discriminating tokens from title (AND-joined)
|
||||
4. Title tokens OR-joined (existing fallback)
|
||||
"""
|
||||
...
|
||||
```
|
||||
|
||||
Resolver loop tries each query; first to yield a chunk match
|
||||
wins.
|
||||
|
||||
## 5. Hard constraints (re-stated)
|
||||
|
||||
1. Failed match still produces no derivations row.
|
||||
2. Phrase match doesn't introduce false positives — phrase
|
||||
syntax is more selective, not less.
|
||||
3. Content-token strategy uses the SAME data path
|
||||
(claim-pack chunks already in shard) — no schema change.
|
||||
4. Idempotent: same input → same output → re-running is
|
||||
no-op at DB layer (PK on derivations).
|
||||
|
||||
## 6. Status
|
||||
|
||||
**Cascade landed 2026-05-09 (commit TBD); zero impact on
|
||||
Hilbert pillar IV records — root cause is terminology, not
|
||||
ranking.** The cascade itself is correct and ready for
|
||||
textbooks that share vocabulary with the claim-pack record's
|
||||
modern naming.
|
||||
|
||||
The 7 still-unresolved Hilbert records are blocked by a
|
||||
different problem:
|
||||
|
||||
**Terminology mismatch.** Claim-pack records (g4-generated
|
||||
2025) use modern post-1950s names: "Axiom of Line Incidence",
|
||||
"Axioms of Incidence" (Group I). Hilbert's 1902 Townsend
|
||||
translation uses the older "Verknüpfung" / "axioms of
|
||||
connection" — Hilbert's own original term, before the field
|
||||
adopted "incidence" as the standard rendering.
|
||||
|
||||
Verified empirically: the literal token "incidence" appears
|
||||
**zero times** in the ingested Hilbert TeX surface;
|
||||
"connection" is the relevant synonym.
|
||||
|
||||
Phase 5's cascade (phrase → content-tokens → discriminating-
|
||||
tokens → OR-fallback) tries each strategy in order, but
|
||||
every strategy looks for tokens that the TEXTBOOK doesn't
|
||||
contain. No matter how clever the query, you can't find a
|
||||
word that isn't there.
|
||||
|
||||
**Two paths forward (out of this ticket's scope):**
|
||||
|
||||
1. **Add a more recent Hilbert translation** that uses
|
||||
modern "incidence" terminology. Robert Bernhard's 1971
|
||||
edition does; in copyright. Goes in `#000038` Phase 4
|
||||
license decisions.
|
||||
2. **Term-alias layer** — `arborist term_aliases` table
|
||||
mapping `("incidence", "geometry") → ("connection",
|
||||
"geometry")` AND'd with the existing query at warrant-
|
||||
resolve time. Sibling design to the citation-alias
|
||||
proposal in `#000041`. File as `#000042` once Phase 4
|
||||
surfaces concrete need-cases.
|
||||
|
||||
The Phase 5 cascade still pulls its weight for any future
|
||||
textbook where cited vocabulary matches textbook prose —
|
||||
Stanley, Brualdi, Knuth, etc. (modern works using modern
|
||||
terminology). The implementation is preserved for that
|
||||
future landing.
|
||||
|
||||
Estimated-size predictions held: ~150 LOC implementation +
|
||||
the helpers + filter lists. Future-ticket #000041 (term-
|
||||
alias) is the next dependency on this chain.
|
||||
|
|
@ -139,3 +139,80 @@ def test_raw_field_preserved():
|
|||
raw = "Some weird citation by Some Author"
|
||||
out = parse_citation(raw)
|
||||
assert out[0].raw == raw
|
||||
|
||||
|
||||
# --- Phase 5: phrase + content-token cascade (#000039) --------------
|
||||
|
||||
|
||||
def test_phrase_for_axiom_strips_categorical_prefix():
|
||||
from arborist.qa.warrant_resolver import _phrase_for_axiom
|
||||
|
||||
assert _phrase_for_axiom("Axiom of Line Incidence") == '"line incidence"'
|
||||
assert _phrase_for_axiom("Axiom of Plane Incidence") == '"plane incidence"'
|
||||
assert _phrase_for_axiom("Theorem of Pythagoras") == '"pythagoras"' or _phrase_for_axiom("Theorem of Pythagoras") == ""
|
||||
|
||||
|
||||
def test_phrase_for_axiom_drops_parenthetical():
|
||||
from arborist.qa.warrant_resolver import _phrase_for_axiom
|
||||
|
||||
assert _phrase_for_axiom("Axiom of Side-Angle-Side (SAS)") == '"side angle side"'
|
||||
|
||||
|
||||
def test_phrase_for_axiom_returns_empty_for_single_token():
|
||||
from arborist.qa.warrant_resolver import _phrase_for_axiom
|
||||
|
||||
# Single-token axioms have nothing to phrase-match — fall through
|
||||
# to AND-join strategy.
|
||||
assert _phrase_for_axiom("Pasch's Axiom") == ""
|
||||
assert _phrase_for_axiom("Pythagorean Theorem") == ""
|
||||
|
||||
|
||||
def test_content_tokens_filters_common_words():
|
||||
from arborist.qa.warrant_resolver import _content_tokens
|
||||
|
||||
content = (
|
||||
"this axiom states that for every triangle there exists "
|
||||
"a unique line through any two points; the system follows. "
|
||||
"Triangle triangle triangle vertex vertex vertex."
|
||||
)
|
||||
toks = _content_tokens(content)
|
||||
# "triangle" appears 4 times → discriminating; "this", "that",
|
||||
# "every", "system" → common, filtered.
|
||||
assert "triangle" in toks
|
||||
assert "this" not in toks
|
||||
assert "system" not in toks
|
||||
assert "every" not in toks
|
||||
|
||||
|
||||
def test_content_tokens_requires_count_at_least_2():
|
||||
from arborist.qa.warrant_resolver import _content_tokens
|
||||
|
||||
# Singleton tokens ditched (likely typo / LaTeX residue).
|
||||
content = "betweenness betweenness consider unique helpfully"
|
||||
toks = _content_tokens(content)
|
||||
assert "betweenness" in toks
|
||||
# singletons dropped
|
||||
assert "consider" not in toks
|
||||
assert "unique" not in toks
|
||||
|
||||
|
||||
def test_build_record_query_cascade_orders_correctly():
|
||||
from arborist.qa.warrant_resolver import (
|
||||
Citation,
|
||||
_build_record_query_cascade,
|
||||
)
|
||||
|
||||
citation = Citation(
|
||||
title="The Foundations of Geometry",
|
||||
authors=("David Hilbert",),
|
||||
raw="The Foundations of Geometry by David Hilbert",
|
||||
)
|
||||
queries = _build_record_query_cascade(
|
||||
citation,
|
||||
theorem_name="Axiom of Line Incidence",
|
||||
record_content="The line line line connection between point point points axiom incidence relation."
|
||||
)
|
||||
# Phrase is first; legacy AND-join is last.
|
||||
assert queries[0] == '"line incidence"'
|
||||
# The content-token AND-join should appear in the cascade.
|
||||
assert any(" AND " in q for q in queries[1:])
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue