agm-r 0.2.2

AGM-R: theorem-minimum reference implementation of AGM belief-revision primitives (T-I1, T-I2, T-M1).

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

Theorem	AGM-R location	What it proves	What the code does
T-I1	(implicit — AGM-R's channel type is not KSubset n k)	Flat-text retrieval over a $k$-passage budget is capped at $\log_2 \binom{n}{k}$ bits	AGM-R's query output type is Answer, not KSubset — it escapes T-I1's H1 by design
T-I2	sigma.py (6 primitives) + queries.py (8 compositions)	A finite composition of typed graph operations saturates $H(\mathrm{qDist})$ on $\mathcal{Q}^\ast$	Every query dispatches to a composition of {aggregate, filter, count, provenance, temporal, compose}
T-M1	postulates.py + operations.py::verify_postulates	Six AGM postulate classes are minimum sufficient	Each operation post-condition checks exactly the six classes; drop any one and an ablation test fails
T-5	(implicit — queries depend only on graph topology)	Error under $\varepsilon$-perturbation is graph-Lipschitz	AGM-R's queries ignore the claim_text free text; they act on the belief graph only
T-C1	operations.py::retract	Art. 17 compliance requires Vacuity-for-Retract + DerivesFrom-closure propagation	Retract propagates over DerivesFrom*; non-propagating retract fails T-C1's companion theorem (and the test_t_c1_propagation test)
T-R1-min	(by construction)	No universal-construction shortcut to AGM-compliance	AGM-R's KnowledgeGraph cannot be instantiated without the six postulate invariants holding on its operation history

Files

File	Role	LoC
types.py	Belief, Source, Relation, KnowledgeGraph — the data types	~100
postulates.py	The six AGM postulate classes as predicates	~150
operations.py	assert_belief, revise, refine, retract, relate	~200
sigma.py	The $\Sigma$-signature from T-I2: 6 composable primitives	~80
queries.py	The 8 structural query types built from $\Sigma$	~150
tests/	One test per postulate, one per query type, one per operation	~250

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 that the paper calls 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 (§5.3 of the paper):

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/:

AGM-R function	Lean theorem / definition	File
postulates.closure_check	Sagrada.AGM.Closure	Sagrada/AGM/Closure.lean
postulates.vacuity_for_retract	t_c1_art17_necessity	Sagrada/Foundations/ComplianceTraceability.lean
operations.retract closure prop	t_c1_companion_flat_memory_violation	ibid
sigma.aggregate / sigma.count	CompositionWitness	Sagrada/Info/RetrievalAchievability.lean
queries.revision_count	t_m1_belief_membership_instance_K2	Sagrada/AGM/Minimality.lean

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.