Paper deep dive
PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval
Xingting Wang, Min Wu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 9/9/2026, 5:49:37 AM
Summary
The paper introduces Proof-Carrying Algebraic-Geometric Retrieval (PAGR), a mathematical framework for Retrieval-Augmented Generation (RAG) that separates certified symbolic knowledge from learned geometric representations. Using typed quivers, path algebras, cellular sheaves, and semiring provenance, PAGR ensures that while geometry aids in retrieval and ranking, only facts derived via sound symbolic rules and source-attested evidence are treated as certified ground truth. This epistemic separation prevents learned models from promoting hypotheses to facts, providing mathematical guarantees for soundness, consistency, and provenance in LLM retrieval systems.
Entities (8)
Relation Signals (7)
PAGR → enforces → Epistemic Separation
confidence 95% · The central principle is epistemic separation: learned geometry may rank and organize evidence, but cannot promote a hypothesis to certified ground truth.
PAGR → uses → Cellular Sheaf
confidence 95% · A cellular sheaf measures local-to-global consistency.
PAGR → uses → Semiring Provenance
confidence 95% · Semiring provenance records derivations and supports machine-checkable certificates.
PAGR → uses → Typed Quiver
confidence 95% · Its symbolic layer is a many-sorted relational theory generated by a typed quiver
Cellular Sheaf → measures → local-to-global consistency
confidence 90% · A cellular sheaf measures local-to-global consistency.
Semiring Provenance → records → derivations
confidence 90% · Semiring provenance records derivations and supports machine-checkable certificates.
Knowledge Graph Embedding → isconflatedwith → Certified Knowledge
confidence 80% · But a small embedding distance is not a proof that a relation is true.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2609.06127v1
- Canonical: https://arxiv.org/abs/2609.06127v1
Trouble viewing inline? Open PDF directly →
Full Text
136,116 characters extracted from source content.
Expand or collapse full text
PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval Xingting Wang Affiliation: Department of Mathematics, Louisiana State University, Baton Rouge, LA 70803, USA xingtingwang@lsu.edu Min Wu Affiliation: Independent Researcher min.wu.2020@gmail.com September 2026 Abstract Retrieval-augmented generation (RAG) is usually formulated as a statistical information-retrieval problem: a query is embedded, nearby text is retrieved, and a language model is conditioned on the result. Graph-based RAG adds relational structure, but the mathematical status of that structure is often underspecified. In particular, three distinct questions are frequently conflated: which statements are certified as knowledge, which latent representations are useful for retrieval, and which multi-hop compositions are semantically admissible. We propose a use-case-agnostic framework called Proof-Carrying Algebraic-Geometric Retrieval (PAGR), which separates and then couples these questions through four mathematical layers. The symbolic layer is a finite many-sorted relational theory generated by a typed quiver, path equations, and positive Horn inclusions. The algebraic representation layer maps the quiver into finite-dimensional inner-product spaces, so relation types act as linear operators and compositional constraints become operator identities or regularizers. The geometric layer equips entity types with metric or mixed-geometry representation spaces for semantic seeding and inductive retrieval. The sheaf layer encodes local compatibility and supplies a local-to-global consistency energy. A fifth, orthogonal mechanism—semiring provenance—attaches machine-checkable derivation certificates to symbolic inferences. The central architectural constraint is an epistemic separation principle: learned geometry may rank, propose, and organize evidence, but it may not promote a hypothesis into certified ground truth. Certification is reserved for source-attested base facts and derivations admitted by a sound symbolic theory. We formalize this distinction and prove four results: a non-interference theorem stating that the certification boundary—the criterion by which a retrieved fact qualifies as certified—is invariant under arbitrary replacement of every learned component, even though which certified facts are retrieved is not, and from which soundness relative to an intended model follows as a corollary; a conditional completeness bound that characterizes exactly which certified facts geometric seeding can fail to reach; a gauge-invariance theorem identifying the isometry group—rather than the full base-change group—as the symmetry that retrieval scores actually respect; and a proposition showing that zero sheaf energy on a retrieved subgraph forces all declared path equations to hold along it, which couples the sheaf and representation layers instead of leaving them parallel. Three further groups of results sharpen and delimit the construction. Sheaf cohomology separates whether a particular retrieved configuration is consistent from whether any consistent configuration exists at all—the latter measured by the dimension of global sections, and assembled across overlapping neighborhoods by a Mayer–Vietoris gluing theorem. Bounded bisimulation yields a minimal index that decides admissible-path realizability exactly, while provenance decides which base facts are redundant. Finally, a scope theorem gives a structural criterion for when a schema leaves the finite and tame representation regimes, delimiting which classical tools the algebraic layer may legitimately invoke. We then define a hybrid retrieval operator combining metric seeding, admissible path expansion, provenance, representation residuals, sheaf consistency, and graph diffusion. The result is a mathematical blueprint for LLM retrieval systems in which geometry improves recall and organization while algebra and proof constrain what may be treated as ground truth. 1 Introduction Large language models possess broad parametric knowledge but provide weak guarantees about factuality, attribution, freshness, or the provenance of individual claims. Retrieval-augmented generation [39] addresses this by conditioning generation on external evidence. Modern graph-based variants extend retrieval from isolated chunks to relational neighborhoods, subgraphs, and multi-hop structures [16, 28, 32, 50, 27]. This is a substantial improvement for questions whose answers depend on relational context. Yet it leaves a foundational issue unresolved: a graph edge can mean at least three different things. First, an edge may be a certified assertion: a source explicitly states a relation. Second, an edge may be a logical consequence: it follows from certified assertions under a declared rule system. Third, an edge may be a statistical hypothesis: a learned model predicts that the relation is likely. These objects are useful for different purposes, but treating them as interchangeable makes the phrase “knowledge graph” mathematically ambiguous and makes “grounded generation” difficult to define. The same ambiguity appears in geometry. Knowledge-graph embedding (KGE) methods associate entities and relations with vectors, rotations, projections, tensors, or transformations and can model symmetry, inversion, hierarchy, and composition [8, 48, 46, 40, 49]. These representations are extremely useful for retrieval and link prediction. But a small embedding distance is not a proof that a relation is true. Conversely, a symbolic graph with no geometry can be exact but brittle: it may fail to retrieve semantically relevant regions when the user’s language does not match the graph’s vocabulary. This paper develops a mathematical framework in which symbolic and geometric knowledge coexist without being conflated. The framework is deliberately independent of any particular domain. It can represent scientific claims, software dependencies, corporate knowledge, legal authorities, biomedical facts, product catalogs, educational concepts, or any other corpus for which typed relations and source evidence exist. Our proposal uses several established theories, but assigns each a sharply delimited role: 1. Typed quivers and path algebras represent the grammar of relation composition. 2. Positive Horn rules and relational fixed points define certified symbolic closure. 3. Quiver representations assign vector spaces to types and linear maps to relation generators, making compositional geometry explicit. 4. Metric and mixed-geometry embeddings support semantic seeding and inductive ranking. 5. Cellular sheaves encode local compatibility and quantify whether local representations glue coherently. 6. Semiring provenance records derivations independently of any one numerical confidence convention. 7. Proof-carrying admission requires a checkable witness before an inferred statement may enter the certified retrieval context. None of these ingredients is new in isolation. Quiver representations are classical, have been used to analyze neural architectures [4, 18], and admit geometric moduli-space formulations [33]. Cellular sheaves have recently been used to generalize graph neural networks and knowledge-graph embeddings [29, 22, 10]. Provenance semirings provide a general algebra of derivations [26, 25]. The contribution here is a unified epistemic architecture for retrieval: symbolic truth, learned geometry, relational algebra, local consistency, and generative synthesis are explicitly separated and connected by typed interfaces. Core thesis. A mathematically trustworthy retrieval system should use geometry to answer where should we look?, algebra and logic to answer what compositions are admissible?, provenance to answer why is this conclusion present?, and a generator only to answer how should the certified context be communicated? 2 Related Work and Positioning 2.1 Graph-based retrieval augmented generation GraphRAG systems retrieve or construct graph-structured context rather than treating text chunks as independent units. Recent frameworks build LLM-derived entity graphs and summarize communities for global queries [16], retrieve textual subgraphs [32], expand seed chunks using graph neighborhoods [50], or run personalized PageRank from query-linked seeds over an extracted knowledge graph [27]; Han et al. [28] survey the space. Our Stage V is deliberately the same diffusion primitive used by Gutiérrez et al. [27], which makes the comparison sharp: the difference is not the diffusion but what the diffused subgraph is permitted to license. We adopt the high-level GraphRAG motivation but focus on a different problem: the semantics of graph edges and the conditions under which graph-derived information is admissible as ground truth. 2.2 Knowledge graph embeddings and relational geometry Latent KGE models encode relational regularities using algebraic transformations. TransE models relations as translations [8]; ComplEx uses complex-valued factorization and can capture symmetric and antisymmetric relations [48]; RotatE models relations as complex rotations and supports inversion and composition patterns [46]. More recent approaches use hyperbolic geometry for hierarchy [11], higher-dimensional orthogonal parameterizations, or mixed Euclidean/hyperbolic geometry [40, 49]. Theoretical work also shows that not every relation is equally representable under simple Euclidean embedding families [6]. Our framework therefore treats the choice of geometry as a model class, not as an ontological commitment. 2.3 Quivers, representations, and machine learning A quiver is a directed multigraph; a representation assigns a vector space to each vertex and a linear map to each arrow [14, 43]. Neural networks themselves can be described using quiver representations augmented with nonlinearities [4, 18]. We instead apply quiver representation theory to the knowledge schema: entity types are vertices, relation types are arrows, and learned relation operators form a representation of that schema. 2.4 Sheaf-theoretic knowledge representations Cellular sheaves attach vector spaces to cells and restriction maps to incidences; the spectral theory of the associated sheaf Laplacian is developed by Hansen and Ghrist [30]. Sheaf neural networks replace ordinary graph diffusion by a sheaf Laplacian, allowing edge-dependent and asymmetric compatibility structure [29, 7, 10]. Knowledge Sheaves formulates KGE as approximate global-section finding and uses schema constraints to model composite relations [22]. Section 10 makes the relationship to our representation layer explicit: the quiver representation is recovered as the special case in which restriction maps are tied by relation type rather than free per edge, and we show that this tying makes sheaf consistency imply representation-layer compositional consistency. We keep the sheaf layer epistemically subordinate to certified symbolic facts: sheaf consistency is evidence of representational coherence, not itself a proof of truth. 2.5 Provenance and proof-carrying computation Provenance semirings annotate base facts and propagate annotations through query derivations [26]; see Abiteboul et al. [1] for the underlying Datalog fixed-point semantics. Extensions address regular path queries and recursive Datalog semantics [25, 9, 2], and m-semirings equip the framework with a monus operator supporting deletion [23]. Our admission principle is conceptually related to proof-carrying code [41]: a consumer accepts an object only together with a mechanically checkable witness that it satisfies a declared policy. Here the object is an inferred fact rather than executable code. The invariance form of our central theorem (Section 12) is a non-interference statement in the sense of Goguen and Meseguer [24], with epistemic status playing the role of a security level. 2.6 Positioning against concurrent neuro-symbolic retrieval Two concurrent lines of work share our vocabulary and must be distinguished explicitly. Koomullil [37] propose proof-carrying certificates for LLM pipelines with a Lean 4 trust boundary, verifying the deterministic computation surrounding a model, including bilattice grounding and embedding-sensitivity certificates. That work is about kernel-checkable certificates for pipeline steps; ours is about the algebraic and geometric structure of the knowledge object being retrieved, and in particular about which multi-hop compositions are admissible. The two are complementary: a PAGR certificate δ is exactly the kind of artifact a Lean-style checker would consume. Gann and Gertz [19] synthesize attributable Prolog modules from retrieved chunks and obtain execution traces linking reasoning steps to sources; this realizes the provenance and certificate layers empirically, but does not separate the representation and consistency layers, does not type the composition grammar with a schema quiver, and does not address the geometric seeding stage. We regard NeSy-RAG as the closest empirical instantiation of Stages I–I and a natural baseline for the hypotheses in Section 22. Finally, citation-level generation evaluation [20] measures whether a generator’s claims are supported by its context; our Design Principles constrain what enters that context in the first place, so the two are orthogonal and should be reported together. 3 Mathematical Preliminaries 3.1 Typed quivers and the free path category Definition 3.1 (Typed schema quiver). A schema quiver is a finite directed multigraph Q=(Q0,Q1,s,t),Q=(Q_0,Q_1,s,t), where Q0Q_0 is a finite set of entity sorts, Q1Q_1 is a finite set of primitive relation types, and s,t:Q1→Q0s,t:Q_1→ Q_0 assign the source and target sort of each relation. A path p=an⋯a1p=a_n·s a_1 is a composable sequence of arrows with t(ai)=s(ai+1)t(a_i)=s(a_i+1). The length-zero path at i∈Q0i∈ Q_0 is denoted eie_i. Paths form the free category Path(Q)Path(Q) under concatenation. Fix a field k, usually ℝR or ℂC. Definition 3.2 (Path algebra). The path algebra kQkQ is the k-vector space with basis all finite paths in Q, equipped with bilinear multiplication given by concatenation when paths are composable and zero otherwise. The idempotents eie_i satisfy ei2=eie_i^2=e_i and eiej=0e_ie_j=0 for i≠ji≠ j. They encode the type decomposition algebraically. 3.2 Equations versus inclusions Two kinds of semantic constraint must be separated. Path equations. If two compositions are intended to denote the same operation, we may impose p=qp=q. Let J⊲kQJ kQ be the ideal generated by differences p−qp-q. Then Q=kQ/JA_Q=kQ/J is the corresponding quotient of the path algebra. This is the correct use of quotient/path-algebra machinery. Remark 3.3 (Admissibility). The classical theory of bound quiver algebras requires J to be admissible, i.e. Rm⊆J⊆R2R^m J R^2 for some m, where R⊲kQR kQ is the arrow ideal [14, 43]. Admissibility guarantees, among other things, that kQ/JkQ/J is finite dimensional and that Q is recovered as its Gabriel quiver. Some schema constraints of practical interest violate this condition. In particular the inverse-pair equations ba=eiba=e_i, ab=ejab=e_j of Section 14.2 involve length-zero paths and so generate a non-admissible ideal; kQ/JkQ/J is then a groupoid-algebra-like quotient rather than a bound quiver algebra. Nothing in this paper requires admissibility—we only ever use QA_Q through the factorization criterion of Proposition 8.2, which holds for an arbitrary two-sided ideal—but the classification results of representation theory should not be invoked unless J is admissible. We therefore write “quotient path algebra” rather than “bound path algebra” throughout. Relational inclusions. A rule such as R1;R2⊆R3R_1;R_2 R_3 does not assert equality of paths. It is a positive Horn implication. Such rules are handled in a relational semantics rather than by quotienting kQkQ. Design Principle 3.4 (Equation–inclusion separation). Use path-algebra quotients only for identities. Use Horn closure for one-way semantic implications. Conflating the two changes the meaning of the knowledge system. 3.3 Relational structures For each sort i∈Q0i∈ Q_0, let PiP_i be a finite set of entities. For an arrow a:i→ja:i→ j, a concrete relation is Ea⊆Pi×Pj.E_a P_i× P_j. Composition is ordinary relational composition. The collection of sets and relations lives in the locally ordered category Rel, where hom-sets are ordered by inclusion. 4 The PAGR Framework Definition 4.1 (PAGR knowledge system). A PAGR knowledge system is a tuple =(Q,P,E,,J,Φ,ρ,ℱ,η),K=(Q,P,E,T,J, ,ρ,F,η), where: 1. Q is a finite schema quiver; 2. P=⨆i∈Q0PiP= _i∈ Q_0P_i is the finite typed entity universe; 3. E=Eaa∈Q1E=\E_a\_a∈ Q_1 is the extensional base relation set; 4. T is a finite set of positive Horn relation rules; 5. J is an optional ideal of path equations; 6. Φ=ϕi:Pi→ℳi =\ _i:P_i _i\ embeds entities into metric or Riemannian spaces; 7. ρ is a finite-dimensional representation of the schema quiver; 8. ℱF is a cellular sheaf encoding local compatibility data; 9. η maps certified base facts to provenance generators and source evidence. This definition intentionally contains both discrete and continuous objects. Their responsibilities differ. E,,JE,T,J define certified symbolic semantics. Φ,ρ,ℱ ,ρ,F define retrieval and consistency geometry. η supplies evidence and derivation identity. 5 Certified Symbolic Semantics 5.1 The extensional base and closure Let ℜ R be the finite lattice of all typed relation families over P. A positive Horn rule has the form Ra1;⋯;Ram⊆Rb,R_a_1;·s;R_a_m R_b, possibly with repeated variables and type-compatible joins. Define the immediate-consequence operator T:ℜ→ℜT_T: R→ R by T(X)=X∪every tuple licensed by one application of a rule in to X.T_T(X)=X∪\every tuple licensed by one application of a rule in T to X\. Remark 5.1 (Inflationarity). T_T is inflationary: X⊆T(X)X T_T(X) for every X∈ℜX∈ R, since the definition retains all elements of X in the union. This is what makes the ascending chain below well-defined; it is stated separately because monotonicity alone does not imply it. Proposition 5.2 (Monotonicity). T_T is monotone: if X⊆YX Y, then T(X)⊆T(Y)T_T(X) T_T(Y). Proof. Every rule in T is positive: premises contain no negation. Any witness tuple satisfying a premise in X also satisfies it in Y. Hence every consequence added from X is also added from Y, and X⊆YX Y handles the copied part. ∎ Theorem 5.3 (Finite least closure). For finite P, the sequence E⊆T(E)⊆T2(E)⊆⋯E T_T(E) T_T^2(E) ·s stabilizes after finitely many steps at a unique least fixed point of T_T above E, Cl(E)=lfp(T).Cl_T(E)=lfp(T_T). Proof. The chain is ascending by Remark 5.1, and ℜ R is a finite lattice, so the chain stabilizes at some N≤|ℜ|N≤| R|; write F=TN(E)F=T_T^N(E), which satisfies T(F)=FT_T(F)=F and E⊆FE F. For minimality, let Y be any fixed point with E⊆YE Y. By induction, T0(E)=E⊆YT_T^0(E)=E Y, and if Tn(E)⊆YT_T^n(E) Y then monotonicity gives Tn+1(E)⊆T(Y)=YT_T^n+1(E) T_T(Y)=Y. Hence F⊆YF Y. (Equivalently, apply Knaster–Tarski to the monotone T_T on the finite lattice X∈ℜ:E⊆X\X∈ R:E X\.) ∎ Thus certified inference is deterministic and terminating on a finite knowledge base without appealing to learned representations; this is the standard fixed-point semantics of positive Datalog [1]. 5.2 Model-relative soundness Let M be a typed relational structure over the same signature, and write At()=f:f is a typed atomic statement and ⊧fAt( M)=\f:f is a typed atomic statement and M f\ for the set of atoms it satisfies. Comparing a derived fact set to At()At( M), rather than to M itself, keeps the containment statements below type-correct. Assumption 5.4 (Source correctness). There exists an intended relational model M such that E⊆At()E ( M). Assumption 5.5 (Rule soundness). Every rule in T is valid in M. Theorem 5.6 (Soundness of certified closure). Under Source Correctness and Rule Soundness, Cl(E)⊆At().Cl_T(E) ( M). Proof. Induct on the stage n of the fixed-point construction of Theorem 5.3. For n=0n=0, T0(E)=E⊆At()T_T^0(E)=E ( M) by Source Correctness. Suppose Tn(E)⊆At()T_T^n(E) ( M). A fact in Tn+1(E)∖Tn(E)T_T^n+1(E) T_T^n(E) is licensed by one application of a rule of T whose premises lie in Tn(E)T_T^n(E) and hence hold in M; Rule Soundness makes the conclusion hold in M. Since the chain stabilizes at Cl(E)Cl_T(E), the claim follows. ∎ The theorem is conditional, as it must be: mathematics cannot establish that a source is factually correct merely from the fact that it was ingested. What the theorem establishes is that the inference engine introduces no conclusions outside the declared semantics. 6 Epistemic Stratification and Ground Truth We now formalize the distinction between certified facts and model hypotheses. Definition 6.1 (Epistemic strata). For each typed atomic statement f, assign one of three statuses: (f)∈,,. status(f)∈\ base, derived, hypothesis\. • base: directly supported by admitted source evidence; • derived: belongs to Cl(E)Cl_T(E) and has a valid derivation certificate; • hypothesis: proposed by geometry, embedding, an LLM, a link predictor, or any process not licensed by T. Definition 6.2 (Certified ground-truth set). The internal certified knowledge set is the closure Cl(E)Cl_T(E) equipped with the status labelling G⋆=E⏟⊔(Cl(E)∖E)⏟,G = E_ base\; \; (Cl_T(E) E )_ derived, subject to the additional requirement that each derived member carry a valid proof object. Remark 6.3. As a set, G⋆=Cl(E)G =Cl_T(E), since E⊆Cl(E)E _T(E); the content of Definition 6.2 is the partition into strata and the proof-object requirement on the second block, not the union. We write it as a disjoint union to emphasize that the two blocks are governed by different admission mechanisms: evidence for base, derivation for derived. The complement ℜ∖G⋆ R G carries status hypothesis. The term “ground truth” throughout means certified relative to an explicit evidence protocol and a declared rule set, not metaphysical truth. This distinction is essential in dynamic or contested domains, and should be stated prominently in any system description. Design Principle 6.4 (No geometric promotion). No numerical score, embedding similarity, neural prediction, or LLM assertion can change a fact’s status from hypothesis to base or derived. Promotion requires new admitted evidence or a valid symbolic derivation. This principle is an architectural invariant rather than a statistical calibration rule. 6.1 Extraction is not attestation The principle above invites an immediate objection. In any realistic deployment the base set E is populated by running an information-extraction model—frequently an LLM—over a text corpus. If LLM assertions cannot become base facts, how does E acquire any members at all? Confronting this squarely is essential, because it is where most implementations of “grounded” retrieval quietly leak. The resolution is to distinguish two different propositions. Let σ be a source span. • Attestation: the span σ asserts f. This is a claim about the text, checkable in principle by re-reading σ. • Extraction: a model believes that σ asserts f. This is a statistical claim about the model. An extractor produces the second; the admission predicate must decide the first. The framework is therefore consistent with LLM-based ingestion provided that extraction output is treated as a hypothesis about attestation, and that the admission predicate applies an independent check—span-grounded verification, a second extractor with disagreement routing, human curation, or a schema-and-type validity test—before the pair (f,ϵf)(f, _f) enters E. Design Principle 6.5 (Attestation gate). An extractor may propose (f,σ)(f,σ) but may not admit it. Admission is the act of an evidence policy AdmitAdmit that is independent of the extractor and that binds f to a stable, re-checkable representation of σ. This weakens no theorem below. Soundness is stated relative to Source Correctness, and Source Correctness is now explicitly a property of the admission policy rather than of the extractor. The practical consequence is a measurable quantity: the attestation error rate of the admission policy, which should be reported as a first-class system statistic alongside retrieval metrics. 7 Provenance as a Derivation Algebra Assign each certified base fact e∈Ee∈ E an indeterminate xex_e. For positive relational queries, provenance can be represented in the polynomial semiring ℕ[X]N[X] [26]. Products represent joint use of premises and sums represent alternative derivations. Definition 7.1 (Proof provenance). For a derived fact f, let Prov(f)=∑δ∈D(f)∏e∈leaves(δ)xe,Prov(f)= _δ∈ D(f) _e (δ)x_e, where D(f)D(f) is the set of admitted finite derivations of f. For recursive rules, care is needed because derivation families may be infinite; semiring semantics for recursive Datalog require additional algebraic conditions or finite proof representations [9, 2]. In a bounded-retrieval implementation one may instead retain a finite derivation DAG up to depth h. Definition 7.2 (Proof-carrying fact). A proof-carrying fact is a pair (f,δ)(f,δ) where f is an atomic statement and δ is a finite derivation tree whose leaves resolve to admitted source evidence and whose internal nodes instantiate rules in T. Proposition 7.3 (Cheap verification). For fixed rule arity and an explicit finite derivation tree δ, verification of (f,δ)(f,δ) is linear in the size of δ plus the cost of resolving its leaves. This is the retrieval analogue of the proof-carrying design pattern [41]: inference may be computationally expensive, but consumption requires only proof checking. 8 Quiver Representations as Relational Geometry 8.1 Representation of the schema Definition 8.1 (Linear representation). A finite-dimensional representation ρ of Q assigns a finite-dimensional inner-product space ViV_i to each i∈Q0i∈ Q_0 and a linear map Aa:Vs(a)→Vt(a)A_a:V_s(a)→ V_t(a) to every arrow a∈Q1a∈ Q_1. For a path p=an⋯a1p=a_n·s a_1, define Ap=Aan⋯Aa1.A_p=A_a_n·s A_a_1. Thus relation composition is literal operator composition. If J is generated by path equations p−qp-q, the representation factors through kQ/JkQ/J precisely when Ap=AqA_p=A_q for every generator of J. Proposition 8.2 (Factorization criterion). Extend ρ linearly to kQkQ by r=∑iλipi↦Ar=∑iλiApir= _i _ip_i A_r= _i _iA_p_i. Then ρ descends to a module over Q=kQ/JA_Q=kQ/J if and only if Ar=0A_r=0 for every r∈Jr∈ J, and it suffices to check this on a generating set of J; equivalently, all declared path equations hold under ρ. Proof. A representation of Q is the same thing as a kQkQ-module, and a kQkQ-module descends to kQ/JkQ/J exactly when J annihilates it. Since ker(ρ) (ρ) is a two-sided ideal, J⊆ker(ρ)J (ρ) holds iff every generator of J lies in ker(ρ) (ρ). ∎ This gives the path algebra a concrete role in learning: exact path equations define hard constraints on the operators, while approximate equality defines structural regularizers. Let ℰJ=(p,q):p−q is a declared generator of JE_J=\(p,q):p-q is a declared generator of J\ be the finite set of declared path-equation pairs. Then ℒalg=∑(p,q)∈ℰJ‖Ap−Aq‖F2.L_alg= _(p,q) _J\|A_p-A_q\|_F^2. 8.2 Entity states For an entity x∈Pix∈ P_i, let zx∈Viz_x∈ V_i denote a learned or encoded state. A relational residual for a:i→ja:i→ j is ra(x,y)=‖Aazx−zy‖Vj.r_a(x,y)=\|A_az_x-z_y\|_V_j. Small residual means the representation predicts compatibility with relation a. It does not certify (x,a,y)(x,a,y) as true. 8.3 Gauge symmetry Choice of basis in each ViV_i is not semantically meaningful. Definition 8.3 (Unitary gauge transformation). For each i∈Q0i∈ Q_0, choose Ui∈U(Vi)U_i∈ U(V_i). Transform zx′=Uizx,Aa′=Ut(a)AaUs(a)−1.z_x =U_iz_x, A_a =U_t(a)A_aU_s(a)^-1. Theorem 8.4 (Gauge invariance of relational residuals). For unitary gauge transformations, ‖Aa′zx′−zy′‖=‖Aazx−zy‖.\|A_a z_x -z_y \|=\|A_az_x-z_y\|. More generally, the same holds for every path residual ‖Apzx−zy‖\|A_pz_x-z_y\|. Proof. For an arrow a:i→ja:i→ j, Aa′zx′−zy′=UjAaUi−1Uizx−Ujzy=Uj(Aazx−zy).A_a z_x -z_y =U_jA_aU_i^-1U_iz_x-U_jz_y=U_j(A_az_x-z_y). Unitary maps preserve norm. For a path p=an⋯a1p=a_n·s a_1 from i to j the operators telescope, Ap′=UjApUi−1A_p =U_jA_pU_i^-1, and the same computation applies. ∎ Design Principle 8.5 (Gauge-invariant retrieval). A retrieval criterion defined on a quiver representation should depend only on quantities invariant under the declared gauge group, not on arbitrary coordinate choices. This principle is useful when different encoders, checkpoints, or distributed components choose different internal bases. 8.4 Representation varieties: which group is the gauge group? For a dimension vector =(di)i∈Q0 d=(d_i)_i∈ Q_0, Rep(Q,)=∏a:i→jHom(kdi,kdj)Rep(Q, d)= _a:i→ jHom(k^d_i,k^d_j) is the affine representation space. The base-change group G=∏i∈Q0GL(di)G_ d= _i∈ Q_0GL(d_i) acts by simultaneous change of basis, and two points in the same G_ d-orbit are isomorphic as representations. Learned relation operators therefore live in a moduli problem, a viewpoint that has appeared in geometric analyses of neural networks and quiver varieties [33, 4, 18]. This orbit equivalence must not be conflated with the invariance established in Theorem 8.4; the distinction has practical consequences for system design. Remark 8.6 (The isometry subgroup, not the full base-change group). Theorem 8.4 holds for unitary UiU_i only. If g=(gi)∈Gg=(g_i)∈ G_ d is a general invertible base change, then ‖Aa′zx′−zy′‖=‖gj(Aazx−zy)‖,\|A_a z_x -z_y \|=\|g_j(A_az_x-z_y)\|, which differs from ‖Aazx−zy‖\|A_az_x-z_y\| unless gjg_j is an isometry. Consequently two representations that are isomorphic—the same point of the moduli space Rep(Q,)//GRep(Q, d)/\!\!/G_ d—can induce different retrieval rankings. Residual-based retrieval is invariant under Iso()=∏i∈Q0U(Vi)⊊G,Iso( d)= _i∈ Q_0U(V_i)\; \;G_ d, and the quotient by G_ d is strictly coarser than the equivalence that retrieval respects. Three responses are available, and a system should state which it adopts. (i) Fix the inner products and declare Iso()Iso( d) to be the gauge group, treating each ViV_i as an inner-product space rather than a bare vector space; the moduli-theoretic object is then a quotient by a compact group and Theorem 8.4 is exactly right. (i) Parameterize relation operators inside the orthogonal or unitary group by construction, as orthogonally parameterized KGE models do [40]; then IsoIso-invariance is structural. (i) Report scores that are genuinely G_ d-invariant—ranks, kernel and image dimensions, or residuals normalized by learned metrics that transform covariantly—accepting a weaker but coordinate-free criterion. Option (i) is our default, and it is what Design Principle 6 in Appendix B asks implementations to log. We do not claim that classification of indecomposable representations is needed for retrieval. The useful consequence is narrower: quiver representation theory supplies the correct object for typed linear relation operators and exposes their symmetries—including, as Remark 8.6 shows, the fact that the naive symmetry group is the wrong one. 9 Metric and Mixed-Geometry Semantic Spaces The representation ρ captures relational transformations. Semantic retrieval additionally requires a notion of proximity. For each type i, let (ℳi,di)(M_i,d_i) be a metric space and ϕi:Pi→ℳi _i:P_i _i an entity embedding (the maps Φ=ϕi =\ _i\ appear in the PAGR tuple of Definition 4.1). A text query q is mapped by type-specific query encoders ψi:→ℳi _i:Q _i, where Q is the space of queries; these are auxiliary inference-time maps and need not be part of the stored system tuple. The geometry need not be uniformly Euclidean. Hierarchical relations often motivate hyperbolic components; cyclic or rotational patterns motivate spherical or complex geometry; modern KGE systems increasingly use richer or mixed geometries [46, 40, 49]. Definition 9.1 (Product geometry). Let ℳi=ℳi(1)×⋯×ℳi(m)M_i=M_i^(1)×·s×M_i^(m) with component distances di(r)d_i^(r). A weighted product metric is di2(x,y)=∑r=1mλrdi(r)(xr,yr)2,λr≥0.d_i^2(x,y)= _r=1^m _rd_i^(r)(x_r,y_r)^2, _r≥ 0. This makes “geometric knowledge graph” precise: geometry is a family of metric representation spaces connected by typed relational operators, not merely a generic vector index. 9.1 Cross-type score commensurability Type-specific geometry creates a difficulty that a single global embedding space does not have, and it must be resolved before any statement about top-k retrieval is meaningful. A raw distance di(ψi(q),ϕi(x))d_i( _i(q), _i(x)) in ℳiM_i and a raw distance dj(ψj(q),ϕj(y))d_j( _j(q), _j(y)) in ℳjM_j are numbers in incomparable units: the spaces may have different dimensions, different curvature, and different diameter. Selecting a top-k set over the whole entity universe P=⨆iPiP= _iP_i by comparing such numbers directly is not well defined. We therefore require an explicit calibration step. Definition 9.2 (Calibrated semantic score). For each type i let FiF_i be the cumulative distribution function of di(ψi(q),ϕi(x))d_i( _i(q), _i(x)) over a reference population of entities of type i. The calibrated score is sgeo(q,x)=πi⋅(1−Fi(di(ψi(q),ϕi(x)))),x∈Pi,s_geo(q,x)= _i· (1-F_i (d_i( _i(q), _i(x)) ) ), x∈ P_i, where πi≥0 _i≥ 0 is a type prior with ∑iπi=1 _i _i=1. Composing with FiF_i maps every type into the common unit interval, so cross-type comparison ranks entities by within-type extremeness weighted by a declared type prior. Any strictly decreasing calibration would serve; the point is that some choice must be declared, since the choice is a modeling commitment and not a normalization detail. All subsequent statements about Sk(q)S_k(q) refer to sgeos_geo in the sense of Definition 9.2. 9.2 Inductive seeding for unseen entities Transductive embeddings assign a vector only to entities present at training time, which is a poor fit for a knowledge base whose base set E grows through the admission protocol of Section 16. Two mechanisms keep seeding usable for entities added after training, and neither disturbs the epistemic strata. First, an entity of type i that has a textual or otherwise featurized description can be embedded directly by ϕi _i whenever ϕi _i is a feature encoder rather than a lookup table; this is the inductive case in the strict sense. Second, a new entity with no usable features but with certified incident edges can be seeded structurally: subgraph-reasoning methods predict relations from the local structure around a candidate pair without entity-specific embeddings [47], and relation-graph methods transfer relation representations to graphs with unseen entities and unseen relation vocabularies [38]. Both mechanisms produce seeds, not facts. An inductively embedded entity enters Stage I exactly as any other entity does, and any relation predicted about it carries status hypothesis until admitted. The value of inductive capability in this architecture is therefore confined to recall, which is precisely where the framework intends learned components to operate. 9.3 Top-k stability Let sq(x)s_q(x) be a retrieval score, larger being better, obtained as in Definition 9.2. Theorem 9.3 (Margin stability of geometric seeding). Assume a perturbation changes every entity score by at most ε : |sq′(x)−sq(x)|≤ε.|s_q (x)-s_q(x)|≤ . Let x(k)x_(k) and x(k+1)x_(k+1) denote the kkth and (k+1)(k+1)st ranked entities under sqs_q. If sq(x(k))−sq(x(k+1))>2ε,s_q(x_(k))-s_q(x_(k+1))>2 , then the top-k seed set is unchanged under the perturbation. Proof. The strict margin implies that the top-k set is uniquely determined under sqs_q. Let x be ranked in the top k and x′x outside it, so that sq(x)≥sq(x(k))s_q(x)≥ s_q(x_(k)) and sq(x′)≤sq(x(k+1))s_q(x )≤ s_q(x_(k+1)). Then sq′(x)≥sq(x)−ε≥sq(x(k))−εandsq′(x′)≤sq(x′)+ε≤sq(x(k+1))+ε.s_q (x)\ ≥\ s_q(x)- \ ≥\ s_q(x_(k))- s_q (x )\ ≤\ s_q(x )+ \ ≤\ s_q(x_(k+1))+ . The hypothesis sq(x(k))−sq(x(k+1))>2εs_q(x_(k))-s_q(x_(k+1))>2 rearranges to sq(x(k))−ε>sq(x(k+1))+εs_q(x_(k))- >s_q(x_(k+1))+ , hence sq′(x)>sq′(x′)s_q (x)>s_q (x ) for every such pair. No boundary crossing occurs and the top-k set is unchanged. ∎ This gives a concrete robustness diagnostic for semantic retrieval: report the boundary margin, not only the nearest-neighbor scores. The scope of the guarantee should be noted. It concerns stability of the seed set under score perturbation, and says nothing about whether the seed set is correct: a systematically biased encoder is perfectly stable. Stability and recall are separate quantities; Section 12 characterizes the latter. 10 Cellular Sheaves as Local-to-Global Consistency A quiver representation says how relation types act globally. A cellular sheaf can encode edge-specific compatibility between local states. Let G=(V,EG)G=(V,E_G) be an undirected support graph obtained from certified or candidate relations. A cellular sheaf ℱF assigns a vector space ℱ(v)F(v) to each vertex, a vector space ℱ(e)F(e) to each edge, and restriction maps ℱv⊴e:ℱ(v)→ℱ(e)F_v e:F(v) (e) for each incidence v⊴ev e. A 00-cochain is x=(xv)v∈V∈C0(G,ℱ)=⨁vℱ(v)x=(x_v)_v∈ V∈ C^0(G;F)= _vF(v). The coboundary on an oriented edge e=(u,v)e=(u,v) is (δx)e=ℱv⊴exv−ℱu⊴exu.(δ x)_e=F_v ex_v-F_u ex_u. The sheaf Laplacian is Lℱ=δ∗δ.L_F=δ δ. Definition 10.1 (Sheaf consistency energy). ℰℱ(x)=⟨x,Lℱx⟩=‖δx‖2.E_F(x)= x,L_Fx =\|δ x\|^2. Proposition 10.2 (Zero-energy consistency). ℰℱ(x)=0⟺δx=0.E_F(x)=0 δ x=0. Hence zero-energy 00-cochains are exactly global sections, kerLℱ=H0(G,ℱ) L_F=H^0(G;F). Proof. Since Lℱ=δ∗δL_F=δ δ, ⟨x,Lℱx⟩=⟨δx,δx⟩=‖δx‖2, x,L_Fx = δ x,δ x =\|δ x\|^2, which vanishes exactly when δx=0δ x=0. ∎ This is the standard positive-semidefiniteness argument for the sheaf Laplacian [30] and we record it only to fix notation; the substantive content of this section is the coupling established below. 10.1 The representation-induced sheaf As defined so far, the sheaf layer and the representation layer are two separate assignments of vector spaces to combinatorial data, and the sheaf energy appears to be an independent add-on. This section shows they are not independent. Take the support graph G to have one edge e per certified relation instance, and let λ(e)∈Q1λ(e)∈ Q_1 be its relation label. Definition 10.3 (Sheaf induced by a representation). Given ρ, define ℱρF^ρ by ℱρ(v)=Vτ(v)F^ρ(v)=V_τ(v) for a vertex of sort τ(v)τ(v), ℱρ(e)=Vt(λ(e))F^ρ(e)=V_t(λ(e)) for an edge, and, for e an instance of a:i→ja:i→ j oriented from u to v, ℱu⊴eρ=Aa,ℱv⊴eρ=idVj.F^ρ_u e=A_a, ^ρ_v e=id_V_j. Under this construction (δx)e=xv−Aaxu(δ x)_e=x_v-A_ax_u, so the edgewise coboundary is exactly the relational residual rar_a of Section 8.2 and the sheaf energy is the sum of squared residuals over the subgraph. The general Knowledge Sheaves construction [22] allows both restriction maps to be free and relation-specific; Definition 10.3 is the special case in which restrictions are tied by relation type through ρ. That tying is what makes the following proposition available. Proposition 10.4 (Sections certify path equations on their support). Let x be a global section of ℱρF^ρ on a subgraph H⊆GH G, i.e. ℰℱρ(x|H)=0E_F^ρ(x|_H)=0. Let p=an⋯a1p=a_n·s a_1 be a path in the schema and suppose u0,u1,…,unu_0,u_1,…,u_n is a sequence of vertices of H with each (um−1,um)(u_m-1,u_m) an edge of H labelled ama_m. Then Apxu0=xun.A_p\,x_u_0=x_u_n. Consequently, if p and q are two such realized paths in H with common endpoints u0u_0 and w, then (Ap−Aq)xu0=0,(A_p-A_q)\,x_u_0=0, so every declared path equation of ℰJE_J realized in H holds when applied to the section. Proof. Zero energy gives δx=0δ x=0, hence xum=Aamxum−1x_u_m=A_a_mx_u_m-1 for each edge of H by Definition 10.3. Induction on m yields xum=Aam⋯Aa1xu0x_u_m=A_a_m·s A_a_1x_u_0, and m=nm=n is the first claim. For the second, apply the first to p and to q and subtract, using xw=Apxu0=Aqxu0x_w=A_px_u_0=A_qx_u_0. ∎ Proposition 10.4 converts the sheaf layer from a decorative addition into a diagnostic with a stated meaning. Low sheaf energy on a retrieved neighborhood is evidence that the representation layer’s compositional constraints are being respected on that neighborhood, which is a statement about ℒalgL_alg localized to the retrieved region rather than averaged over training. The converse fails, and usefully so: Ap=AqA_p=A_q as operators does not imply that any particular 00-cochain is a section, so the two diagnostics are genuinely different measurements. Remark 10.5 (Scope of the certification). The proposition is a statement about the section, not about the operators. It asserts (Ap−Aq)xu0=0(A_p-A_q)x_u_0=0, not Ap=AqA_p=A_q as operators. A retrieved subgraph can therefore have zero sheaf energy while the declared path equation fails outside the span of the observed entity states. This is the appropriate strength for a retrieval-time diagnostic: the system observes only finitely many entity states, and the guarantee is local to them. In PAGR, we use the energy as a consistency signal: a retrieved subgraph with high local disagreement can be down-ranked, flagged, or split before generation. Design Principle 10.6 (Consistency is not truth). Low sheaf energy indicates that local representations agree under the chosen restrictions. It does not imply that the underlying factual assertions are correct. 10.2 Sheaf cohomology and section-existence The coboundary δ:C0(G,ℱ)→C1(G,ℱ)δ:C^0(G;F)→ C^1(G;F), where C1(G,ℱ)≔⨁e∈EGℱ(e),C^1(G;F)\; \; _e∈ E_GF(e), is the first differential of the cellular cochain complex. Because G is a graph (a one-dimensional CW complex), the complex terminates at degree 11: 0⟶C0(G,ℱ)→C1(G,ℱ)⟶ 0,0\; \;C^0(G;F)\; \;δ\;\;C^1(G;F)\; \;0, with cohomology groups H0(G,ℱ) H^0(G;F) =kerδ(global sections; cf. Proposition 10.2), \;=\; δ (global sections; cf.\ Proposition~ prop:zero-energy), H1(G,ℱ) H^1(G;F) =C1(G,ℱ)/im(δ). \;=\;C^1(G;F)\,/\,im(δ). The primary diagnostic built from these groups is H0H^0, not H1H^1. Definition 10.7 (Consistency dimension). The consistency dimension of a retrieved subgraph H⊆GH G under ρ is σρ(H)≔dimkH0(H,ℱρ|H). _ρ(H)\; \; _kH^0(H;F^ρ|_H). So σρ(H)>0 _ρ(H)>0 means that a nonzero globally consistent entity-state assignment exists on H, and σρ(H)=0 _ρ(H)=0 means that the zero cochain is the only one. In general σρ(H) _ρ(H) is computed directly as dimkerδ δ, a rank computation on the coboundary; no further structure is assumed, and in particular the relation operators AaA_a need not be invertible. When they are, the quantity acquires a classical interpretation. Proposition 10.8 (Holonomy form under invertible transport). Suppose every relation operator realized on a connected H is an isomorphism. Then ℱρ|HF^ρ|_H is a local system: all restriction maps are invertible, since ℱv⊴eρ=idF^ρ_v e=id and ℱu⊴eρ=AaF^ρ_u e=A_a. Fixing a base vertex v0v_0, transport along any closed walk γ based at v0v_0 is a well-defined automorphism HolγHol_γ of Vτ(v0)V_τ(v_0), and restriction to the base stalk identifies global sections with holonomy-invariant base states: σρ(H)=dim⋂γ∈π1(H,v0)ker(Holγ−I), _ρ(H)\;=\; \!\! _γ∈ _1(H,v_0)\!\! (Hol_γ-I ), where π1(H,v0) _1(H,v_0) is free of rank c, so the intersection may be taken over the c fundamental cycles of a spanning tree. Proof. A section is determined by its value at v0v_0, since invertibility lets one transport uniquely along every edge of a spanning tree in either direction; and a base state extends consistently to a section precisely when it is unchanged by transport around each independent cycle. ∎ Remark 10.9 (Why invertibility is needed for the holonomy form, but not for σρ _ρ). Without invertibility the holonomy statement is unavailable, and not merely unproved. Transport along a spanning tree may require traversing an edge against its direction, which asks for a preimage under AaA_a that need neither exist nor be unique; and the round-trip operator of a cycle is undefined when an operator along it is singular. Take H with sorts u,v,wu,v,w, two relations u→wu→ w realized by AaA_a and AcA_c, and one relation v→wv→ w realized by AbA_b: every spanning tree of H¯ H reaches v through w, so tree propagation cannot even begin unless AbA_b is invertible, and the holonomy of the u–w cycle would be Ac−1AaA_c^-1A_a. The consistency dimension is nevertheless perfectly well defined in this case and is computed from δ as usual. This is why Definition 10.7 is stated as dimH0 H^0 rather than through holonomy: the rank computation is the general object, and Proposition 10.8 is the special case that explains what it measures. Remark 10.10 (Why H1H^1 is not the consistency diagnostic). On a graph with ∑vdτ(v)=∑edt(λ(e)) _vd_τ(v)= _ed_t(λ(e))—the balanced case, typical when all sorts have the same embedding dimension—the Euler characteristic identity dimH0−dimH1=0 H^0- H^1=0 forces σρ(H)=dimH1(H,ℱρ|H) _ρ(H)= H^1(H;F^ρ|_H). In a triangle with consistent operators (Ac=AbAaA_c=A_bA_a) and stalks k3k^3, for instance, σρ=3 _ρ=3 and dimH1=3 H^1=3; with generic inconsistent operators, σρ=0 _ρ=0 and dimH1=0 H^1=0. So H1>0H^1>0 co-occurs with existence of consistent configurations, not their absence. More generally, when edge stalks outweigh vertex stalks (χ<0χ<0), the identity forces dimH1≥σρ+|χ|>0 H^1≥ _ρ+|χ|>0 regardless of the operators, making H1>0H^1>0 vacuous as a diagnostic. The role of H1H^1 in this framework is topological: it measures the excess of overlap sections over those explainable by restriction from local sections, which is a property of the graph’s cycle structure and the relative operator images rather than of operator consistency directly. The next theorem covers the multi-seed setting: Stage I expands each seed to a local acyclic neighborhood, and the question is whether neighborhoods from distinct seeds can be assembled consistently. Its hypothesis is that the individual neighborhoods have vanishing H1H^1, and that condition requires care: it does not follow from acyclicity alone. Lemma 10.11 (Vanishing on expansion forests). Let H⊆GH G be a forest in which no vertex is the head of two edges—for instance an expansion tree produced by Stage I from a single seed, in which each reached entity is recorded together with one witnessing traversal. Then H1(H,ℱρ|H)=0H^1(H;F^ρ|_H)=0. Proof. By Definition 10.3 the restriction at the head of an edge e=(u,v)e=(u,v) labelled a is ℱv⊴eρ=idVt(a)F^ρ_v e=id_V_t(a), so (δx)e=xv−Aaxu(δ x)_e=x_v-A_ax_u. Given c∈C1(H,ℱρ)c∈ C^1(H;F^ρ), root each component of H and traverse outward. Each non-root vertex v is the head of exactly one edge e=(u,v)e=(u,v), and u has already been assigned, so setting xv≔ce+Aaxux_v c_e+A_ax_u assigns every vertex exactly once and gives (δx)e=ce(δ x)_e=c_e on every edge. Hence δ is surjective and H1=0H^1=0. ∎ Remark 10.12 (Acyclicity alone is not sufficient). The in-degree hypothesis cannot be dropped. If two edges of H share a head, say u1→w←u2u_1 aw bu_2, then realizing a target (ce1,ce2)(c_e_1,c_e_2) requires xw∈(ce1+imAa)∩(ce2+imAb),x_w∈ (c_e_1+imA_a )∩ (c_e_2+imA_b ), which is empty for suitable c unless AaA_a and AbA_b are surjective. Taking Vi=k2V_i=k^2 for all three sorts and Aa,AbA_a,A_b of rank one gives dimH1=1 H^1=1 on this three-vertex tree. For a general cellular sheaf the situation is worse still, since neither restriction map need be surjective. An implementation that retains several witnessing traversals per reached entity should therefore verify H1(U,ℱρ|U)=H1(V,ℱρ|V)=0H^1(U;F^ρ|_U)=H^1(V;F^ρ|_V)=0 directly—a rank computation on δ—rather than infer it from acyclicity. Surjectivity of every AaA_a is a sufficient alternative hypothesis. Theorem 10.13 (Mayer–Vietoris gluing). Let H=U∪VH=U∪ V where U and V are retrieved neighborhoods satisfying H1(U,ℱρ|U)=H1(V,ℱρ|V)=0H^1(U;F^ρ|_U)=H^1(V;F^ρ|_V)=0—for instance expansion forests in the sense of Lemma 10.11. There is a short exact sequence of cochain complexes 0→C∙(H,ℱρ)→C∙(U,ℱρ)⊕C∙(V,ℱρ)→C∙(U∩V,ℱρ)→0,0→ C (H;F^ρ)→ C (U;F^ρ) C (V;F^ρ)→ C (U∩ V;F^ρ)→ 0, whose associated long exact sequence in cohomology, truncated using H1(U)=H1(V)=0H^1(U)=H^1(V)=0, gives 0→H0(H,ℱρ)→H0(U,ℱρ)⊕H0(V,ℱρ)→H0(U∩V,ℱρ)→∂H1(H,ℱρ)→ 0,0\;→\;H^0(H;F^ρ)\;→\;H^0(U;F^ρ) H^0(V;F^ρ)\; \;r\;\;H^0(U∩ V;F^ρ)\; \;∂\;\;H^1(H;F^ρ)\;→\;0, where r(sU,sV)=sU|U∩V−sV|U∩Vr(s_U,s_V)=s_U|_U∩ V-s_V|_U∩ V. Consequently: (i) A pair of local sections (sU,sV)∈H0(U,ℱρ)⊕H0(V,ℱρ)(s_U,s_V)∈ H^0(U;F^ρ) H^0(V;F^ρ) extends to a global section on H if and only if sU|U∩V=sV|U∩Vs_U|_U∩ V=s_V|_U∩ V. (i) σρ(H)=dimker(r) _ρ(H)= (r): the consistency dimension of H equals the number of independent ways local sections on U and V can be consistently matched on their overlap. (i) H1(H,ℱρ)≅H0(U∩V,ℱρ)/im(r)H^1(H;F^ρ) H^0(U∩ V;F^ρ)/im(r): a topological residual measuring how much the overlap’s section space exceeds what restriction from U and V can reach. Proof. The short exact sequence of cochain complexes is standard: in degree 00, C0(H,ℱρ)↪C0(U,ℱρ)⊕C0(V,ℱρ)↠C0(U∩V,ℱρ)C^0(H;F^ρ) C^0(U;F^ρ) C^0(V;F^ρ) C^0(U∩ V;F^ρ) is the restriction sequence, exact because every function on U∩VU∩ V extends to U and V separately (the sheaf assigns spaces to vertices and edges, so surjectivity holds by definition). In degree 11, both sides are edge-stalk direct sums and the same argument applies. The long exact sequence is then the standard algebraic consequence [13]. Truncation at H1(U)=H1(V)=0H^1(U)=H^1(V)=0 yields the displayed five-term sequence. Claim (i) is exactness at H0(U,ℱρ)⊕H0(V,ℱρ)H^0(U;F^ρ) H^0(V;F^ρ) and the identification of the kernel of r with H0(H,ℱρ)H^0(H;F^ρ). Claims (i) and (i) follow from the five-term sequence by definition. ∎ The Euler characteristic identity σρ(H)−dimH1(H,ℱρ)=∑v∈Hdτ(v)−∑e∈Hdt(λ(e))≕χ(H,ℱρ) _ρ(H)- H^1(H;F^ρ)\;=\; _v∈ Hd_τ(v)- _e∈ Hd_t(λ(e))\; \;χ(H;F^ρ) is computable from the schema dimension vector alone, independently of ρ. When χ≥0χ≥ 0 it implies σρ(H)≥dimH1(H,ℱρ)≥0 _ρ(H)≥ H^1(H;F^ρ)≥ 0; when χ<0χ<0 it forces dimH1≥|χ|>0 H^1≥|χ|>0 regardless of operators, which is why H1H^1 is not a useful consistency signal in that regime. Remark 10.14 (Two-tier consistency diagnosis). The two diagnostics are complementary. ℰℱρ(x)=0E_F^ρ(x)=0 witnesses that a specific observed configuration x is globally consistent. σρ(H)>0 _ρ(H)>0 certifies that a globally consistent configuration exists in principle, independently of which particular entity states are observed: it is a property of the operators Aa\A_a\ and the graph topology together. A retrieved context with σρ(H)>0 _ρ(H)>0 but positive observed energy indicates that the entity states are not yet in a consistent configuration, but one exists and could be recovered by adjusting them (a training or inference task). A context with σρ(H)=0 _ρ(H)=0 certifies that no nonzero globally consistent assignment exists for the current operators—the zero cochain is always a section—which is a structural operator-inconsistency rather than a configurational gap. Reporting both ℰℱρE_F^ρ and σρ _ρ is therefore more informative than energy alone. 11 A Unified Retrieval Operator We now combine the layers without collapsing them. Let q be a query. 11.1 Stage I: geometric seeding For each eligible entity x, compute a semantic score sgeo(q,x)s_geo(q,x). Select Sk(q)=TopKx∈Psgeo(q,x).S_k(q)=TopK_x∈ Ps_geo(q,x). This stage maximizes semantic recall and may use dense text encoders, type-aware embeddings, or mixed geometry. 11.2 Stage I: admissible symbolic expansion Let L⊆Q1∗L Q_1 be a regular language of allowed relation-label paths and let h be a hop bound. For a path p=an⋯a1p=a_n·s a_1 in the schema write Cl(E)p=Cl(E)an∘⋯∘Cl(E)a1⊆Ps(p)×Pt(p)Cl_T(E)_p\;=\;Cl_T(E)_a_n ·s _T(E)_a_1\; \;P_s(p)× P_t(p) for the relational composite of the certified closure along p, where Cl(E)aCl_T(E)_a denotes the a-component of the closure and ∘ is relational composition. Define ReachL,h(S)=y:∃x∈S,∃p∈L,|p|≤h,(x,y)∈Cl(E)p.Reach_L,h(S)=\y:∃ x∈ S,\ ∃ p∈ L,\ |p|≤ h,\ (x,y) _T(E)_p\. This is a bounded regular-path query over certified closure. Candidate/hypothesis edges may be explored in a separate channel but are never silently merged with this set. Remark 11.1 (Paths navigate; edges assert). A witness path p from x to y is a route, not an assertion: the framework does not claim that the composite relation p holds of (x,y)(x,y) unless T separately licenses that composite as an atom. Accordingly the certified retrieval output defined in Section 12 consists of the individual certified edges traversed, each of which is an element of Cl(E)Cl_T(E), together with the path structure presented as navigational metadata. Conflating the two would silently reintroduce the equation–inclusion confusion that Design Principle 3.4 rules out. 11.3 Stage I: proof attachment Every certified edge exposed by Stage I receives a certificate δ and provenance object Prov(⋅)Prov(·). Results without a valid certificate remain candidates rather than certified context. 11.4 Stage IV: geometric-algebraic scoring For a retrieved endpoint y, define components such as ssem(y) s_sem(y) =sgeo(q,y), =s_geo(q,y), spath(y) s_path(y) =g(|py|,type(py)), =g(|p_y|,type(p_y)), srep(y) s_rep(y) =exp(−βrpy(x,y)), = (-β r_p_y(x,y)), sprov(y) s_prov(y) =φ(Prov(y)), = (Prov(y)), scons(y) s_cons(y) =exp(−γℰℱ(x|Ny)). = (- _F(x|_N_y)). A ranking score may combine normalized components, Score(q,y)=∑jωjs~j(q,y),ωj≥0,Score(q,y)= _j _j s_j(q,y), _j≥ 0, subject to a hard epistemic gate: ranking cannot convert a hypothesis into a certified fact. 11.5 Stage V: graph diffusion Within the certified candidate subgraph, one may use personalized PageRank [34] or another diffusion score, as GraphRAG systems built on entity graphs already do [27]. Let W be the column-stochastic transition matrix of the certified candidate subgraph and vqv_q a probability distribution supported on seed nodes. (We use W rather than the more common P to avoid collision with the typed entity universe P=⨆iPiP= _iP_i.) The personalization equation πq=αWπq+(1−α)vq _q=α W _q+(1-α)v_q has the unique solution πq=(1−α)(I−αW)−1vq,0<α<1, _q=(1-α)(I-α W)^-1v_q, 0<α<1, where I−αWI-α W is invertible because α‖W‖1=α<1α\|W\|_1=α<1 bounds the spectral radius of αWα W. The vector vqv_q, rather than a nonexistent “query node,” is the mathematically natural personalization object; the seed distribution may be taken proportional to the calibrated scores of Definition 9.2 restricted to Sk(q)S_k(q). 11.6 Stage VI: generative synthesis The LLM receives a context package Cq=(f,source(f),δf,Prov(f),(f))C_q=\(f,source(f), _f,Prov(f), status(f))\ plus optional candidate hypotheses explicitly marked as such. The model may summarize, compare, explain, or abstain, but it is not the authority that determines membership in G⋆G . Algorithm 1 Proof-carrying geometric retrieval 1: query q, PAGR system K, seed count k, hop bound h 2: S←TopKx∈Psgeo(q,x)S _x∈ Ps_geo(q,x) 3: C←∅C← 4: for all x∈Sx∈ S do 5: for all admissible paths p∈Lp∈ L with |p|≤h|p|≤ h do 6: for all edges e traversed by a realization of p from x in Cl(E)Cl_T(E) do 7: construct or retrieve derivation certificate δe _e 8: if δe _e verifies then 9: compute provenance, representation residual, and consistency features for e 10: add the certified edge e to C, tagged with its witnessing path 11: end if 12: end for 13: end for 14: end for 15: rank C using gauge-invariant features and optional graph diffusion 16: return proof-carrying context CqC_q 12 Non-Interference, Soundness, and Conditional Completeness Collect the learned components into a single configuration θ=(Φ,ρ,ℱ,ω,LLM),θ=( ,ρ,F,ω,LLM), and let ℛcertθ(q)R^θ_cert(q) denote the set of atomic facts exposed to the generator as certified by Algorithm 1 under configuration θ (edges, in the sense of Remark 11.1). Write Θ for the space of all such configurations. The result below is often stated as a soundness theorem, but soundness is the weaker half of what the architecture actually buys. The stronger and more informative statement is an invariance property: the certification criterion is a function of the symbolic data alone, uniformly over Θ . This is a non-interference statement in the sense of Goguen and Meseguer [24], with epistemic status in place of a security level: no variation in the low-authority (learned) components can produce a variation in the high-authority (certified) predicate. Theorem 12.1 (Epistemic non-interference). For every query q, ⋃θ∈Θℛcertθ(q)⊆Cl(E). _θ∈ R^θ_cert(q)\; \;Cl_T(E). Equivalently, the criterion by which a retrieved fact qualifies as certified is invariant under arbitrary replacement of Φ , ρ, ℱF, the ranking weights ω, and the language model. Replacement may well change which certified facts are retrieved—the sets ℛcertθ(q)R^θ_cert(q) genuinely vary with θ, and Theorem 12.4 characterizes how—but not the standard a fact must meet to enter them: for every θ∈Θθ∈ and every f, f∈ℛcertθ(q)⟹f∈Cl(E),f ^θ_cert(q)\ \ f _T(E), and the predicate on the right-hand side does not depend on θ. Learned components may therefore alter whether a certified fact is retrieved, but not the criterion by which an exposed fact qualifies as certified. Proof. Fix θ. Learned components enter Algorithm 1 at exactly three points: the seed selection S←TopKsgeoS _geo, the computation of provenance, residual and consistency features, and the final ranking of C. The first only restricts which candidates are enumerated; the second and third only attach or reorder scores. None of the three adds an element to C, because the sole insertion into C is guarded by the verification test on δe _e. A certificate verifies only if its leaves resolve to admitted evidence and its internal nodes instantiate rules of T, which by Definition 6.2 and Theorem 5.3 witnesses membership in Cl(E)Cl_T(E). Since Cl(E)Cl_T(E) depends only on (E,)(E,T) and not on θ, the bound holds uniformly in θ, and taking the union over Θ preserves it. ∎ Corollary 12.2 (Retrieval soundness). Under Source Correctness and Rule Soundness, ℛcertθ(q)⊆At()R^θ_cert(q) ( M) for every query q and every configuration θ. Proof. Combine Theorem 12.1 with Theorem 5.6. ∎ Remark 12.3 (What this theorem does and does not say). Corollary 12.2 is immediate from the construction, and we do not present it as a deep result: a system that emits only certificate-checked facts trivially emits only certified facts. The substantive content is in the universal quantifier of Theorem 12.1. It is a statement about an entire design space Θ , not about a single fixed system: an engineer may swap encoders, retrain relation operators, redesign the sheaf, retune ω, or replace the generator, and the certified channel’s correctness guarantee requires no re-examination. That is a maintenance and auditing guarantee, and it is precisely the property that fails in architectures where a similarity threshold or an LLM judgment can promote a hypothesis into certified context. The theorem’s value is therefore as a specification that a system either satisfies or does not, and Appendix B lists the invariants that an implementation must enforce to satisfy it. 12.1 Conditional completeness Soundness bounds precision and says nothing about recall, yet recall is the entire justification for including a geometric layer. We therefore state the complementary bound, which is what makes the seed count k and hop bound h tunable against a stated criterion rather than by taste. Theorem 12.4 (Conditional completeness of certified retrieval). Fix a query q, seed count k, hop bound h, and admissible language L, and let θ∈Θθ∈ be a configuration whose certificate checker is complete for T. Write Skθ(q)S_k^θ(q) for the seed set that θ produces, which depends on θ through Φ . Let f=(x′,a,y′)∈Cl(E)f=(x ,a,y ) _T(E) be a certified fact. If there exist a seed x∈Skθ(q)x∈ S_k^θ(q) and a path p∈Lp∈ L with |p|≤h|p|≤ h whose realization from x traverses the edge f, then f∈ℛcertθ(q)f ^θ_cert(q). Consequently Cl(E)∖ℛcertθ(q)=f∈Cl(E):f lies on no L-admissible path of length≤h from Skθ(q).Cl_T(E)\ \ R^θ_cert(q)\;=\;\f _T(E):f lies on no L-admissible path of length≤ h from S_k^θ(q)\. Proof. Since x∈Sk(q)x∈ S_k(q) and p∈Lp∈ L with |p|≤h|p|≤ h, the nested enumeration of Algorithm 1 reaches the edge f while expanding p from x. A checker complete for T accepts the derivation of f∈Cl(E)f _T(E) guaranteed by Theorem 5.3, so the verification test succeeds and f is added to C. The displayed identity is the contrapositive, together with the observation that by Theorem 12.1 nothing outside Cl(E)Cl_T(E) is ever added. ∎ Corollary 12.5 (Failure modes are attributable). A certified fact absent from ℛcertθ(q)R^θ_cert(q) fails for one or more of three attributable reasons: (i) seed miss, no endpoint of a route to f lies in Skθ(q)S_k^θ(q); (i) horizon miss, every route exceeds h; (i) grammar miss, every route leaves L. Corollary 12.5 is the practical payoff. Each failure mode has a distinct remedy—improve Φ or raise k; raise h; widen L—and each is separately measurable by re-running retrieval with that single parameter relaxed. Theorem 13.3 shows that admissible-word feasibility can be decided on the bisimulation index alone, which rules out horizon and grammar explanations at the level of the path language; attributing a particular fact’s absence still requires the certified graph (Remark 13.4). Reporting the three-way decomposition of recall loss is more informative than a single Recall@k number, and we recommend it as the primary diagnostic for the semantic-recall axis of Section 21. Together, Theorems 12.1 and 12.4 express the intended division of labor precisely: the learned configuration θ controls the second containment and has no influence whatsoever on the first. 13 Minimal Structures for Certified Retrieval Two natural minimality questions arise for a PAGR system, and both bear directly on the retrieval operator rather than on the framework’s presentation. Given the certified graph, what is the smallest structure that answers the same Stage I expansions? And given the base set E, which facts are load-bearing? We answer both, and in each case the useful result is accompanied by a caveat that a naive statement would get wrong. 13.1 Bounded bisimulation as a minimal Stage-I index Let G denote the certified graph (distinct from the base-change group G_ d of Section 8.4): vertex set P, and for each a∈Q1a∈ Q_1 an edge relation ℰa=Cl(E)aE_a=Cl_T(E)_a. Write x→yx ay for (x,y)∈ℰa(x,y) _a and x→yx wy for a path spelling w∈Q1∗w∈ Q_1 . Definition 13.1 (Bounded forward bisimulation). Let x≈0yx _0y iff x and y have the same sort. Inductively, x≈m+1yx _m+1y iff x≈myx _my and for every a∈Q1a∈ Q_1, [z]≈m:x→z=[z]≈m:y→z. \[z]_ _m:x az \= \[z]_ _m:y az \. We call ≈h _h the h-bisimulation and write Gh=G/≈hG_h=G/\! _h for the quotient, in which [x]→[y][x] a[y] iff x′→y′x ay for some x′∈[x]x ∈[x], y′∈[y]y ∈[y]. This is the classical notion underlying structural indexes for graph-structured data [36], and ≈h _h is computable by partition refinement in O(h|ℰ|)O(h\,|E|), or the full bisimulation in O(|ℰ|log|P|)O(|E| |P|) [42]. Lemma 13.2 (Word preservation). If x≈hyx _hy then for every w∈Q1∗w∈ Q_1 with |w|≤h|w|≤ h, x has an outgoing w-path iff y does. Proof. Induction on |w||w|; the case |w|=0|w|=0 is immediate. Let w=aw′w=aw with |w|≤h|w|≤ h and suppose x→zx az with z having an outgoing w′w -path. Since x≈hyx _hy and h≥1h≥ 1, the class [z]≈h−1[z]_ _h-1 occurs among the a-successor classes of y, so there is z′z with y→z′y az and z′≈h−1z _h-1z. As |w′|≤h−1|w |≤ h-1, the induction hypothesis gives z′z an outgoing w′w -path. ∎ Theorem 13.3 (Exact word realizability on the index). For every x∈Px∈ P and every w with |w|≤h|w|≤ h: the class [x][x] has an outgoing w-path in GhG_h if and only if x has an outgoing w-path in G. Consequently, for any regular L and any h′≤h ≤ h, membership of a seed in the set DomL,h′=x∈P:∃p∈L,|p|≤h′,x has an outgoing p-pathDom_L,h =\x∈ P:∃\,p∈ L,\ |p|≤ h ,\ x has an outgoing p-path\ is decided exactly on GhG_h. Proof. (⇐ ) The quotient map π:G→Ghπ:G→ G_h is a graph homomorphism, so any w-path from x in G projects to a w-path from [x][x] in GhG_h. (⇒ ) Let [x]=C0→a1C1→a2⋯→anCn[x]=C_0 a_1C_1 a_2·s a_nC_n be a w-path in GhG_h with n=|w|≤hn=|w|≤ h. For each k=1,…,nk=1,…,n, the definition of quotient edges supplies y~k−1∈Ck−1 y_k-1∈ C_k-1 and yk∈Cky_k∈ C_k with y~k−1→akyk y_k-1 a_ky_k in G. Set y0=y~0∈C0y_0= y_0∈ C_0. We claim y0y_0 has an outgoing w-path in G, which we construct one step at a time. We have y0→a1y1y_0 a_1y_1. Now y1∈C1y_1∈ C_1 and y~1∈C1 y_1∈ C_1, so y1≈hy~1y_1 _h y_1. Since y~1→a2y2 y_1 a_2y_2 and |a2⋯an|=n−1≤h−1<h|a_2·s a_n|=n-1≤ h-1<h, Lemma 13.2 gives y1y_1 an outgoing (a2⋯an)(a_2·s a_n)-path in G. Concatenating with y0→a1y1y_0 a_1y_1 yields a w-path from y0y_0. Since y0∈C0=[x]≈hy_0∈ C_0=[x]_ _h we have x≈hy0x _hy_0, and |w|=n≤h|w|=n≤ h, so Lemma 13.2 transfers the w-path to x. ∎ The corresponding statement about endpoints is false, and the failure is instructive. Remark 13.4 (The index does not preserve reached endpoints). It is tempting to conclude that ReachL,h(S)Reach_L,h(S) can be computed on GhG_h and read back. It cannot. Unfolding [x]→C1→a′C2[x] aC_1 a C_2 yields a successor z of x with z≈h−1y1z _h-1y_1 for some y1∈C1y_1∈ C_1, but ≈h−1 _h-1 does not imply ≈h _h, so z need not lie in C1C_1 and the continuation need not land in C2C_2. Each unfolding step loses one level of the bisimulation, so only word realizability—which Lemma 13.2 shows is preserved—survives to depth h. What remains true is one-sided: since the quotient map is a homomorphism, ReachL,h(S)⊆π−1(ReachL,hGh(π(S))),Reach_L,h(S)\ \ π^-1\! (Reach^G_h_L,h(π(S)) ), so index expansion is a sound over-approximation. It never discards a certified fact, and a validation pass against G removes the false positives. This is the standard index-then-validate discipline [36], and it is the only correct way to use GhG_h in Stage I. Proposition 13.5 (Minimality of the index). ≈h _h is the coarsest equivalence refining the sort partition that is stable under h rounds of the refinement of Definition 13.1. Hence GhG_h has the fewest vertices among quotients through which the depth-h unfolding of G factors. Proof. Immediate from the construction: ≈h _h is obtained by h rounds of coarsest-stable partition refinement started from the sort partition, and each round produces the coarsest refinement satisfying its stability condition. ∎ We state minimality relative to bisimulation rather than to word equivalence deliberately. Trace equivalence—identifying nodes with the same realizable word sets—is strictly coarser on nondeterministic graphs, and knowledge graphs are nondeterministic in the relevant sense, since a node may have many a-successors. But deciding trace equivalence is PSPACE-complete, whereas ≈h _h is near-linear. The bisimulation quotient is the largest compression that remains cheap, which is why it is the one used in practice. The concrete payoff is narrower than it may first appear, and Remark 13.4 bounds it. Theorem 13.3 decides admissible-word feasibility exactly, so it can rule out candidate horizon and grammar explanations at the path-language level—if no admissible word of length ≤h≤ h leaves a seed, nothing is reachable from that seed and it can be discarded without expanding G. Attributing the absence of a particular certified fact f in the sense of Corollary 12.5 is a different question, since it asks whether some realization of an admissible word traverses f, and that requires validation against G: the index preserves neither reached endpoints nor individual traversed edges. 13.2 Minimal bases and the value of redundancy The second question concerns E itself. Some admitted base facts may be derivable from the others. Definition 13.6 (Redundant base fact). f∈Ef∈ E is redundant if f∈Cl(E∖f)f _T(E \f\). Proposition 13.7 (Provenance decides redundancy). Let Prov(f)∈ℕ[X]Prov(f) [X] be the provenance of f computed over E. Then f is redundant if and only if the Boolean evaluation of Prov(f)Prov(f) under xf↦0x_f 0 and xe↦1x_e 1 for all e≠fe≠ f is 11. Proof. The monomials of Prov(f)Prov(f) enumerate the admitted derivations of f, one of which is the trivial derivation contributing xfx_f. Setting xf↦0x_f 0 annihilates exactly the monomials whose derivations use f as a leaf. A surviving monomial is therefore a derivation of f from E∖fE \f\, and conversely. ∎ So the redundancy test requires no additional machinery: it is a semiring evaluation of an object the system already maintains for certification. Definition 13.8 (Base core). E′⊆E E is a base core if Cl(E′)=Cl(E)Cl_T(E )=Cl_T(E) and no proper subset of E′E has this property. Greedily testing facts by Proposition 13.7 and deleting redundant ones yields a base core. Two limits should be recorded so that this is not oversold. Proposition 13.9 (Minimum bases are intractable). Computing a base core of minimum cardinality is NP-hard. Proof. Take T to consist of the single transitivity rule R;R⊆R;R R, so that Cl(E)Cl_T(E) is the transitive closure of the digraph E. A minimum-cardinality E′⊆E E with the same transitive closure is exactly a minimum equivalent digraph of E, which is NP-hard [21]; see Aho et al. [3] for the relationship to transitive reduction. ∎ Remark 13.10 (No canonical simplest knowledge base). Base cores are not unique, and unlike the core of a relational structure under homomorphism equivalence [12] they need not be isomorphic to one another. More fundamentally, equivalence of Datalog programs is undecidable [44], so there is no general procedure for deciding whether two PAGR systems carry the same inferential content. Minimality claims in this framework are therefore always relative to a fixed rule set and a fixed query class. Most importantly, minimizing E is not epistemically free, and a system should usually decline to do it. Design Principle 13.11 (Redundancy in the base is trust redundancy). Deleting a redundant f from E changes its status from base to derived. Its certification then depends on rule soundness in addition to source correctness, lengthening its trust path, and by Section 18 it becomes vulnerable to retraction of the facts that now derive it. Base minimization is therefore an analysis and compression tool, not a maintenance policy: a fact supported both by direct evidence and by derivation is more robust than one supported by either alone. This suggests reporting, rather than eliminating, redundancy. Define the evidential multiplicity of a certified fact as the number of monomials in Prov(f)Prov(f) that survive deletion of any single base fact. Facts of multiplicity zero are single points of failure in the evidence graph; their distribution is a more informative robustness statistic than the size of E, and it is computable from provenance alone. 14 Quiver Algebra Beyond Notation It is tempting either to overuse representation theory or to dismiss it as decorative. We identify four concrete roles for quiver algebra. 14.1 Typed operator composition The first role is exact: ApA_p is defined only for type-compatible paths. Ill-typed relation composition is impossible at the algebraic level. 14.2 Constraint regularization Path identities yield testable operator constraints. For example, if a is an inverse of b in the schema, the equations ba=ei,ab=ejba=e_i, ab=e_j induce AbAa≈IVi,AaAb≈IVj.A_bA_a≈ I_V_i, A_aA_b≈ I_V_j. If c=bac=ba is a declared compositional identity, enforce Ac≈AbAaA_c≈ A_bA_a. Note that the inverse-pair equations are not admissible relations in the sense of Remark 3.3, since they equate a length-two path with a length-zero one; they are perfectly usable as operator constraints, but the representation-theoretic classification results should not be applied to the resulting quotient. 14.3 Idempotent decomposition For an QA_Q-module V, V=⨁i∈Q0eiV.V= _i∈ Q_0e_iV. This is the algebraic origin of type-specific embedding spaces. It avoids forcing heterogeneous entities into one undifferentiated vector space. 14.4 Representation type of schema quivers: a scope theorem A framework that invokes quiver representations should say precisely which classical results are available to it. For PAGR the answer is sharply negative, and stating it is useful: it rules out an entire family of approaches that a reader might otherwise expect us to pursue, and it explains why the diagnostics of Section 14.5 are restricted to invariants of a given representation. Recall the classification of representation type. Write Q¯ Q for the underlying undirected multigraph of Q, obtained by forgetting arrow orientation. Theorem 14.1 (Gabriel; Kac; Drozd). Let Q be a connected finite quiver and k algebraically closed, and let Repk(Q)Rep_k(Q) denote the category of finite-dimensional representations of Q. Say Q has finite representation type if Repk(Q)Rep_k(Q) has finitely many indecomposables up to isomorphism, and tame or wild type in the usual sense for that category. (i) [17] Q has finite representation type if and only if Q¯ Q is a simply-laced Dynkin diagram AnA_n, DnD_n, E6E_6, E7E_7, or E8E_8. In that case the indecomposables correspond bijectively to the positive roots of the associated root system. (i) [35] Q has tame type if and only if Q¯ Q is an affine (Euclidean) Dynkin diagram A~n A_n, D~n D_n, E~6 E_6, E~7 E_7, or E~8 E_8. In all types, the dimension vectors of indecomposables are exactly the positive roots of the associated Kac–Moody root system. (i) [15] Otherwise Q is wild: its representation classification problem contains that of every finite-dimensional k-algebra. Remark 14.2 (Which category the classification concerns). The algebra kQkQ is finite dimensional precisely when Q has no oriented cycles, and PAGR deliberately permits schemas that do: inverse pairs, self-relations such as :M→M refines:M→ M, and directed cycles among sorts are all natural in a knowledge schema. We therefore state Theorem 14.1 for Repk(Q)Rep_k(Q), the category of finite-dimensional representations—which is what the representation layer actually parameterizes—rather than for kQkQ as a finite-dimensional algebra. This is the setting of Kac’s theorem, which covers quivers with loops and oriented cycles, and in which the trichotomy depends only on Q¯ Q. Two consequences are worth noting. Orientation is immaterial, so it makes no difference whether a double edge arises from an inverse pair or from two relations in the same direction. And clause (i) is quoted in its standard form for finite-dimensional algebras; when Q has an oriented cycle, kQkQ is infinite dimensional and it is the classification problem for Repk(Q)Rep_k(Q), not for the algebra kQkQ in Drozd’s sense, that is wild. Statements elsewhere in this paper that genuinely require kQkQ to be finite dimensional are flagged where they occur; the hereditary property used in Section 14.5 is not among them, since path algebras satisfy gl.dimkQ≤1gl.dimkQ≤ 1 for every Q. Two features of this classification matter for schema design. First, representation type depends only on Q¯ Q, so the orientation of relations is irrelevant: declaring :A→D authored:A→ D rather than :D→A authoredBy:D→ A cannot change which regime a schema falls into. Second, every Dynkin diagram is a tree, and every affine Dynkin diagram is either a tree or a single cycle. This yields a purely arithmetic test. Corollary 14.3 (Cyclomatic criterion). Let Q be a connected schema quiver with n=|Q0|n=|Q_0| sorts and m=|Q1|m=|Q_1| primitive relation types, and let c=m−n+1c=m-n+1 be the cyclomatic number of Q¯ Q. Then: (i) finite type requires c=0c=0, i.e. m=n−1m=n-1, with Q¯ Q a Dynkin tree; (i) tame type requires c≤1c≤ 1; (i) c≥2c≥ 2—equivalently m≥n+1m≥ n+1—forces wild type. Proof. Dynkin diagrams are trees, so c=0c=0; affine Dynkin diagrams are either trees (D~ D, E~ E) or a single cycle (A~n A_n, including A~1 A_1 the double edge and A~0 A_0 the single loop), so c≤1c≤ 1. By Theorem 14.1 anything else is wild. ∎ Corollary 14.4 (Common schema features force wildness). Call a cycle feature of Q any of the following configurations in Q¯ Q: a self-relation a:i→ia:i→ i; a pair of relation types between the same two sorts, in either orientation—so in particular an inverse pair a:i→ja:i→ j, b:j→ib:j→ i; or an undirected cycle through three or more distinct sorts. Then a connected schema is of wild type as soon as it contains (i) two edge-disjoint cycle features, or (i) three or more relation types between a single pair of sorts. A single cycle feature is not enough: one self-relation alone gives A~0 A_0 and one pair of parallel relations alone gives A~1 A_1, the Kronecker quiver, both of which have c=1c=1 and are tame. Proof. Each cycle feature is a cycle of Q¯ Q in the graph-theoretic sense—a loop, a 22-cycle, or a longer cycle. Edge-disjoint cycles are linearly independent in the cycle space of Q¯ Q, whose dimension is c, so case (i) gives c≥2c≥ 2. In case (i), the two sorts and their k≥3k≥ 3 connecting edges already give c≥k−1≥2c≥ k-1≥ 2. Corollary 14.3(i) then applies. The final claim is Corollary 14.3(i)–(i): a single loop has n=m=1n=m=1 and a single parallel pair has n=m=2n=m=2, so c=1c=1 in both cases. ∎ Remark 14.5 (Why the features must be edge-disjoint). The disjointness hypothesis cannot be dropped, and dropping it is a natural mistake, because two informally stated features can name the same edges. The quiver i→ji aj, j→ij bi is at once “an inverse pair” and “two distinct relation types between the same pair of sorts,” yet these are one cycle feature and not two: representation type depends only on Q¯ Q, in which both descriptions collapse to a single double edge with c=1c=1. The quiver is A~1 A_1 and tame. The practical reading is direct. A schema with a single self-relation and nothing else—the worked example’s :M→M refines:M→ M in isolation—is tame, being A~0 A_0, whose indecomposables are Jordan blocks. A schema with one inverse pair and nothing else is A~1 A_1, the Kronecker quiver, also tame; the same holds for two distinct relation types between the same pair of sorts, since representation type depends only on Q¯ Q and both cases yield a double edge. Wildness requires c≥2c≥ 2, so by Corollary 14.4 it is combinations that force it: an inverse pair together with a self-relation on a disjoint set of arrows, three or more relation types between one pair of sorts, or any two edge-disjoint cycle features. The criterion is mild: by Corollary 14.3 a connected schema need only carry one more primitive relation type than it has entity sorts. Many schemas will satisfy it, but we deliberately make no claim about how many. Establishing such a claim would require a stated counting convention for sorts and primitive relation types, applied to a sample of published schemas, and we have not carried out that study; nor does anything in PAGR require the relation vocabulary to outgrow the sort vocabulary, since a schema may keep a small set of primitive relations and carry its semantic variation in attributes, Horn rules, or evidence metadata instead. What the scope theorem supplies is a decision procedure rather than a census: given Q, compute c and read off which classical tools are legitimately available. Remark 14.6 (This is a delimitation, not a defect). Theorem 14.1 does not weaken PAGR; it tells us which tools are unavailable and thereby which are worth building. Three consequences are worth recording. (a) In the wild regime no tractable Dynkin- or affine-style classification of the indecomposables is to be expected, so the representation layer must be learned and validated empirically rather than selected from a classification—this is the formal reason the hypotheses of Section 22 are stated as experiments. (b) Auslander–Reiten theory and quiver-Grassmannian techniques remain perfectly well defined in the wild regime; what fails is the manageable global classification of indecomposables that makes them a practical design tool, so results obtained for Dynkin or affine schemas should not be transported to ours without checking that they survive. (c) Wildness concerns the classification of all representations and says nothing about a given one. Invariants of a particular learned ρ—its endomorphism algebra, its direct-sum decomposition, its kernels and images—remain computable, which is precisely the scope of Section 14.5. Remark 14.7 (Scope of the theorem under path equations). Theorem 14.1 classifies kQkQ, i.e. the hereditary case J=0J=0. Imposing path equations can only cut down the module category, so a quotient Q=kQ/JA_Q=kQ/J may have strictly smaller representation type than kQkQ. The representation type of a bound quiver algebra is not determined by Q¯ Q alone and its classification is substantially more delicate; moreover the standard theory presumes J admissible, which Remark 3.3 shows some natural PAGR constraints violate. We therefore state the scope theorem for the unconstrained representation layer, which is the regime in which relation operators are actually trained, and make no claim about QA_Q. 14.5 Representation-theoretic diagnostics For small schemas, one may study kernels, images, invariant subspaces, or decompositions of composite maps to identify redundant relation channels or bottlenecks. By Remark 14.6(c) these remain available in wild type, since each is an invariant of a fixed ρ rather than a classification of all of them. Homological tools such as ExtExt become relevant when there is an actual module-theoretic question—for instance, Ext1(M,N)Ext^1(M,N) classifies the extensions of M by N and therefore measures the obstruction to a decomposition being a direct sum—not merely because a graph exists. The consistency dimension σρ(H) _ρ(H) of Section 10.2 provides a global diagnostic computable on the retrieved subgraph without access to the full certified closure: it reports the dimension of the space of globally consistent entity-state assignments, and σρ(H)=0 _ρ(H)=0 is a certificate that no reassignment of entity states can render the retrieved context consistent. A further homological tool operates at the level of the algebra itself. The Hochschild cohomology HH∗(AQ)H^*(A_Q) of the schema algebra AQ=kQ/JA_Q=kQ/J governs the infinitesimal deformations of its representations: HH2(AQ)H^2(A_Q) classifies first-order algebra deformations, and for a specific representation ρ the obstruction to deforming ρ as an AQA_Q-module is controlled by ExtAQ2(Mρ,Mρ)Ext^2_A_Q(M_ρ,M_ρ), where MρM_ρ is the module defined by ρ. In the hereditary case J=0J=0 the global dimension of kQkQ is 11, so ExtkQn(M,N)=0Ext^n_kQ(M,N)=0 for all n≥2n≥ 2 and all modules M,NM,N. In particular ExtkQ2(Mρ,Mρ)=0Ext^2_kQ(M_ρ,M_ρ)=0, so the deformation problem for any single representation is unobstructed: every first-order deformation extends to all orders. (Formal rigidity, the stronger condition Ext1(Mρ,Mρ)=0Ext^1(M_ρ,M_ρ)=0, does not hold in general.) The corresponding statement about the algebra is a separate one and does not follow from the global dimension, since HHn(A)=ExtAen(A,A)H^n(A)=Ext^n_A^e(A,A) is computed over the enveloping algebra Ae=A⊗kAopA^e=A _kA^op rather than over A. It nonetheless holds here: a path algebra admits a two-term projective bimodule resolution, so its Hochschild dimension is at most 11 and HHn(kQ)=0H^n(kQ)=0 for n≥2n≥ 2 [31], meaning kQkQ has no nontrivial infinitesimal algebra deformations either. This is a theorem the framework inherits for free whenever path equations are absent, and it justifies treating unconstrained relation operators as continuously trainable without algebraic obstruction. When J≠0J≠ 0 the vanishing may fail: ExtAQ2(Mρ,Mρ)Ext^2_A_Q(M_ρ,M_ρ) supplies a nonzero obstruction space, permitting obstructed parameter regimes in which relation operators may resist simultaneous consistent training; whether an obstruction is actually met depends on whether a particular obstruction class is nonzero—a structural precursor to the compositional generalization gaps of Hypothesis H1 in Section 22. 15 Learning Without Corrupting Ground Truth The architecture supports learning at several levels. 15.1 Learned entity embeddings Train or freeze ϕi _i using text, images, tabular features, or multimodal encoders. 15.2 Learned relation operators Given positive certified triples (x,a,y)(x,a,y), fit AaA_a by minimizing a loss such as ℒrel=∑(x,a,y)∈Eℓ(Aazx,zy)+ℒneg.L_rel= _(x,a,y)∈ E (A_az_x,z_y)+L_neg. Add algebraic constraints ℒalgL_alg and sheaf energy regularization. 15.3 Joint objective A general objective is ℒ=λ1ℒretr+λ2ℒrel+λ3ℒalg+λ4ℒsheaf+λ5ℒcal.L= _1L_retr+ _2L_rel+ _3L_alg+ _4L_sheaf+ _5L_cal. Here ℒcalL_cal may calibrate hypothesis scores against held-out certified edges. 15.4 Hypothesis queue High-scoring predicted edges enter a separate queue H=(x,a,y,s):s≥τ,H=\(x,a,y,s):s≥τ\, where they can be used for discovery, active learning, or evidence acquisition. They remain outside G⋆G until admitted by source evidence or a symbolic proof. This separation permits aggressive learning without contaminating certified context. 16 Ground-Truth Establishment as an Evidence Protocol A retrieval system cannot mathematically manufacture truth from text. It can, however, make the establishment of its internal ground-truth set explicit. Definition 16.1 (Evidence object). An evidence object for a base fact f is ϵf=(sourceID,locator,spanHash,extract,timestamp,validator), _f=(sourceID,locator,spanHash,extract,timestamp,validator), where the locator identifies the relevant source region and the hash binds the admitted fact to a stable source representation. Definition 16.2 (Admission predicate). Admit(f,ϵf)∈0,1Admit(f, _f)∈\0,1\ is a deterministic policy deciding whether evidence is sufficient for f to enter E. The policy may be domain-specific—peer-reviewed publication, signed database record, official API response, human curator approval, consensus threshold, or cryptographic attestation—but the mathematical framework is invariant to that choice. Design Principle 16.3 (Ground truth is protocol-relative). The certified base E is not “all truths in the world.” It is the set of assertions admitted under an explicit evidence protocol. Reproducibility requires versioning both E and the admission policy. 17 Contradiction and Paraconsistent Extensions Real knowledge bases may contain conflicting sources. Classical closure over an inconsistent theory can be problematic if arbitrary negation is allowed. The positive Horn fragment used above avoids explosion because it contains no unrestricted classical negation. For domains requiring explicit contradiction, one may maintain signed predicates R+R^+ and R−R^- or adopt a paraconsistent truth lattice. A simple four-valued status for an atom f is Belnap’s bilattice [5] ,,,,\T,F,B,N\, meaning supported true, supported false, both, or neither. Geometry may rank evidence on either side, while the generator must expose the conflict rather than collapse it to one scalar probability. This is an extension rather than a required part of the core PAGR framework. 18 Retraction and Non-Monotonic Maintenance The closure of Section 5 is monotone, so it models a knowledge base that only grows. Real corpora do not behave this way: sources are corrected, superseded, withdrawn, or found to have been misextracted, and an admitted base fact may have to be removed. Because Design Principle 6.4 forbids repairing this by re-scoring, the framework needs an explicit retraction mechanism, and provenance supplies one. Suppose e∈Ee∈ E is retracted. The facts that must be reconsidered are exactly those whose provenance polynomial mentions xex_e; a fact f survives if and only if Prov(f)Prov(f) has a monomial none of whose variables has been retracted, i.e. if Prov(f)Prov(f) evaluated with xe↦0x_e 0 and all surviving generators mapped to 11 is nonzero in the Boolean semiring. Provenance thus doubles as a truth-maintenance index: no re-derivation from scratch is needed, and the surviving derivations are exactly the certificates that remain valid. Two formal routes are available for the general case. One may move from the polynomial semiring ℕ[X]N[X] to an m-semiring equipped with a monus operator, which is what is required for a difference operation on annotated relations to be well behaved [23]; or one may keep the positive semiring and treat retraction as recomputation of the least fixed point over the reduced base, using the provenance index only to bound which facts can possibly be affected. The second is simpler and adequate whenever retractions are rare relative to queries, which is the common regime. Design Principle 18.1 (Retraction is an evidence event). Removing a fact from E is an action of the admission policy, not of the retrieval system. Its effect on Cl(E)Cl_T(E) is determined by provenance, and the recomputation preserves both Theorem 12.1 and Corollary 12.2, since both are stated relative to whatever E currently is. Versioning E and the admission policy, as Design Principle 16.3 already requires, is what makes a retraction auditable after the fact. Design Principle 13.11 is the counterpart on the other side: redundant base facts are precisely what makes a certified closure robust to retraction, which is why E should not be minimized in production. 19 Temporal and Dynamic Knowledge Let facts be indexed by validity intervals or event time. Replace EaE_a by Ea⊆Pi×Pj×.E_a P_i× P_j×T. Rules become temporal Horn rules, and provenance certificates inherit temporal constraints. A query at time t retrieves from a temporal slice or interval algebra. The same epistemic separation continues to apply: learned temporal embeddings can predict changes, but predictions remain hypotheses. 20 Complexity and Computational Boundaries 20.1 Symbolic closure For a fixed finite rule set T and finite P, naive saturation terminates but may be expensive. The relevant classical bounds are standard [1]: evaluating a fixed positive Datalog program is PTime-complete in data complexity, and for a program whose rule bodies contain at most v distinct variables the closure is computed in O(||⋅|P|v)O(|T|·|P|^v) time by naive saturation. Semi-naive evaluation avoids re-deriving old facts and reduces the constant substantially; combined complexity is ExpTime-complete, which is why the rule set should be treated as fixed and small. In practice, materialization can be partial and query-driven. 20.2 Bounded path retrieval Let A be a deterministic automaton for L. Evaluating the bounded regular-path query ReachL,hReach_L,h amounts to a breadth-first search of depth h in the product of the certified graph with A, costing O(h⋅||⋅|Cl(E)|)O(h·|A|·|Cl_T(E)|) edge traversals from a single seed and hence O(k⋅h⋅||⋅|Cl(E)|)O(k· h·|A|·|Cl_T(E)|) for k seeds. Unbounded regular-path query evaluation is NL-complete in data complexity; the hop bound h is what keeps the practical cost linear in the certified edge count and simultaneously controls semantic drift. Note the direct tension with Corollary 12.5: raising h or widening L removes horizon and grammar misses at exactly this linear cost. The bisimulation index of Section 13.1 replaces |Cl(E)||Cl_T(E)| by |Gh||G_h| in the pruning phase, at a one-off preprocessing cost of O(h|Cl(E)|)O(h\,|Cl_T(E)|) and the price of a validation pass. 20.3 Index construction and base analysis Computing ≈h _h is O(h|ℰ|)O(h\,|E|) by partition refinement, or O(|ℰ|log|P|)O(|E| |P|) for the full bisimulation [42]. Redundancy testing over the base (Proposition 13.7) is a semiring evaluation per fact, linear in the size of the stored provenance; computing a minimum base is NP-hard (Proposition 13.9), so only the greedy variant is practical. 20.4 Representation scoring A path operator ApA_p requires |p||p| matrix-vector applications. When relation operators are sparse, orthogonal, diagonal, block-structured, or low-rank, costs can be substantially reduced. 20.5 Sheaf energy On a retrieved subgraph, computing δxδ x is linear in incidences times the local restriction-map cost. Full spectral decomposition of LℱL_F is unnecessary for simple consistency scoring. 21 Evaluation Framework A PAGR system should not be evaluated by answer accuracy alone. We propose seven independent axes: six measuring properties of the retrieval system itself, and one measuring the ingestion policy on which soundness depends. Axis Question Example metric Semantic recall Did geometry find the right region? Recall@k of evidence-bearing seed neighborhoods, decomposed into seed / horizon / grammar misses per Corollary 12.5. Symbolic precision Are admitted compositions sound? Precision of derived relations under expert or held-out validation. Proof coverage How much retrieved certified context has machine-checkable witnesses? Fraction of certified outputs with valid certificates; target 11. Representation coherence Does learned geometry respect schema equations? Mean normalized path-equation residual. Local consistency Do retrieved representations glue under the sheaf? Distribution of ℰℱE_F over retrieved neighborhoods; consistency dimension σρ(H)=dimH0(H,ℱρ|H) _ρ(H)= H^0(H;F^ρ|_H) (Section 10.2) as the dimension of the space of globally consistent configurations. Generation faithfulness Does the LLM state only what the context supports? Claim-level entailment/attribution evaluation [20], separate from citation presence. Attestation fidelity Do admitted base facts actually appear in their cited spans? Attestation error rate of AdmitAdmit on a held-out audited sample (Section 6.1). The first six axes are properties of the retrieval system and can be measured without inspecting the ingestion pipeline. The seventh, attestation fidelity, is a property of the admission policy and is the empirical content of Assumption Source Correctness: reporting it is what prevents Corollary 12.2 from being read as a stronger guarantee than it actually provides. Additional ablations should remove geometry, algebraic constraints, sheaf consistency, provenance, and graph diffusion separately. The key empirical hypothesis is that the layers are complementary: geometry should improve recall, while proof-carrying symbolic constraints should protect precision. 22 Proposed Research Hypotheses The framework yields experimentally testable hypotheses. Each is stated so that a negative result is informative; H1, H2, and H5 are cheap enough to run on a standard benchmark such as FB15k-237 or WN18R without building a full retrieval stack, and we regard them as the minimum evidence the framework should be asked to produce. H1: Algebraic regularization improves compositional retrieval. Relation operators trained with path-equation constraints should generalize better to unseen multi-hop compositions than unconstrained operators. H2: Sheaf energy predicts retrieval incoherence. High ℰℱE_F neighborhoods should correlate with contradictory or semantically unstable retrieval contexts. Proposition 10.4 gives this hypothesis a mechanism to test rather than a correlation to hope for: energy should track localized path-equation violation, so the two quantities should be measured jointly and their correlation reported. H3: Epistemic separation improves factual precision at fixed recall. Allowing learned hypotheses to influence ranking but not certification should preserve discovery benefits while reducing unsupported generated claims. H4: Type-specific geometry dominates a single global metric in heterogeneous graphs. Separate spaces ℳiM_i and typed maps AaA_a should outperform a single homogeneous embedding space when relation signatures differ substantially. H5: Gauge-invariant scores improve reproducibility across equivalent parameterizations. Retrieval based on invariant residuals should be stable under isometric basis changes. Remark 8.6 sharpens this into a falsifiable pair of predictions: rankings should be exactly invariant under Iso()Iso( d) and should measurably drift under general G_ d base changes unless operators are orthogonally parameterized. Observing drift under G_ d is a confirmation, not a bug, and its magnitude quantifies how much a moduli-space account of the representation layer overstates the true invariance. 23 Worked Abstract Example Consider three entity types ,, Document, Claim, Method and primitive arrows :D→C,:C→C,:C→M,:M→M. states:D→ C, supports:C→ C, uses:C→ M, refines:M→ M. Suppose the symbolic theory contains the valid inclusion ;⊆ supports; uses uses but deliberately omits ;−1⊆, uses; refines^-1 uses, which might be unsound depending on the semantics of refinement. A query is embedded and retrieves claim c0c_0. The certified graph expands from c0c_0 through ; supports; uses to method m. The result carries a proof tree with two source-backed leaves. Meanwhile, the quiver representation predicts that another method m′m has low residual under a learned composite operator, and the sheaf layer finds that inserting m′m would lower local energy. The system may therefore rank m′m as an excellent hypothesis for further evidence search. It may not state that c0c_0 uses m′m as a certified fact until a source or symbolic derivation admits it. This example illustrates the architecture’s central asymmetry: continuous mathematics proposes; discrete proof certifies. 24 What Is New and What Is Not 24.1 Established ingredients The following are not claimed as novel: quivers and path algebras; representations of quivers; category-theoretic schemas; Horn/Datalog fixed-point semantics; semiring provenance; KGE relation operators; mixed geometry; cellular sheaves; sheaf Laplacians; graph diffusion; or proof-carrying verification patterns. All have substantial prior literatures [45, 26, 41, 22, 18, 1, 30, 34]. 24.2 What concurrent work already covers Honesty about novelty requires naming the nearest neighbors rather than only the ancestors. Three claims that a reader might expect us to make are not available. First, proof-carrying certificates attached to LLM pipeline outputs are not new; Koomullil [37] develop a kernel-checkable version. Second, attributable symbolic execution traces over retrieved evidence are not new; Gann and Gertz [19] produce them from synthesized Prolog modules and report benchmark gains. Third, using personalized PageRank over a knowledge graph for multi-hop retrieval is not new [27]. What remains, and what Section 2.6 argues is the actual gap, is that none of these separates the grammar of admissible composition from the geometry of proposal, and none states an invariance property over a design space of learned components. 24.3 Proposed synthesis The research contribution is the combined architecture and the sharp division of epistemic responsibilities: 1. a symbolic knowledge layer generated by source-attested facts and sound closure; 2. a quiver-algebraic representation layer in which relation types act as typed operators and path identities become structural constraints; 3. a metric/mixed-geometry layer used for semantic discovery; 4. a sheaf layer used for local-to-global consistency; 5. provenance and proof objects used as an admissibility condition for certified retrieval, and as the index for retraction; 6. an explicit non-interference theorem (Theorem 12.1) guaranteeing that arbitrary replacement of learned retrieval components cannot introduce an uncertified fact into the certified channel, together with a matching completeness bound (Theorem 12.4) that attributes every recall failure to one of three named causes; 7. a coupling result (Proposition 10.4) showing that the sheaf layer’s consistency energy is a localized measurement of the representation layer’s compositional constraints, so the two layers are not parallel decorations; 8. a scope theorem (Section 14.4) delimiting which representation-theoretic tools are available—essentially every practical schema is of wild type—and minimality results for the retrieval operator itself: a bounded-bisimulation index that exactly decides admissible-word realizability, and a provenance-based characterization of redundant base facts. We call this design proof-carrying geometric retrieval. Its novelty, if validated empirically, is architectural rather than foundational: modern algebraic and geometric machinery is arranged so that statistical power and epistemic authority are intentionally non-coincident. 25 Limitations First, symbolic soundness is only relative to source correctness and rule validity. The framework cannot prove that a corrupted source or mistaken curator is correct, and Section 6.1 makes clear that in an LLM-ingested corpus this assumption is doing a great deal of work; the attestation error rate is the honest measure of how much. Second, constructing a high-quality typed schema and rule set is costly, and this cost is the framework’s main barrier to adoption relative to schema-free GraphRAG pipelines [16, 27]. Third, learned representations may add limited value when the graph is tiny or relations are already exhaustive. Fourth, sheaf construction may require learned or curated restriction maps; Definition 10.3 removes this freedom by tying restrictions to ρ, but a system that instead learns them freely reacquires the problem that poor restrictions yield misleading consistency signals. Fifth, recursive provenance can become large and requires compact DAGs, absorptive semantics, or bounded proof policies. Sixth, exact path-algebra constraints may be inappropriate where relations are intrinsically noisy; regularization rather than equality is then preferable. Seventh, and most importantly for a reader deciding whether to build on this: the paper is entirely theoretical. Every claim about the benefit of the architecture—that geometry improves recall, that algebraic regularization helps compositional generalization, that sheaf energy flags incoherence—is a conjecture stated in Section 22, not a result. Only the structural claims (Theorems 12.1, 12.4, 8.4, Proposition 10.4) are established, and those are established by construction rather than by evidence about the world. The framework should be read as a specification and a set of testable predictions, and it should not be cited as showing that proof-carrying geometric retrieval outperforms anything. Finally, the framework does not imply that every useful knowledge graph should be represented by a finite-dimensional linear quiver representation. Nonlinear maps, probabilistic kernels, enriched categories, operator algebras, or higher-order relational structures may be better in particular domains. The quiver representation is a disciplined baseline, not a universal theorem about cognition. 26 Future Directions Several mathematical extensions are natural. Enriched and quantaloid semantics. Because Rel is locally ordered, one can formulate the schema in an order-enriched categorical setting where inclusions are native 22-cells. Weighted relations suggest enrichment over quantales, potentially unifying symbolic reachability and graded costs. Nonlinear quiver representations. Replace Vect by smooth manifolds and relation arrows by differentiable maps, or by Markov kernels for probabilistic semantics. Composition remains functorial while permitting nonlinear geometry. Derived and homological diagnostics. The consistency dimension σρ(H) _ρ(H) (Section 10.2) and the Hochschild cohomology sketch of Section 14.5 open a systematic homological program. Computing HH∗(AQ)H^*(A_Q) for concrete schemas via the bar resolution yields explicit generators that bound the deformation space of any trained representation and predict which regions of parameter space are compatible with the declared path equations. Derived categories Db(mod-AQ)D^b(mod-A_Q) provide the natural ambient category: ExtAQn(M,N)≅HomDb(M,N[n])Ext^n_A_Q(M,N) _D^b(M,N[n]), and ExtAQ1(Mρ,Mρ)Ext^1_A_Q(M_ρ,M_ρ) parameterizes the first-order deformation directions of MρM_ρ, with obstructions to integrating them controlled by ExtAQ2(Mρ,Mρ)Ext^2_A_Q(M_ρ,M_ρ); a nonzero first-order class supplies a concrete direction in operator space that could guide regularization or generate adversarial test cases for compositional generalization. Higher persistent sheaf cohomology, indexing σρ(H) _ρ(H) across filtrations of the retrieved subgraph by evidence score or hop depth, could track how the space of consistent configurations collapses as context is expanded—a topological analogue of precision-recall curves with a certificate rather than a threshold. Persistent and topological retrieval. Filtrations by score, hop count, or evidence threshold induce filtered complexes. Persistent homology could identify retrieval structures stable across thresholds, complementing the simple top-k margin theorem. Certified neural-symbolic training. One may train relation operators and sheaf restrictions against certified derivations while reserving symbolic proof checking as an independent verifier, analogous to a prover–checker split. Evidence acquisition agents. Hypothesis edges with high geometric score but no proof can trigger tools that search external sources. The resulting evidence passes through the same admission predicate before promotion. This provides a principled route from statistical discovery to certified knowledge growth. 27 Conclusion A grounded retrieval system should be more than a graph whose nodes happen to have embeddings. Geometry, algebra, logic, and provenance answer different questions. When these questions are made explicit, a coherent architecture emerges. The symbolic layer defines which facts are certified and which compositions are sound. The quiver and path algebra define typed compositional structure. Quiver representations turn that structure into learnable operators while preserving type and composition information. Metric and mixed-geometry spaces support semantic discovery. Cellular sheaves quantify whether local representations are mutually compatible. Semiring provenance and proof objects explain derivations. An LLM sits downstream of these structures and synthesizes their output rather than silently redefining them. The resulting principle is simple: geometry proposes⟶algebra structures⟶proof certifies⟶generation communicates geometry proposes\; \;algebra structures\; \;proof certifies\; \;generation communicates This separation does not reduce the role of learning. It makes learning safer to use aggressively: retrieval and hypothesis generation may exploit sophisticated geometric models precisely because the architecture prevents latent similarity from being mistaken for ground truth. We suggest that this is a productive mathematical foundation for the next generation of graph-based retrieval systems. References [1] Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison-Wesley, 1995. [2] Mahmoud Abo Khamis, Hung Q. Ngo, Reinhard Pichler, Dan Suciu, and Yisu Remy Wang. Convergence of datalog over (pre-)semirings. arXiv preprint arXiv:2105.14435, 2021. Also in Proceedings of PODS 2022. [3] Alfred V. Aho, Michael R. Garey, and Jeffrey D. Ullman. The transitive reduction of a directed graph. SIAM Journal on Computing, 1(2):131–137, 1972. doi: 10.1137/0201008. [4] Marco Antonio Armenta and Pierre-Marc Jodoin. The representation theory of neural networks. arXiv preprint arXiv:2007.12213, 2020. Published in Mathematics 9(24):3216, 2021. [5] Nuel D. Belnap. A useful four-valued logic. In J. Michael Dunn and George Epstein, editors, Modern Uses of Multiple-Valued Logic, pages 5–37. Reidel, Dordrecht, 1977. [6] Robi Bhattacharjee and Sanjoy Dasgupta. What relations are reliably embeddable in euclidean space? In Proceedings of the 31st International Conference on Algorithmic Learning Theory (ALT), volume 117 of PMLR, pages 174–195, 2020. [7] Cristian Bodnar, Francesco Di Giovanni, Benjamin Paul Chamberlain, Pietro Liò, and Michael M. Bronstein. Neural sheaf diffusion: A topological perspective on heterophily and oversmoothing in GNNs. In Advances in Neural Information Processing Systems (NeurIPS), volume 35, 2022. [8] Antoine Bordes, Nicolas Usunier, Alberto Garcia-Duran, Jason Weston, and Oksana Yakhnenko. Translating embeddings for modeling multi-relational data. In Advances in Neural Information Processing Systems (NIPS), volume 26, pages 2787–2795, 2013. [9] Camille Bourgaux, Pierre Bourhis, Liat Peterfreund, and Michael Thomazo. Revisiting semiring provenance for datalog. arXiv preprint arXiv:2202.10766, 2022. Also in Proceedings of KR 2022. [10] Luke Braithwaite, Iulia Duta, and Pietro Liò. Heterogeneous sheaf neural networks. arXiv preprint arXiv:2409.08036, 2024. [11] Ines Chami, Adva Wolf, Da-Cheng Juan, Frederic Sala, Sujith Ravi, and Christopher Ré. Low-dimensional hyperbolic knowledge graph embeddings. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL), pages 6901–6914, 2020. [12] Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. In Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC), pages 77–90, 1977. doi: 10.1145/800105.803397. [13] Justin M. Curry. Sheaves, Cosheaves and Applications. PhD thesis, University of Pennsylvania, 2014. arXiv:1303.3255. [14] Harm Derksen and Jerzy Weyman. An Introduction to Quiver Representations, volume 184 of Graduate Studies in Mathematics. American Mathematical Society, 2017. [15] Yuriy A. Drozd. Tame and wild matrix problems. In Representation Theory I, volume 832 of Lecture Notes in Mathematics, pages 242–258. Springer, 1980. [16] Darren Edge, Ha Trinh, Newman Cheng, Joshua Bradley, Alex Chao, Apurva Mody, Steven Truitt, Dasha Metropolitansky, Robert Osazuwa Ness, and Jonathan Larson. From local to global: A graph RAG approach to query-focused summarization. arXiv preprint arXiv:2404.16130, 2024. [17] Peter Gabriel. Unzerlegbare darstellungen I. Manuscripta Mathematica, 6:71–103, 1972. doi: 10.1007/BF01298413. [18] Iordan Ganev and Robin Walters. Quiver neural networks. arXiv preprint arXiv:2207.12773, 2022. [19] Jonas Gann and Michael Gertz. NeSy-RAG: Neuro-symbolic RAG for explainable question answering. arXiv preprint arXiv:2608.06292, 2026. [20] Tianyu Gao, Howard Yen, Jiatong Yu, and Danqi Chen. Enabling large language models to generate text with citations. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 6465–6488, 2023. [21] Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. [22] Thomas Gebhart, Jakob Hansen, and Paul Schrater. Knowledge sheaves: A sheaf-theoretic framework for knowledge graph embedding. In Proceedings of the 26th International Conference on Artificial Intelligence and Statistics (AISTATS), volume 206 of PMLR, pages 9094–9116, 2023. [23] Floris Geerts and Antonella Poggi. On database query languages for k-relations. Journal of Applied Logic, 8(2):173–185, 2010. doi: 10.1016/j.jal.2009.09.001. [24] Joseph A. Goguen and José Meseguer. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy, pages 11–20, 1982. [25] Gösta Grahne and Alex Thomo. Provenance for regular path queries. arXiv preprint arXiv:2001.09864, 2020. [26] Todd J. Green, Grigoris Karvounarakis, and Val Tannen. Provenance semirings. In Proceedings of the 26th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS), pages 31–40, 2007. doi: 10.1145/1265530.1265535. [27] Bernal Jiménez Gutiérrez, Yiheng Shu, Yu Gu, Michihiro Yasunaga, and Yu Su. HippoRAG: Neurobiologically inspired long-term memory for large language models. In Advances in Neural Information Processing Systems (NeurIPS), volume 37, 2024. arXiv:2405.14831. [28] Haoyu Han, Yu Wang, Harry Shomer, Kai Guo, Jiayuan Ding, Yongjia Lei, Mahantesh Halappanavar, Ryan A. Rossi, Subhabrata Mukherjee, Xianfeng Tang, Qi He, Zhigang Hua, Bo Long, Tong Zhao, Neil Shah, Amin Javari, Yinglong Xia, and Jiliang Tang. Retrieval-augmented generation with graphs (GraphRAG). arXiv preprint arXiv:2501.00309, 2025. [29] Jakob Hansen and Thomas Gebhart. Sheaf neural networks. arXiv preprint arXiv:2012.06333, 2020. NeurIPS 2020 Workshop on Topological Data Analysis and Beyond. [30] Jakob Hansen and Robert Ghrist. Toward a spectral theory of cellular sheaves. Journal of Applied and Computational Topology, 3(4):315–358, 2019. doi: 10.1007/s41468-019-00038-7. [31] Dieter Happel. Hochschild cohomology of finite-dimensional algebras. In Séminaire d’Algèbre Paul Dubreil et Marie-Paul Malliavin, volume 1404 of Lecture Notes in Mathematics, pages 108–126. Springer, Berlin, 1989. doi: 10.1007/BFb0084073. [32] Yuntong Hu, Zhihan Lei, Zheng Zhang, Bo Pan, Chen Ling, and Liang Zhao. GRAG: Graph retrieval-augmented generation. arXiv preprint arXiv:2405.16506, 2024. [33] George Jeffreys and Siu-Cheong Lau. Kähler geometry of quiver varieties and machine learning. arXiv preprint arXiv:2101.11487, 2021. [34] Glen Jeh and Jennifer Widom. Scaling personalized web search. In Proceedings of the 12th International Conference on World Wide Web (W), pages 271–279, 2003. doi: 10.1145/775152.775191. [35] Victor G. Kac. Infinite root systems, representations of graphs and invariant theory. Inventiones Mathematicae, 56:57–92, 1980. doi: 10.1007/BF01403155. [36] Raghav Kaushik, Pradeep Shenoy, Philip Bohannon, and Ehud Gudes. Exploiting local similarity for indexing paths in graph-structured data. In Proceedings of the 18th International Conference on Data Engineering (ICDE), pages 129–140, 2002. [37] George Koomullil. Proof-carrying certificates for LLM pipelines: A trust-boundary architecture. arXiv preprint arXiv:2605.16407, 2026. [38] Jaejun Lee, Chanyoung Chung, and Joyce Jiyoung Whang. Ingram: Inductive knowledge graph embedding via relation graphs. In Proceedings of the 40th International Conference on Machine Learning (ICML), volume 202 of PMLR, pages 18796–18809, 2023. [39] Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. Retrieval-augmented generation for knowledge-intensive NLP tasks. In Advances in Neural Information Processing Systems (NeurIPS), volume 33, pages 9459–9474, 2020. [40] Rui Li, Chaozhuo Li, Yanming Shen, Zeyu Zhang, and Xu Chen. Generalizing knowledge graph embedding with universal orthogonal parameterization. In Proceedings of the 41st International Conference on Machine Learning (ICML), 2024. arXiv:2405.08540. [41] George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 106–119, 1997. doi: 10.1145/263699.263712. [42] Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987. doi: 10.1137/0216062. [43] Ralf Schiffler. Quiver Representations. CMS Books in Mathematics. Springer, 2014. [44] Oded Shmueli. Equivalence of Datalog queries is undecidable. The Journal of Logic Programming, 15(3):231–241, 1993. doi: 10.1016/0743-1066(93)90040-N. [45] David I. Spivak. Functorial data migration. Information and Computation, 217:31–51, 2012. doi: 10.1016/j.ic.2012.05.001. [46] Zhiqing Sun, Zhi-Hong Deng, Jian-Yun Nie, and Jian Tang. Rotate: Knowledge graph embedding by relational rotation in complex space. In International Conference on Learning Representations (ICLR), 2019. arXiv:1902.10197. [47] Komal Teru, Etienne Denis, and William Hamilton. Inductive relation prediction by subgraph reasoning. In Proceedings of the 37th International Conference on Machine Learning (ICML), volume 119 of PMLR, pages 9448–9457, 2020. [48] Théo Trouillon, Johannes Welbl, Sebastian Riedel, Eric Gaussier, and Guillaume Bouchard. Complex embeddings for simple link prediction. In Proceedings of the 33rd International Conference on Machine Learning (ICML), volume 48 of PMLR, pages 2071–2080, 2016. [49] Viacheslav Yusupov, Maxim Rakhuba, and Evgeny Frolov. Knowledge graph completion with mixed geometry tensor factorization. In Proceedings of the 28th International Conference on Artificial Intelligence and Statistics (AISTATS), volume 258 of PMLR, pages 4924–4932, 2025. [50] Xiangrong Zhu, Yuexiang Xie, Yi Liu, Yaliang Li, and Wei Hu. Knowledge graph-guided retrieval augmented generation. In Proceedings of the 2025 Conference of the North American Chapter of the Association for Computational Linguistics (NAACL), 2025. arXiv:2502.06864. Appendix A Notation Summary Symbol Meaning Q finite schema quiver Q0,Q1Q_0,Q_1 entity sorts and primitive relation types kQkQ path algebra of Q over field k J ideal generated by path equations Q=kQ/JA_Q=kQ/J quotient path algebra (see Remark 3.3) ℰJE_J declared path-equation pairs generating J P=⨆iPiP= _iP_i typed entity universe; PiP_i are entities of sort i E source-attested extensional relation base T positive Horn relational rule set Cl(E)Cl_T(E) least certified closure At()At( M) atoms satisfied by the intended model M ℳiM_i type-specific metric/geometric space ϕi,ψi _i, _i entity and query encoders into ℳiM_i ViV_i vector space assigned to sort i in quiver representation AaA_a linear operator assigned to relation arrow a G,Iso()G_ d,Iso( d) base-change group and its isometry subgroup ℱ,ℱρF,F^ρ cellular sheaf; the sheaf induced by ρ C0(G,ℱ),C1(G,ℱ)C^0(G;F),C^1(G;F) vertex-stalk and edge-stalk cochain groups LℱL_F sheaf Laplacian H0(G,ℱ)H^0(G;F) zeroth sheaf cohomology (global sections, =kerδ= δ) H1(G,ℱ)H^1(G;F) first sheaf cohomology (=C1/im(δ)=C^1/im(δ); a topological residual, not a consistency diagnostic—see Remark 10.10) σρ(H) _ρ(H) consistency dimension dimH0(H,ℱρ|H) H^0(H;F^ρ|_H) of retrieved subgraph H HHn(AQ)H^n(A_Q) n-th Hochschild cohomology of the schema algebra AQA_Q Prov(f)Prov(f) provenance object for fact f φ scalarization of a provenance object for ranking G⋆G certified internal knowledge set θ,Θθ, learned configuration and its design space W column-stochastic diffusion matrix (Stage V) h,kh,k hop bound and seed count Appendix B Minimal Machine-Checkable Invariants A practical implementation should enforce at least the following invariants. Invariants 1–5 are together sufficient for Theorem 12.1; the remainder are hygiene conditions that make the paper’s diagnostics meaningful. 1. Every base fact is well typed under Q and resolves to an evidence object admitted by a policy independent of the extractor that proposed it (Design Principle 6.5). 2. Every derived certified fact has a valid derivation DAG whose internal nodes instantiate rules in T. 3. Path-equation constraints in J are distinguished from Horn inclusions in T. 4. Learned edges are stored in a hypothesis relation namespace separate from certified relations. 5. Retrieval output preserves epistemic status through ranking and serialization. 6. Any relation-representation score used for ranking is invariant to the declared gauge group, and the declared group is recorded; per Remark 8.6 it is Iso()Iso( d) and not G_ d unless operators are orthogonally parameterized. 7. Cross-type seed scores are calibrated to a common scale before top-k selection (Definition 9.2). 8. The query seed margin is logged when robustness claims depend on top-k stability. 9. Recall failures are attributed to seed, horizon, or grammar misses (Corollary 12.5). 10. Sheaf energy is reported as a consistency statistic, never as factual confidence. 11. Retraction of a base fact triggers provenance-indexed invalidation of every certificate depending on it (Section 18), and evidential multiplicity is reported rather than minimized away (Design Principle 13.11). 12. Any bisimulation index used to accelerate Stage I is treated as a sound over-approximation and its results validated against the certified graph (Remark 13.4). 13. Generator citations are checked for containment in the supplied context, while claim-level source faithfulness is evaluated separately. Appendix C Alternative Categorical Formulation One can package parts of the framework categorically. Path equations generate a category =Path(Q)/∼JC=Path(Q)/ _J. A strict linear representation is a functor ρ:→k.ρ:C _k. A relational interpretation is a functor into Rel only for equational constraints. Horn inclusions require the local order on Rel to be used explicitly: a rule p⊆qp q is interpreted as a 22-cell I(p)⇒I(q)I(p) I(q) in the order-enriched sense. Thus the most faithful categorical home for the combined schema is not an ordinary 11-category alone but an order-enriched or locally posetal setting. This explains why a plain “finitely presented category” captures path identities but not all one-way inference rules. Appendix D Relationship Between Quiver Representations and Sheaves Both constructions attach vector spaces and maps to combinatorial data, but they serve different roles here. A quiver representation attaches spaces to schema vertices and maps to relation types; many concrete entity edges share the same typed operator. A cellular sheaf attaches spaces and restrictions to individual graph cells or incidences; different entity edges may impose different compatibility maps. The former is therefore a global typed parameterization, while the latter is a local compatibility system. Definition 10.3 exhibits one canonical coupling: the sheaf ℱρF^ρ in which every edge inherits its restriction from the relation operator of its label. Under that tying the two structures carry the same information, and Proposition 10.4 shows the consequence—sections of ℱρF^ρ satisfy the declared path equations on their support. The general case is strictly larger. A free cellular sheaf can assign different restrictions to two edges bearing the same relation label, which lets it model edge-specific context that no representation of Q can express, at the cost of losing the guarantee that consistency implies compositional coherence. The design choice is therefore a real one: tying restrictions buys Proposition 10.4, freeing them buys expressiveness. A hybrid in which ℱu⊴e=Aλ(e)+ΔeF_u e=A_λ(e)+ _e with ‖Δe‖\| _e\| penalized interpolates between the two, and the penalty weight is the knob controlling how much the guarantee degrades. We flag this as the most concrete open modeling question raised by the framework.