arborist/docs/tickets/ticket-000029-claim-pack-source.md

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

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.