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 Rcoreᵛ4) 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.
Abdiel Mars (Tue,) studied this question.