Metadata-Version: 2.4
Name: agm-r
Version: 0.2.2
Summary: AGM-R: theorem-minimum reference implementation of AGM belief-revision primitives (T-I1, T-I2, T-M1).
Author-email: Mars Ausili <mars@cruxia.ai>
License-Expression: MIT
Project-URL: Homepage, https://github.com/Cruxia-AI/agm-r
Project-URL: Repository, https://github.com/Cruxia-AI/agm-r
Keywords: agm,belief-revision,epistemic,provenance,retrieval
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Operating System :: OS Independent
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Requires-Python: >=3.10
Description-Content-Type: text/markdown
Provides-Extra: dev
Requires-Dist: pytest>=7; extra == "dev"

# 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

```python
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.

```python
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`](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):

```bash
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.
