PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval

Abstract

Retrieval-augmented generation is usually formulated as a statistical information-retrieval problem. Graph-based variants add relational structure, but the mathematical status of that structure is often left underspecified. Three distinct questions tend to be conflated: which statements are certified as knowledge, which latent representations are useful for retrieval, and which multi-hop compositions are semantically admissible. We propose Proof-Carrying Algebraic-Geometric Retrieval (PAGR), a framework that separates these questions mathematically. Its symbolic layer is a many-sorted relational theory generated by a typed quiver, path equations, and positive Horn inclusions. A quiver representation assigns inner-product spaces to entity types and linear operators to relations. A cellular sheaf measures local-to-global consistency. Semiring provenance records derivations and supports machine-checkable certificates. The central principle is epistemic separation: learned geometry may rank and organize evidence, but cannot promote a hypothesis to certified ground truth. We show the certification criterion is invariant under arbitrary replacement of learned components. Further results include a conditional completeness bound, identification of the isometry group as the relevant symmetry for residual-based retrieval, a cohomological consistency diagnostic, and a bounded-bisimulation index for admissible-path expansion. PAGR is a mathematical architecture for separating where a system should look from what it is allowed to treat as knowledge.