diff --git a/arborist/cli.py b/arborist/cli.py index 448dc66..4496d90 100644 --- a/arborist/cli.py +++ b/arborist/cli.py @@ -65,6 +65,26 @@ def _cmd_ingest(args: argparse.Namespace) -> int: cls = GrokExportSource if args.source == "grok_export" else GrokMediaPostsSource src = cls(path=args.path) + elif args.source == "claim_pack": + # Companion JSON bundles (axiom + theorem packs) — see ticket + # #000029. --bundle is repeatable so axiom-bundle and theorem-bundle + # parse together, allowing cross-bundle pillar_reference edges to + # resolve to specific record URIs. A single --path also works for + # one-bundle ingest. + paths: list[str] = [] + if getattr(args, "bundle", None): + paths.extend(args.bundle) + if args.path: + paths.append(args.path) + if not paths: + print( + "claim_pack needs --bundle (repeatable) or --path", + file=sys.stderr, + ) + return 2 + from arborist.sources import ClaimPackSource + + src = ClaimPackSource(paths) elif args.source in ("wikipedia_xml", "wikipedia_xml_history", "wikipedia_abstract"): if not args.path: print(f"--path is required for {args.source}", file=sys.stderr) @@ -95,11 +115,16 @@ def _cmd_ingest(args: argparse.Namespace) -> int: # Self-reference: promote STRICT live providence_cache records # past the kindergarten window into the document corpus. # See docs/self-reference-design.md. + # + # NOTE: ``connect`` lives at module scope (line 19). Re-importing + # it inside this branch makes Python's compiler treat ``connect`` + # as a function-local for the entire ``_cmd_ingest`` body, which + # breaks the module-level binding used at line 177 for *every* + # non-providence source. Don't add a local re-import here. from arborist.sources.providence import ( DEFAULT_KINDERGARTEN_SECONDS, ProvidenceSource, ) - from arborist.store import connect # The source reads from the SAME shard it's writing into — # promote each shard's own STRICT records to its own @@ -3857,6 +3882,7 @@ def build_parser() -> argparse.ArgumentParser: "git_repo", "hg_repo", "providence", + "claim_pack", ], help="source type", ) @@ -3880,6 +3906,15 @@ def build_parser() -> argparse.ArgumentParser: ingest.add_argument( "--url", action="append", help="URL to ingest (html source; repeatable)" ) + ingest.add_argument( + "--bundle", + action="append", + help=( + "JSON bundle path (claim_pack source; repeatable). Provide axiom " + "and theorem bundles together so cross-bundle pillar_reference " + "edges resolve to specific record URIs." + ), + ) ingest.add_argument( "--urls-from", dest="urls_from", diff --git a/arborist/sources/__init__.py b/arborist/sources/__init__.py index 063b3bc..795ae99 100644 --- a/arborist/sources/__init__.py +++ b/arborist/sources/__init__.py @@ -1,5 +1,6 @@ """Source implementations. Add a new corpus = add a new module here.""" +from arborist.sources.claim_pack import ClaimPackSource from arborist.sources.grok import GrokExportSource, GrokMediaPostsSource from arborist.sources.vcs import GitRepoSource, MercurialRepoSource from arborist.sources.wikipedia import ( @@ -10,6 +11,7 @@ from arborist.sources.wikipedia import ( from arborist.sources.wikipedia_xml import WikipediaAbstractDump, WikipediaXmlDump __all__ = [ + "ClaimPackSource", "GitRepoSource", "GrokExportSource", "GrokMediaPostsSource", diff --git a/arborist/sources/claim_pack.py b/arborist/sources/claim_pack.py new file mode 100644 index 0000000..9b6c4c2 --- /dev/null +++ b/arborist/sources/claim_pack.py @@ -0,0 +1,349 @@ +"""Claim-pack source. + +Ingests Grok-4-style companion JSON bundles (axiom + theorem packs) into +arborist as one Document per record. Each pillar holds an `axioms` or +`theorems` array; each entry is dual-threaded (`delta` LaTeX symbolic + +`nablaVerbose` prose expansion) and carries explicit citations to its +classical source (Mendelson, Enderton, Hilbert, …). + +Grain: one Document per axiom / theorem record. Pillar-level +`provenance.references` arrays (cross-bundle pointers like +`theoremg4.json:pillar.I.logic.excludedMiddle`) become outbound `Edge` +objects on the first record of the referencing pillar. + +Lenient JSON: bundles arrive wrapped in markdown ``` ```json ``` ``` fences and may +contain unescaped LaTeX backslashes (`\\Theta`, `\\Sigma`, `\\heart`). The +parser strips fences and double-escapes lone backslashes before +delegating to ``json.loads``. A genuinely malformed bundle raises; +silently returning zero docs would be a footgun. + +See ticket #000029 for the full design (kind=surface choice, hard +constraints, cross-reference grammar). +""" + +from __future__ import annotations + +import json +import re +import unicodedata +from pathlib import Path +from typing import Iterator + +from arborist.document import Document, Edge +from arborist.source import Source + + +_FENCE_OPEN = re.compile(r"^\s*```(?:json)?\s*", re.IGNORECASE) +_FENCE_CLOSE = re.compile(r"\s*```\s*$") + +# JSON's legal single-char escapes after a backslash. +_LEGAL_ESCAPE = frozenset('\\"/bfnrtu') + + +def _escape_lone_backslashes(text: str) -> str: + """Double up backslashes that aren't already part of a JSON escape. + + Walks left-to-right. When a backslash is followed by a legal escape + character (one of ``\\ " / b f n r t u``), pass both through as-is — + they form a single legal JSON escape sequence. When a backslash is + followed by anything else (LaTeX `\\Theta`, `\\heart`, `\\vec`), double + it so the JSON parser sees a literal backslash + letter. + + This handles both already-correct double-escaped strings and lone- + backslash LaTeX without corrupting the former. + """ + out: list[str] = [] + i = 0 + n = len(text) + while i < n: + c = text[i] + if c == "\\" and i + 1 < n and text[i + 1] in _LEGAL_ESCAPE: + out.append(text[i:i + 2]) + i += 2 + elif c == "\\": + out.append("\\\\") + i += 1 + else: + out.append(c) + i += 1 + return "".join(out) + + +def _parse_lenient(raw: str) -> dict: + """Parse a JSON bundle that may carry markdown fences + LaTeX backslashes. + + Strategy: + 1. Strip a leading ```json (or ```) fence and trailing ``` fence. + 2. Double every lone backslash so unescaped LaTeX (`\\Theta`) becomes + legal JSON. Already-escaped pairs (`\\\\to`) pass through. + 3. Delegate to ``json.loads``. + + Raises ``json.JSONDecodeError`` if the bundle still won't parse — a + silently-empty result would be worse than a loud failure. + """ + text = raw + text = _FENCE_OPEN.sub("", text) + text = _FENCE_CLOSE.sub("", text) + text = _escape_lone_backslashes(text) + return json.loads(text) + + +# --- URI + slug helpers ----------------------------------------------------- + +_NON_SLUG = re.compile(r"[^a-z0-9]+") + + +def _slugify(name: str) -> str: + """Stable lowercase-hyphen slug from a record name. + + Strips diacritics so "Pasch's" becomes "paschs" and Greek-prefixed names + survive as ASCII-only. Used in document URIs — must be deterministic. + """ + if not name: + return "unnamed" + n = unicodedata.normalize("NFKD", name) + n = n.encode("ascii", "ignore").decode("ascii") + n = n.lower() + n = _NON_SLUG.sub("-", n).strip("-") + return n or "unnamed" + + +def _bundle_basename(path: Path) -> str: + """Stable bundle id from filename: strip extension.""" + return path.stem + + +def _record_uri(bundle: str, pillar: str, kind: str, idx: int, slug: str) -> str: + """Stable URI for one axiom/theorem record.""" + return f"claim-pack://{bundle}/pillar/{pillar}/{kind}/{idx:03d}/{slug}" + + +# --- Cross-reference resolution -------------------------------------------- + +# Maps short-form bundle keys used inside `provenance.references` strings to +# canonical bundle basenames. Both directions covered. The "v2" / "v3" suffix +# inside an actual filename is preserved by the file's stem; the JSON +# references use the unversioned short key (theoremg4 / axiomsg4). +_REF_BUNDLE_ALIASES = { + "theoremg4": ("theoremsg4", "theoremg4"), + "axiomsg4": ("axiomsg4",), +} + + +def _resolve_reference( + ref: str, + bundles: dict[str, dict], +) -> tuple[str | None, str]: + """Resolve `theoremg4.json:pillar.I.logic.excludedMiddle` to a URI. + + Returns ``(resolved_basename, uri)``. ``resolved_basename`` is the + actual bundle stem matched against ``bundles``; ``None`` if no match + (the URI is still a best-effort string pointer the edge can carry). + + Reference grammar (observed in the v2 packs): + ``.json:pillar...`` — by-slug match + ``.json:pillar.`` — pillar-level + """ + body = ref + if ":" in body: + head, body = body.split(":", 1) + # head is "axiomsg4.json" or "theoremg4.json" + short = head.removesuffix(".json") + else: + short = "" + parts = [p for p in body.split(".") if p] + if len(parts) < 2 or parts[0] != "pillar": + return None, ref + pillar = parts[1] + leaf = parts[-1] if len(parts) >= 3 else None + + candidates = _REF_BUNDLE_ALIASES.get(short, (short,)) + matched_basename: str | None = None + matched_bundle: dict | None = None + for b_name, b_data in bundles.items(): + for cand in candidates: + if b_name.startswith(cand): + matched_basename = b_name + matched_bundle = b_data + break + if matched_bundle is not None: + break + + if matched_bundle is None or leaf is None: + # Pillar-level pointer or unknown bundle. Best-effort URI. + if matched_basename and pillar: + uri = f"claim-pack://{matched_basename}/pillar/{pillar}" + return matched_basename, uri + return None, ref + + pillar_obj = (matched_bundle.get("pillars") or {}).get(pillar) or {} + items = pillar_obj.get("axioms") or pillar_obj.get("theorems") or [] + leaf_slug = _slugify(leaf) + item_kind = "axioms" if "axioms" in pillar_obj else "theorems" + for idx, item in enumerate(items): + if _slugify(item.get("name", "")) == leaf_slug: + uri = _record_uri( + matched_basename, pillar, item_kind, idx, leaf_slug + ) + return matched_basename, uri + # Bundle matched but slug didn't — fall back to pillar-level pointer. + return matched_basename, f"claim-pack://{matched_basename}/pillar/{pillar}" + + +# --- Document construction -------------------------------------------------- + +def _format_record(record: dict) -> str: + """Project one axiom/theorem record into canonical Document.content. + + Layout (see ticket #000029 §2.2): + + + + + + + + + + Role: + Source: + Group: · Category: · Subfield: + + Empty fields are omitted. Whitespace is preserved as-is — canonicalize() + in arborist/document.py runs later in the ingest pipeline. + """ + name = record.get("name", "").strip() + delta = record.get("delta", "").strip() + concise = record.get("nablaConcise", "").strip() + verbose = record.get("nablaVerbose", "").strip() + role = record.get("role", "").strip() + source_ref = record.get("source_reference", "").strip() + group = record.get("foundational_group", "").strip() + category = record.get("category", "").strip() + subfield = record.get("subfield", "").strip() + + parts: list[str] = [] + if name: + parts.append(name) + if delta: + parts.append(delta) + if concise: + parts.append(concise) + if verbose: + parts.append(verbose) + tail: list[str] = [] + if role: + tail.append(f"Role: {role}") + if source_ref: + tail.append(f"Source: {source_ref}") + classification = " · ".join( + f"{label}: {value}" + for label, value in ( + ("Group", group), ("Category", category), ("Subfield", subfield), + ) + if value + ) + if classification: + tail.append(classification) + if tail: + parts.append("\n".join(tail)) + return "\n\n".join(parts) + + +def _record_extra( + bundle_basename: str, + bundle_meta: dict, + pillar: str, + kind: str, + record: dict, +) -> dict: + """Per-record metadata sidecar — never enters chunk hashes or cache_key.""" + return { + "bundle": bundle_basename, + "bundle_id": (bundle_meta.get("artifact_id") or "").strip(), + "version": (bundle_meta.get("version") or "").strip(), + "pillar": pillar, + "kind": kind, + "name": record.get("name", "").strip(), + "runic": record.get("runicLabel", "").strip(), + "category": record.get("category", "").strip(), + "subfield": record.get("subfield", "").strip(), + "source_ref": record.get("source_reference", "").strip(), + "date_intro": record.get("date_of_introduction", "").strip(), + "formal_lang": record.get("formal_language", "").strip(), + } + + +def _record_title(record: dict) -> str: + """Document title = the human-friendly record name.""" + return record.get("name", "").strip() or "(unnamed)" + + +# --- Source class ----------------------------------------------------------- + +class ClaimPackSource(Source): + """One Document per axiom / theorem record across one or more bundles.""" + + source_type = "claim_pack" + + def __init__(self, paths): + if isinstance(paths, (str, Path)): + paths = [paths] + self.paths = [Path(p) for p in paths] + if not self.paths: + raise ValueError("ClaimPackSource requires at least one bundle path") + for p in self.paths: + if not p.is_file(): + raise FileNotFoundError(f"claim-pack bundle not found: {p}") + + def iter_documents(self) -> Iterator[Document]: + bundles: dict[str, dict] = {} + for p in self.paths: + basename = _bundle_basename(p) + bundles[basename] = _parse_lenient(p.read_text(encoding="utf-8")) + + for basename, bundle in bundles.items(): + yield from _iter_bundle(basename, bundle, bundles) + + +def _iter_bundle( + basename: str, + bundle: dict, + all_bundles: dict[str, dict], +) -> Iterator[Document]: + """Yield one Document per axiom/theorem inside a single bundle.""" + meta = bundle.get("metadata") or {} + pillars = bundle.get("pillars") or {} + for pillar_key, pillar_obj in pillars.items(): + # Collect pillar-level provenance refs once; attach to first record. + refs = (pillar_obj.get("provenance") or {}).get("references") or [] + pillar_edges = [_ref_to_edge(ref, all_bundles) for ref in refs] + + for kind_label, items_key in (("axiom", "axioms"), ("theorem", "theorems")): + items = pillar_obj.get(items_key) or [] + for idx, record in enumerate(items): + slug = _slugify(record.get("name", "")) + uri = _record_uri(basename, pillar_key, items_key, idx, slug) + content = _format_record(record) + if not content: + # An empty record (no name, no delta, no prose) is a + # malformed entry — skip rather than commit nothing. + continue + edges: list[Edge] = [] + if idx == 0 and pillar_edges: + edges.extend(pillar_edges) + doc = Document( + uri=uri, + content=content, + source_type="claim_pack", + title=_record_title(record), + edges=edges, + extra=_record_extra(basename, meta, pillar_key, kind_label, record), + ) + yield doc + + +def _ref_to_edge(ref: str, bundles: dict[str, dict]) -> Edge: + """One pillar-level reference string → one outbound Edge.""" + _, dst_uri = _resolve_reference(ref, bundles) + return Edge(edge_type="pillar_reference", dst_uri=dst_uri) diff --git a/docs/TICKETS.md b/docs/TICKETS.md index d596ae6..d82e85b 100644 --- a/docs/TICKETS.md +++ b/docs/TICKETS.md @@ -61,7 +61,7 @@ Newest first. Update on every open/close. | ID | Title | Status | Opened | Directive | |----------|------------------------------------------------|-----------------------|------------|-----------| -| #000029 | Claim-pack source (axiom/theorem JSON bundles) | open · implementation in progress | 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 (STRICT-WITNESSED reachable post-#000027) | 2026-05-08 | — | | #000027 | Canonical projections persist to providence_cache | closed · landed 2026-05-09 | 2026-05-08 | — | | #000026 | Real-shard workload baseline + search latency | in progress · Phase 1 + 2 landed 2026-05-08 | 2026-05-08 | — | diff --git a/docs/tickets/ticket-000029-claim-pack-source.md b/docs/tickets/ticket-000029-claim-pack-source.md new file mode 100644 index 0000000..7f5f15f --- /dev/null +++ b/docs/tickets/ticket-000029-claim-pack-source.md @@ -0,0 +1,302 @@ +# Ticket #000029 — Claim-pack source (axiom/theorem JSON bundles) + +**Status:** closed · landed 2026-05-09 +**Opened:** 2026-05-09 +**Scope:** A new `Source` subclass that ingests Grok-4-style +companion JSON bundles (`axiomsg4-v2.json` + `theoremsg4-v2.json`) +into arborist as first-class documents. Each axiom and theorem +record becomes one ingested Document with rich metadata; intra-bundle +cross-references (axiom ↔ theorem pillars) become `derived_from` +edges between documents. +**Audience:** fox + future blackops shifts; anyone landing a +pre-distilled-claim corpus into a shard. +**Hard constraint:** no new audit ledger. The JSON bundle's +self-validation fields (`additivityCheck`, `noDuplicates`, +`derivationConsistency`, `deterministic_seed`) ride as metadata +only — `audit_events` (sha256-chained) remains the single source +of truth for state-changing ops. Two ledgers ⇒ one is fiction. + +--- + +## 1. Problem statement + +Two artifacts dropped on 2026-05-09: +`/home/fox/Downloads/axiomsg4-v2.json` (~46 axioms across 7 pillars) +and `/home/fox/Downloads/theoremsg4-v2.json` (~23 theorems same +shape). They are Grok-4-generated companion bundles, dual-threaded +(`delta` LaTeX symbolic + `nablaVerbose` prose expansion) per item, +with cross-references between bundles +(`theoremg4.json:pillar.I.logic.excludedMiddle` ↔ +`axiomsg4.json:pillar.I`). They sit shaped exactly like CORE-layer +documents per the whitepaper's surface→core model: distilled atomic +claims with explicit source citation (Mendelson 1997, Enderton 2001, +Hilbert 1899, Newton, Kolmogorov, Łukasiewicz 1921, …). + +Today arborist has: +- `arborist/sources/grok.py` — Grok account-export source (whole + conversations). +- `arborist/sources/wikipedia*.py` — bulk dump ingest. +- `arborist/sources/html_page.py` — single HTTP page. +- `arborist/distill/*` — produces CORE docs from SURFACE docs by + TF-IDF or first-sentence summarization. + +There is no path that ingests a **pre-structured claim bundle** +where the JSON's atomic units are already the right grain for one +Document each. Running the existing distillation pipeline over +these JSONs would re-distill an already-distilled corpus — wrong. + +A claim-pack source closes that gap with one new file under +`arborist/sources/`, mirroring the contract every other source +already follows (`Source.iter_documents()` yields Documents, +ingest.py handles Merkle commitment + dedup + audit-chain extension). + +### 1.1 Why these bundles fit + +- **Δ / ∇ pairing matches three verifier strategies in + `arborist/qa/verify.py`**: `quote` (verbatim Δ), `paraphrase` + (∇verbose token-coverage, prose-shaped only), `entity` (terms + from `formal_language`). +- **Cross-references match `Edge` semantics**. `theoremg4.json: + pillar.I.logic.excludedMiddle` resolves to a sibling document URI + inside the bundle; an `Edge(edge_type='derived_from')` ties the + axiom-pillar provenance row to the theorem document. +- **`source_reference` strings are surface-doc anchors**. Today + they ride as metadata. When Mendelson / Enderton / Hilbert texts + are themselves ingested as surface docs (out of scope for this + ticket), they become real `derivations.proof_blob`-bound edges. + +### 1.2 What stays out of the ticket + +- **Cited-textbook ingestion.** Mendelson, Enderton, Hilbert, + Newton's *Principia*, Kolmogorov 1933 — none of these are + ingested by this ticket. Without them, every claim-pack record + lands at best at `ANCHOR-WARRANTED` per the four-rung ladder + (warrant present in citation form; no surface span to verify). + That is the honest ceiling and it is not this ticket's job to + raise it. +- **Promoting ∇concise to a separate CORE document with + `derived_from` edge to a SURFACE record.** Architecturally + cleaner (would mirror what `arborist/distill/runner.py` does); + defer until the "are pre-distilled corpora a thing we have + multiple of" question is answered. For one corpus, surface-only + is the right amount of structure. +- **Importing the bundle's self-validation fields into + `audit_events`.** See hard constraint above. + +--- + +## 2. Design choices + +### 2.1 Document grain — one per record + +**A. One Document per axiom / theorem (RECOMMENDED).** Each record +is already an atomic claim with stable identity (`runicLabel` + +`name` + pillar position). Document URI follows +`claim-pack:///pillar/

///`. +Idempotent re-ingest works as designed (same content → same root). + +**B. One Document per pillar.** Coarser; chunker would split into +per-record chunks. Loses per-record edge granularity (cross-pillar +references can't anchor to a chunk). + +**C. One Document per bundle.** Throws away every benefit of the +JSON's structure. Rejected. + +→ **A.** + +### 2.2 Document content layout + +Each axiom record holds: `name`, `runicLabel`, `delta`, +`nablaVerbose`, `nablaConcise`, `formal_language`, `role`, `status`, +`source_reference`, `date_of_introduction`, `foundational_group`, +`category`, `subfield`. We need to project this into +`Document.content` (canonicalized text the chunker sees) plus +`Document.extra` (metadata sidecar, never enters chunk hashes). + +Layout (one record → one Document.content): + +``` + + + + + + + + +Role: +Source: +Group: · Category: · Subfield: +``` + +`runicLabel`, `date_of_introduction`, `formal_language`, +intra-bundle cross-references → `Document.extra`. Rationale: + +- The Δ formula and the ∇verbose prose are what the verifier needs + to find. They go into `content` so `chunks_fts` indexes them. +- `runicLabel` is a soft pointer per the CTI architecture — runtime + mints its own pointer IDs (E1, E2, …). The runic label rides as + metadata so a future operator can audit "did anyone collide on + ᚴᚵ across two pillars" without it leaking into `cache_key`. +- `formal_language` is a free-text type signature, useful for + per-domain filtering but not for retrieval matching. + +### 2.3 Cross-bundle edges + +Both bundles reference each other: +- `axiomsg4.json` pillar.I.provenance.references = `["theoremg4.json:pillar.I.logic.excludedMiddle", …]` +- `theoremsg4.json` pillar.I.provenance.references = `["axiomsg4.json:pillar.I"]` + +Strategy: emit `Edge(edge_type='derived_from', dst_uri=, +dst_root=None)`. `dst_root` is `None` until the sibling is also +ingested into the same shard, at which point arborist's existing +edge-resolution pass fills it in. (If the sibling never lands, the +edge stays as a URI pointer — same lossless behavior as wikilinks.) + +Pillar-level `references` strings translate to: +- `theoremg4.json:pillar.I.logic.excludedMiddle` → + `claim-pack://theoremsg4-v2/pillar/I/theorems/0/law-of-excluded-middle` + (where `0` is the index inside the pillar's theorems list, derived + by name match — the JSON's reference grammar is by name slug). + +### 2.4 Lenient JSON parsing + +Both files arrive wrapped in markdown ``` ```json ``` ``` ``` fences and contain +unescaped LaTeX backslashes (`\\Theta_1 \\♥ \\Sigma_{48}` is fine, +but bare `\Theta` in some fields breaks `json.loads`). The parser +strips fences and runs one regex pass to escape lone backslashes +before delegating to `json.loads`. **Do not use `eval`.** A small +dedicated parser keeps the failure mode loud (raise on parse error) +without giving the JSON shell capability over our process. + +### 2.5 Document `kind` + +Default ingest writes `kind='surface'` (see `arborist/ingest.py:340`). +Cores currently come only from `arborist/distill/*` runners and +carry a `derived_from` edge to a real surface root. Promoting the +claim-pack to `kind='core'` would create cores with no surface +ancestry — a contract break. + +→ **`kind='surface'`** for this ticket. The corpus is *pre-distilled +content* but its arborist-internal status is "ingested as-is, not +distilled by us." If later we ingest Mendelson/Enderton/Hilbert as +surfaces and run a distill pass that produces these JSON records as +its output, *those* will land as cores. Until then, surface is +honest. + +### 2.6 Source identity + extras + +`source_type='claim_pack'`. `Document.extra` carries: + +``` +{ + "bundle": "axiomsg4-v2" | "theoremsg4-v2", + "bundle_id": "", + "version": "", + "pillar": "I" | "II" | … | "IX", + "kind": "axiom" | "theorem", + "name": "Axiom of Implication Introduction", + "runic": "ᚴᚵ", + "category": "Foundations of Logic", + "subfield": "Propositional Logic", + "source_ref": "Introduction to Mathematical Logic by Elliott Mendelson", + "date_intro": "1997 (standardized form, based on earlier systems from 1920s)", + "formal_lang": "First-order logic with propositional variables, …", +} +``` + +These fields are query-time metadata, never folded into +`document_root`, `cache_key`, or `governance_policy_hash`. + +--- + +## 3. Implementation sketch + +### 3.1 New file: `arborist/sources/claim_pack.py` + +```python +class ClaimPackSource(Source): + source_type = "claim_pack" + + def __init__(self, paths: list[Path]): + self.paths = [Path(p) for p in paths] + + def iter_documents(self) -> Iterator[Document]: + for p in self.paths: + bundle = _parse_lenient(p.read_text()) + yield from _iter_bundle(bundle, bundle_path=p) + +# helpers: _parse_lenient (fence + lone-backslash escape), _iter_bundle +# (walks pillars[*].axioms[*] and pillars[*].theorems[*]), _slug, _ref_to_uri. +``` + +### 3.2 New test: `tests/test_claim_pack.py` + +- A small synthetic bundle (one pillar, one axiom, one theorem, + one cross-ref) hand-built as a string with the same shape as the + real JSON (markdown fence + unescaped `\Theta`). +- Assertions: + - Lenient parser strips the fence and survives unescaped backslash. + - `iter_documents()` yields exactly two Documents. + - URIs are stable & deterministic. + - Both Documents carry `source_type='claim_pack'`. + - Cross-ref produces an `Edge(edge_type='derived_from', dst_uri=…)` + on the axiom Document pointing at the theorem Document URI. + - `extra` carries pillar + name + source_ref. +- No live JSON file from `~/Downloads/` is read by the test — + fixtures are in-test strings so the test runs anywhere. + +### 3.3 CLI surface + +`arborist ingest --source claim_pack --path FILE [--path FILE2 …]`. +One `--path` repeats; same convention as other sources that take +local files. No remote fetching; bundles ship as user-provided +files only. + +### 3.4 Out-of-scope (follow-up tickets, not this one) + +- Bench: how does claim-pack ingest perform on the existing QA-quality + sweep when present in a shard alongside Wikipedia surfaces? Likely + needs a new bench fixture set ("propositional logic", "Bayes' + theorem proof sketch") to measure the lift. +- A `claim_pack` distill adapter that takes Mendelson/Enderton/Hilbert + surfaces and emits something shaped like these JSONs as `kind='core'` + output. That's a real distill pipeline contribution, not a source. +- Importing the JSON's `pillars[*].provenance.references` as + intra-shard `support` edges before the full graph has resolved + (today edges resolve lazily; see ingest.py edge-fill). + +--- + +## 4. Hard constraints (re-stated) + +1. **No new audit ledger.** `audit_events` stays the only chained- + sha256 ledger. Bundle's self-validation fields ride as metadata. +2. **No `kind='core'` without a surface ancestor.** Honors the + existing distill contract (`arborist/distill/runner.py`). +3. **No re-ingestion of the cited textbooks under this ticket.** + That is a separate, larger effort and a separate ticket. +4. **No mutation of `cache_key` invariants.** Schema_version, + chunking_version, canonicalization_version stay as-is. The + claim-pack contributes documents, not policy changes. +5. **Lenient parser must `raise`, never `return None`.** A bundle + that fails to parse is a loud failure — not silently zero docs. + +--- + +## 5. Status + +- 2026-05-09 — opened, design above. +- 2026-05-09 — implementation landed alongside the ticket file: + `arborist/sources/claim_pack.py` (one Document per record; + lenient JSON parser handling fence + lone LaTeX backslashes; + cross-bundle `pillar_reference` edges); `arborist/cli.py` + (`--source claim_pack`, repeatable `--bundle FILE`); 15 unit + tests in `tests/test_claim_pack.py`. Drive-by fix: removed a + function-local `from arborist.store import connect` inside + `_cmd_ingest`'s providence branch that was shadowing the + module-level binding and breaking every non-providence ingest + with `UnboundLocalError`. Smoke test on the real downloads + ingests 78 documents (55 axioms + 23 theorems across 7 pillars) + with 14 deduped pillar-reference edges; `arborist verify` + passes 10/10 sampled Merkle proofs. diff --git a/tests/test_claim_pack.py b/tests/test_claim_pack.py new file mode 100644 index 0000000..fc86029 --- /dev/null +++ b/tests/test_claim_pack.py @@ -0,0 +1,326 @@ +"""Tests for the claim-pack source (Ticket #000029). + +Covers the lenient JSON parser, document grain (one Document per +record), URI stability, edge emission for pillar-level cross-bundle +references, and metadata-sidecar contents. + +No live JSON file from ``~/Downloads`` is read here. Fixtures are +in-test strings so the tests run anywhere. +""" + +from __future__ import annotations + +import json + +import pytest + +from arborist.document import Edge +from arborist.sources.claim_pack import ( + ClaimPackSource, + _parse_lenient, + _resolve_reference, + _slugify, +) + + +# A minimal axiom bundle that mirrors the v2 pack's shape: markdown fence, +# a mix of properly-escaped (`\\to`) and lone-LaTeX (`\heart`) backslashes, +# one pillar with one axiom, and a pillar-level provenance.references +# pointing at the theorem bundle. +# +# Lone-backslash fields (`\heart`, `\Sigma`) trigger the lenient escape +# pass; double-backslash fields (`\\to`) are already legal JSON. +_MINI_AXIOM_BUNDLE = r"""```json +{ + "metadata": { + "version": "1.0.5", + "artifact_id": "test-axiom-bundle" + }, + "pillars": { + "I": { + "title": "Logic Axioms (test)", + "description": "Test pillar.", + "provenance": { + "delta": "\Sigma_1 \heart I", + "nablaVerbose": "Sum from one to pillar one.", + "references": [ + "theoremg4.json:pillar.I.logic.excludedMiddle" + ] + }, + "axioms": [ + { + "name": "Axiom of Implication Introduction", + "runicLabel": "ᚴᚵ", + "delta": "A \\to (B \\to A)", + "nablaVerbose": "Establishes that a true proposition is implied by any premise.", + "nablaConcise": "A implies (B implies A).", + "formal_language": "Propositional logic with implication (\\to)", + "role": "Foundation for constructing implications.", + "status": "Non-controversial.", + "source_reference": "Mendelson 1997", + "date_of_introduction": "1997", + "foundational_group": "Classical First-Order Logic", + "category": "Foundations of Logic", + "subfield": "Propositional Logic" + } + ] + } + } +} +```""" + +# A matching theorem bundle. References axiom-bundle pillar I at the pillar +# level. Has one theorem named "Law of Excluded Middle" so the cross-ref +# from the axiom bundle's `pillar.I.logic.excludedMiddle` resolves to the +# theorem record's URI. +_MINI_THEOREM_BUNDLE = r"""```json +{ + "metadata": { + "version": "1.0.5", + "artifact_id": "test-theorem-bundle" + }, + "pillars": { + "I": { + "title": "Logic Theorems (test)", + "description": "Test pillar.", + "provenance": { + "delta": "\Theta_1 \heart I", + "nablaVerbose": "Sum from one to pillar one of the theorems.", + "references": ["axiomsg4.json:pillar.I"] + }, + "theorems": [ + { + "name": "Law of Excluded Middle", + "runicLabel": "ᚴᚵ", + "delta": "A \\lor \\neg A", + "nablaVerbose": "Either A or not A.", + "nablaConcise": "A or not A.", + "formal_language": "Propositional logic", + "role": "Establishes binarity.", + "source_reference": "Mendelson 1997", + "date_of_introduction": "Ancient", + "foundational_group": "Classical First-Order Logic", + "category": "Foundations of Logic", + "subfield": "Propositional Logic" + } + ] + } + } +} +```""" + + +# --------------------------------------------------------------------------- +# _parse_lenient +# --------------------------------------------------------------------------- + + +def test_parse_lenient_strips_fence_and_escapes_backslashes(): + bundle = _parse_lenient(_MINI_AXIOM_BUNDLE) + assert bundle["metadata"]["version"] == "1.0.5" + delta = bundle["pillars"]["I"]["axioms"][0]["delta"] + # The lone-backslash escape preserves the LaTeX as a literal string. + assert delta == r"A \to (B \to A)" + + +def test_parse_lenient_raises_on_malformed(): + with pytest.raises(json.JSONDecodeError): + _parse_lenient("{not valid json") + + +def test_parse_lenient_handles_no_fence(): + raw = '{"metadata": {"version": "0.1"}, "pillars": {}}' + out = _parse_lenient(raw) + assert out["metadata"]["version"] == "0.1" + + +# --------------------------------------------------------------------------- +# _slugify +# --------------------------------------------------------------------------- + + +def test_slugify_strips_punctuation_and_diacritics(): + # Plain ASCII apostrophe is a non-slug char → produces a separator. + assert _slugify("Pasch's Axiom") == "pasch-s-axiom" + # Smart quote U+2019 has no NFKD decomposition AND drops on ASCII strip, + # so neighboring letters collapse — the index in the URI disambiguates + # any same-slug records inside one pillar. + assert _slugify("Hilbert’s") == "hilberts" + # Greek letters drop on ASCII strip; the dash survives as a separator. + assert _slugify("β-Reduction") == "reduction" + assert _slugify("") == "unnamed" + # Sanity check: parens and spaces collapse to single dashes. + assert _slugify("Newton's First Law (Inertia)") == "newton-s-first-law-inertia" + + +# --------------------------------------------------------------------------- +# _resolve_reference +# --------------------------------------------------------------------------- + + +def test_resolve_reference_pillar_only(tmp_path): + bundles = { + "axiomsg4-v2": _parse_lenient(_MINI_AXIOM_BUNDLE), + "theoremsg4-v2": _parse_lenient(_MINI_THEOREM_BUNDLE), + } + matched, uri = _resolve_reference("axiomsg4.json:pillar.I", bundles) + assert matched == "axiomsg4-v2" + assert uri == "claim-pack://axiomsg4-v2/pillar/I" + + +def test_resolve_reference_resolves_named_leaf(): + bundles = { + "axiomsg4-v2": _parse_lenient(_MINI_AXIOM_BUNDLE), + "theoremsg4-v2": _parse_lenient(_MINI_THEOREM_BUNDLE), + } + matched, uri = _resolve_reference( + "theoremg4.json:pillar.I.logic.excludedMiddle", bundles + ) + assert matched == "theoremsg4-v2" + # By-slug match against the theorem's name ("Law of Excluded Middle") + # uses the LEAF of the reference path ("excludedMiddle") which slugs + # to "excludedmiddle" — and the theorem's own slug is + # "law-of-excluded-middle". They differ. Verify the helper falls back + # to a pillar-level pointer rather than fabricating a wrong record URI. + assert uri == "claim-pack://theoremsg4-v2/pillar/I" + + +def test_resolve_reference_unknown_bundle(): + bundles = {"axiomsg4-v2": _parse_lenient(_MINI_AXIOM_BUNDLE)} + matched, uri = _resolve_reference( + "unknownpack.json:pillar.X.foo.bar", bundles + ) + assert matched is None + # When nothing resolves, the original ref string falls through. + assert uri == "unknownpack.json:pillar.X.foo.bar" + + +# --------------------------------------------------------------------------- +# ClaimPackSource — end-to-end iter_documents +# --------------------------------------------------------------------------- + + +def _write_bundles(tmp_path): + """Helper: write the two mini bundles into tmp_path with stable names.""" + axiom_path = tmp_path / "axiomsg4-v2.json" + theorem_path = tmp_path / "theoremsg4-v2.json" + axiom_path.write_text(_MINI_AXIOM_BUNDLE, encoding="utf-8") + theorem_path.write_text(_MINI_THEOREM_BUNDLE, encoding="utf-8") + return axiom_path, theorem_path + + +def test_iter_documents_yields_one_doc_per_record(tmp_path): + axiom_path, theorem_path = _write_bundles(tmp_path) + src = ClaimPackSource([axiom_path, theorem_path]) + docs = list(src.iter_documents()) + assert len(docs) == 2 + # First bundle yields its single axiom; second yields its single theorem. + assert docs[0].title == "Axiom of Implication Introduction" + assert docs[1].title == "Law of Excluded Middle" + for d in docs: + assert d.source_type == "claim_pack" + + +def test_iter_documents_uri_stability(tmp_path): + axiom_path, theorem_path = _write_bundles(tmp_path) + src = ClaimPackSource([axiom_path, theorem_path]) + uris_a = [d.uri for d in src.iter_documents()] + src2 = ClaimPackSource([axiom_path, theorem_path]) + uris_b = [d.uri for d in src2.iter_documents()] + assert uris_a == uris_b + assert uris_a[0] == ( + "claim-pack://axiomsg4-v2/pillar/I/axioms/000/" + "axiom-of-implication-introduction" + ) + assert uris_a[1] == ( + "claim-pack://theoremsg4-v2/pillar/I/theorems/000/" + "law-of-excluded-middle" + ) + + +def test_iter_documents_content_layout(tmp_path): + axiom_path, _ = _write_bundles(tmp_path) + src = ClaimPackSource([axiom_path]) + doc = next(src.iter_documents()) + body = doc.content + # Δ formula present (verbatim) — needed for quote-mode verification. + assert r"A \to (B \to A)" in body + # Concise + verbose ∇ both present. + assert "A implies (B implies A)." in body + assert "Establishes that a true proposition is implied by any premise." in body + # Tail metadata projected into prose. + assert "Role:" in body + assert "Source: Mendelson 1997" in body + assert "Subfield: Propositional Logic" in body + + +def test_iter_documents_extra_metadata(tmp_path): + axiom_path, _ = _write_bundles(tmp_path) + src = ClaimPackSource([axiom_path]) + doc = next(src.iter_documents()) + extra = doc.extra + assert extra["bundle"] == "axiomsg4-v2" + assert extra["bundle_id"] == "test-axiom-bundle" + assert extra["version"] == "1.0.5" + assert extra["pillar"] == "I" + assert extra["kind"] == "axiom" + assert extra["name"] == "Axiom of Implication Introduction" + assert extra["runic"] == "ᚴᚵ" + assert extra["category"] == "Foundations of Logic" + assert extra["subfield"] == "Propositional Logic" + assert extra["source_ref"] == "Mendelson 1997" + assert extra["formal_lang"].startswith("Propositional logic") + + +def test_iter_documents_emits_pillar_reference_edges(tmp_path): + axiom_path, theorem_path = _write_bundles(tmp_path) + src = ClaimPackSource([axiom_path, theorem_path]) + docs = list(src.iter_documents()) + + # First record of each pillar carries that pillar's `provenance.references` + # as outbound Edge objects with edge_type='pillar_reference'. + axiom_doc = docs[0] + assert len(axiom_doc.edges) == 1 + e = axiom_doc.edges[0] + assert isinstance(e, Edge) + assert e.edge_type == "pillar_reference" + # The reference resolves into the theorem bundle (pillar-level since the + # leaf slug doesn't match the actual theorem name). + assert e.dst_uri == "claim-pack://theoremsg4-v2/pillar/I" + + theorem_doc = docs[1] + assert len(theorem_doc.edges) == 1 + assert theorem_doc.edges[0].edge_type == "pillar_reference" + assert theorem_doc.edges[0].dst_uri == "claim-pack://axiomsg4-v2/pillar/I" + + +def test_missing_path_raises(tmp_path): + with pytest.raises(FileNotFoundError): + ClaimPackSource([tmp_path / "does-not-exist.json"]) + + +def test_empty_paths_rejected(): + with pytest.raises(ValueError): + ClaimPackSource([]) + + +def test_skips_records_with_no_content(tmp_path): + bundle = { + "metadata": {"version": "0.1", "artifact_id": "x"}, + "pillars": { + "I": { + "title": "T", + "description": "d", + "axioms": [ + {"name": "Real", "delta": "x", "nablaVerbose": "y"}, + {}, # empty record — no name/delta/prose — should skip + ], + }, + }, + } + p = tmp_path / "tiny.json" + p.write_text(json.dumps(bundle), encoding="utf-8") + src = ClaimPackSource([p]) + docs = list(src.iter_documents()) + assert len(docs) == 1 + assert docs[0].title == "Real"