An Axiomatic Foundation for Agent Memory: Three Primitive Roles, Boundaries, and Conditional Results

Long-form technical report (~36,000 words) developing the axiomatic foundation of agent memory in partial Horn logic. Formalises three primitive roles — Genesis (origin and chosen operation histories), Stratification (coherent movement across layers), and Relation Reification (turning relations and operations into first-class objects) — over a finite many-sorted partial Horn signature with eight sorts, forty function symbols, and one non-logical predicate Atomic. Main results: first-order soundness (Theorem 5.1) and completeness via PV translation chain (Theorem 5.2, with Lemma 11.1 conservative translation proof-theoretically established in both directions in §A.12.5); conditional decidability for a computational rewrite core (Proposition 6.4); modular independence of the three axiom groups under standard-ℕ restriction (Theorem 7.1, H4); two Diagnostic Schemas DS1, DS2 plus one Proposition (8.3, DP3) for explicit architecture classes. Assumption T (termination of R_core^v4) discharged via direct 55-rule AProVE YES in 2.35 seconds. Methodology: L3 boundary discipline explicitly separating first-order Horn theory, fortified theory with five meta-conditions, and the intended agent-memory schema class. Eleven hidden assumptions catalogued (H1–H11) plus one definitional convention (DC1). Standards Correspondence (§3.7) against PROV-O, RDF 1.2, Cypher, GQL. Section 13 records zero open mathematical obligations within this paper itself: prior obligations on (i) Lemma 11.1 backward direction (Purity Lemma + structural induction in §A.12.5), (ii) Horn-sequent forms for seven axioms (§A.3.G/Σ/R), and (iii) modular termination (replaced by direct full-system AProVE run) are all discharged. Lean/Isabelle mechanisation of §A.12.5 remains future work (§11 Item 4). Status: Long-form technical report, formal companion to Mars 2026 (Categorical Primitives for Agent Memory: A Foundational Proposal, doi:10.5281/zenodo.20032332). Not a peer-reviewed venue submission. Companion shorter papers under preparation: Paper 2A (formal, targeted at LICS/LMCS) and Paper 2B (systems, targeted at NeurIPS/AAAI Agents) plus a separate L3 boundary methodology paper. Reproducibility: All AProVE termination and Z3/CVC5 axiom-consistency artifacts included with SHA-256 hashes recorded in §9.2 Evidence Inventory.