AGM-R: theorem-minimum reference implementation

AGM-R is the theorem-minimum reference implementation of the capacity triangle (T-I1 + T-I2 + T-M1) defined in the Sagrada formal framework.

It is not a product. It is a 700-line Python artifact that materialises, line-by-line, the structure the theorems prescribe. Sagrada — the production belief-graph engine in engine/core/ — is one member of the AGM-R family, plus production layers (Merkle audit, PROV-O export, NLI integration for paraphrase, extraction pipeline, PyO3 bindings, etc.) that are orthogonal to the theorems.

The theorem-to-code map

Files

What AGM-R is NOT

AGM-R deliberately ships without:

• Merkle audit chain. Production Sagrada embeds chain hashes for cryptographic verification. Out of scope for the capacity-triangle theorems.
• PROV-O / W3C provenance export. Interoperability concern, not a theorem concern.
• NLI / paraphrase-robust comparison. T-I2 saturation holds under exact-text; paraphrase robustness is a separate property that §5.4 shows requires NLI integration.
• Question-type classifier. The 8 structural query types are dispatched via an explicit question_type argument; a learned router is an engineering concern, not a theorem concern.
• Ingestion / extraction from free text. AGM-R takes pre-structured belief records as input. Production Sagrada's LLM-based ingestion is out of scope.
• Performance optimisation. Pure Python; no indices, no caching, no async. A 197-query benchmark run takes ~1 second; this is irrelevant to capacity claims.

Running AGM-R

from agm_r import KnowledgeGraph, assert_belief, revise, retract
from agm_r.queries import revision_count

kg = KnowledgeGraph()
kg = assert_belief(kg, term="pluto_classification", source_id="pluto_1930",
                       claim_text="Pluto is the ninth planet", timestamp="1930-02-18",
                       author="Tombaugh")
kg = assert_belief(kg, term="pluto_classification", source_id="pluto_2006",
                       claim_text="Pluto is a dwarf planet", timestamp="2006-08-24",
                       author="IAU")
print(revision_count(kg, term="pluto_classification"))  # 2

Epistemic Vectors — the retrieval-pipeline primitive

AGM-R exposes the same belief-state summary called an Epistemic Vector: a typed, provenance-native vector for a single belief. Five slots (revision_state, provenance_depth, consistency_score, authority, freshness) are derived deterministically from graph topology and timestamps — no LLM, no free-text classifier.

from agm_r import epistemic_vector

ev = epistemic_vector(kg, "pluto_1930")
print(ev)
# EV(pluto_1930, revised, prov=0, cons=0.00, auth=0.80, fresh=0.00)

Any retrieval pipeline that accepts one vector per document can filter, re-rank, and audit with the same infrastructure cosine-similarity already enjoys. See vectors.py for slot semantics and tests/test_vectors.py for the operational definition.

The empirical claim

Run on the 197-query real-world structural benchmark:

cd cruxia-engine
python -m lab.epistemic_development.pipeline.structural_bench.runner \
    --queries lab/epistemic_development/pipeline/structural_bench/queries_real.jsonl \
    --kb-dir lab/epistemic_development/pipeline/structural_bench/kbs_real \
    --backends agm_r \
    --out-dir results/benchmarks/agm_r/

Expected result: ≥83% accuracy, tying Sagrada (83.8%) and PROV-O + SPARQL (83.8%).

If AGM-R ties, the theorem-minimum claim is empirically vindicated: 700 lines of Python saturate the achievability bound that the capacity triangle characterises. Production Sagrada's additional 5,000+ lines deliver audit, compliance, paraphrase, and deployment value — not accuracy on $\mathcal{Q}^\ast$.

Corresponding Lean artifacts

Each AGM-R function has a Lean counterpart in formal/lean/Sagrada/:

License

AGM-R is MIT-licensed. The intent is that any researcher, LLM-training lab, or system-builder can take AGM-R as a reference substrate and build in the same family. Sagrada the product remains proprietary; AGM-R the science is open.