engineering/arborist
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

ticket #000029: claim-pack source for axiom/theorem JSON bundles

Browse source 
ClaimPackSource ingests Grok-4 companion bundles (axiomsg4-v2.json +
theoremsg4-v2.json) at the right grain — one Document per axiom or
theorem record. Each record carries Δ (LaTeX symbolic) + ∇verbose
prose, explicit source citation (Mendelson, Enderton, Hilbert,
Newton, Kolmogorov, Łukasiewicz), foundational-group taxonomy, and a
runicLabel that rides as soft metadata only (runtime mints its own
pointer IDs per CTI architecture). Pillar-level
provenance.references arrays become outbound pillar_reference edges.

Lenient JSON parser strips ```json fences and double-escapes lone
LaTeX backslashes (\Theta, \heart, \vec) without corrupting
already-correct \\to pairs — walks left-to-right and pass-throughs
legal escape sequences. Malformed bundles raise rather than return
empty; silent zero-doc would be a footgun.

CLI surface: --source claim_pack with a repeatable --bundle FILE
flag mirroring html source's --url action=append. Single --path
also accepted for one-bundle ingest.

Drive-by: removed a function-local `from arborist.store import
connect` inside _cmd_ingest's providence branch that was shadowing
the module-level binding via Python's "any local assignment makes
the name local for the entire function" rule, breaking every
non-providence ingest with UnboundLocalError. Comment left in
place explaining why not to re-add it.

Smoke-tested on /home/fox/Downloads/{axiomsg4,theoremsg4}-v2.json
end-to-end: 78 docs (55 axioms + 23 theorems across 7 pillars),
14 deduped pillar-reference edges, 78 audit events, 10/10 sampled
Merkle proofs verify, FTS5 search returns Modus Tollens for
"modus tollens".

Honest ceiling: kind=surface for every record. The pack is
pre-distilled but its provenance is asserted not proven — until
Mendelson/Enderton/Hilbert texts are themselves ingested as
surfaces, the verifier has no derivations.proof_blob to compute
and claim-pack records max out at ANCHOR-WARRANTED on the
four-rung ladder. That's a follow-up ticket, not this one.

Hard constraints honored: no new audit ledger (audit_events
remains the only chained-sha256 ledger; bundle's self-validation
fields ride as metadata only); no kind=core without surface
ancestor; cache_key invariants untouched.

15 unit tests cover lenient parser, slug stability, ref
resolution, doc grain, URI stability, content layout, extra
metadata, edge emission, error paths. All 1280 tests in
make test pass.
This commit is contained in:
russell@unturf.com 2026-05-09 11:44:08 -04:00
parent e19aed8da0
commit b38f4b8b59
No known key found for this signature in database
6 changed files with 1016 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

37
arborist/cli.py
View file

@ -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",

2
arborist/sources/__init__.py
View file

@ -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",

349
arborist/sources/claim_pack.py Normal file
View file

@ -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):
``<bundle_short>.json:pillar.<pillar>.<area>.<slug>`` — by-slug match
``<bundle_short>.json:pillar.<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):
<name>
<delta>
<nablaConcise>
<nablaVerbose>
Role: <role>
Source: <source_reference>
Group: <foundational_group> · Category: <category> · Subfield: <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)

2
docs/TICKETS.md
View file

@ -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 | — |

302
docs/tickets/ticket-000029-claim-pack-source.md Normal file
View file

@ -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://<bundle_id>/pillar/<P>/<axioms|theorems>/<idx>/<slug>`.
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):
```
<name>
<delta>
<nablaConcise>
<nablaVerbose>
Role: <role>
Source: <source_reference>
Group: <foundational_group> · Category: <category> · Subfield: <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=<sibling 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": "<artifact_id from JSON metadata>",
"version": "<JSON metadata.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.

326
tests/test_claim_pack.py Normal file
View file

@ -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"