Coalgebraic Memory

1 Introduction

An agent that forgets everything between sessions is a function; an agent that remembers is a state-based system, and state-based systems are the subject matter of coalgebra (15, 5). Banu takes this as the first row of a correspondence between the four externalization pillars of Zhou et al. and the ArchAgents Architecture triple (1, 20, 14). Memory there is a coalgebra $(S, \varphi)$ for a polynomial functor, and the correspondence is validated against one reference implementation. It is stated at the level of the pair $(S, \varphi)$. It does not fix the functor, the laws, or the means of checking either against a system that was not built to fit the account.

This paper fixes all three for one system. ContextFS is a memory layer for coding agents. It stores typed records and exposes them over a command line, a Python facade and a Model Context Protocol server. It also maintains a graph of relation-labelled edges recording how records were derived from one another. Its lineage module offers four derivation operations, evolve, merge, split and supersede, each of which creates new records and leaves the originals in place. The coalgebraic account presupposes a persistent carrier, non-destructive derivation and an explicit edge vocabulary. A system with all three is the informative case to examine: where the account fails here, it fails for reasons other than the absence of the structure it needs.

The test isolates a stable derivation fragment rather than a property of the whole system. Derivations add fresh records and ancestry edges, which preserves the ancestry of existing records and confines effects when every named record belongs to one namespace. Deletion and replacement fall outside that fragment: deletion removes incident edges, while a save under an existing identifier replaces a record. Proposition 5.9 proves that the restricted fragment is closed and reachable. The failed clauses identify conditions that the informal state-and-transitions description leaves unstated.

1.1 Scope

Every result below is proved from the definitions in Section 3 or established by the inspection procedure of Section 1.3. Companion work on the other three pillars is cited where a reader may want the adjacent layer.

The claim being tested is narrow. It is not claimed that the four externalization pillars and the Architecture triple $(G, \mathrm{Know}, \Phi)$ are the same object. Three things are claimed, under stated assumptions. There is a structure-preserving interpretation of the pillars in the triple. A production system realises that interpretation on an identifiable fragment. The places where the interpretation fails are exhibited rather than passed over.

For memory, the identifiable fragment is the lineage fragment: the record store, the edge graph, and the four derivation operations, together with saves that allocate fresh identifiers. Deletion and saves under an existing identifier are outside it. Every positive result below carries that exclusion in its hypotheses (Proposition 5.2, Proposition 5.9). The fragment not covered is retrieval: similarity search over an external vector index is not an observation of the state space in the sense of Definition 3.14, for the reasons given in Section 7.4. The most-quoted feature of the correspondence is that agent memory is bitemporal in the sense of Jensen and Snodgrass (6). Its absence here is not merely conceded: valid time is proved to be unrecoverable from the recorded state (Theorem 5.27).

1.2 Contributions

1. A model of a memory store as a pair $(m, E)$ of a finite partial map on identifiers and a finite relation-labelled edge set, with a partial commutative monoid structure given by domain-disjoint union (Definition 3.4, Proposition 3.6).

2. Two coalgebras over that data and an account of what each is for. The store coalgebra $(S, \alpha \colon S \to F S)$ for $F X = (\mathrm{Out}\times X)^{A^{+}}$ models the API dynamics (Definition 3.14). The lineage coalgebra $(\mathrm{Id}, \beta_{s})$ for $H X = \mathrm{Rec}_{\bot} \times \mathcal{P}_{\mathrm{fin}}(\mathcal{R}\times X)$ models what can be observed about one memory’s derivation (Definition 3.18). The alphabet of the first is the memory API extended by an allocation oracle, without which the structure map is not a function (Remark 3.9).

3. Seven laws that a lineage realisation should satisfy (Definition 3.21), chosen so that each is decidable by inspection of a candidate implementation rather than by testing.

4. A proof that the ancestry fragment is homomorphism-stable (Theorem 5.7) and that the full lineage fragment is not (Proposition 5.13). This is the positive result of the paper.

5. A separation of the two halves of namespace locality: operations that name only records of one namespace have effects confined to it (Proposition 5.17), while merge nevertheless carries payload across the boundary by construction (Proposition 5.18).

6. Three further negative results with code-level witnesses. The merged record’s type is decided by an enumeration order the interface does not declare (Proposition 5.20). Ancestry is recorded in two representations that need not agree (Proposition 5.14). The recorded state is single-axis (Theorem 5.27).

7. An algebraic account of merge at the level a coalgebra calls for: it is idempotent up to allocation-blind bisimilarity (Proposition 5.24) and not commutative even up to that equivalence (Proposition 5.25).

8. A frame property for operations that name their identifiers (Proposition 6.2) and two independent failures of it, one for recall by identifier prefix (Proposition 6.3) and one for the lineage observation on stores with dangling edges (Proposition 6.4). Together these are the obstruction to composing memory stores by disjoint union in a multi-tenant setting.

9. An appendix mapping every code-backed claim in the paper to a repository, path, identifier, line and commit.

1.3 Evidence and proof method

The results below are of two kinds and it matters that they are not confused, so we separate them by construction rather than by convention.

Results of the first kind are theorems about the model of Section 3. Their hypotheses are properties of a lineage realisation stated in the model’s own vocabulary, chiefly the derivation schema of Definition 3.23, which says which records and edges each operation adds. They are proved from those hypotheses and from the definitions, with no appeal to any repository. Theorem 5.7, Corollary 5.12, Proposition 5.17, Proposition 5.24, Proposition 7.1 and Proposition 6.2 are of this kind, as are all results in Section 3. They stand or fall on the mathematics.

Results of the second kind are instantiation claims: statements that the source of one repository at one commit exhibits a construct the model names. Their evidence is a path, an identifier and a line range, and their epistemic status is that of a careful reading, not that of a proof. We do not give an operational semantics for Python and SQLite, and we do not claim to have verified anything mechanically. Where such a claim appears in a numbered environment it is because it plays a role in an argument and needs a label. The environment is not a claim of formal derivation. Every instantiation claim in the paper appears as a row of Appendix A with its file, identifier and lines, so a reader can check each one directly against the repository.

Companion work on the other three pillars is cited in a third way again, and never as a premise. Such a citation reports a fact about a different repository that a reader may want for context, for instance whether one system declares a dependency on another. No definition, hypothesis or proof step below rests on a companion, and every object used here is defined in Section 2 or Section 3.

The two kinds meet in exactly one place. Lemma 5.6 is an instantiation claim: it asserts that ContextFS at a93035d instantiates the derivation schema. Every positive result about the system in Section 5 is then a theorem of the first kind applied to that lemma. A reader who disputes the reading of the source can reject Lemma 5.6 without any of the mathematics changing, and a reader who accepts it gets the theorems. Negative results are simpler: each exhibits a concrete counterexample whose only code-dependent ingredient is a single named expression.

1.4 Series context

This paper is the first of four on the externalization pillars, and the papers share notation. The results below do not depend on formal claims from the companion papers.

Nothing formal is imported. The proofs need $\mathbf{Set}$, the definition of a coalgebra and its homomorphisms, and the bitemporal vocabulary of the temporal database literature, all recalled in Section 2.

The companion treatment of skills as operations of a coloured operad (10) uses the memory carrier as one colour. The type $\mathsf{Mem}$ of a handle on the carrier is therefore defined here (Definition 3.15), as a single colour rather than a family indexed by record schemas. Port types themselves are defined in the companion treatment of protocols (11), together with the alphabet $\mathsf{T}$. The notion is used here in that sense, and the symbol $\mathsf{T}$ is not reused for anything else.

The companion treatment of the harness (12) develops the Architecture triple $(G, \mathrm{Know}, \Phi)$ in full, together with the categories $\mathbf{Arch}$ and $\mathbf{Sys}$ and the reading of an agent as a lax monoidal functor $A \colon \mathbf{Arch}\to \mathbf{Sys}$. None of that is needed here and none of it is used. One boundary is needed, and we fix it ourselves so that nothing below depends on a companion. A certificate $\mathrm{cert}$ in the sense of Banu’s Definition 1 is a checkable statement about an architecture, consisting of a claim, an assignment of its parameters, and evidence that can be replayed (1). The $\mathrm{Know}$ component of an architecture is a collection of such statements. The state space $S$ of this paper is a different thing: it is what is remembered, not what is checked. In ContextFS, the schema registry and the structured-data validation are $\mathrm{Know}$-level and lie outside $S$. The record store and the edge set are $S$.

Theorem 5.27 is proved here rather than assumed anywhere, and is what companion work cites when it describes the memory component of a harness as a single-axis store.

What this layer offers a composite is the carrier together with one stability guarantee. A skill that reads the ancestry of a record at one point in a composite and again later is entitled, by Theorem 5.7, to assume the ancestry has not changed. It is not entitled to assume the same of descendants, and Proposition 6.3 records what identifier discipline is needed for even the first assumption to be meaningful when several tenants share a store.

Throughout, statements about code are claims about the source at the pinned commit. We write “the implementation at a93035d does $X$” and mean that a reader of the named file and line will find $X$ written there. We do not report runtime observations, and we do not describe any property as established by anything stronger than a reading of the source.

2 Background

2.1 The memory pillar

Zhou et al. survey the externalization of agent capability into four components that sit around a language model rather than inside it: memory, skills, protocols, and the harness that composes them (20). Memory in that taxonomy is whatever survives the boundary of a single model call. It is not the context window, which is an input. It is the store the agent consults to build the input and updates after acting.

Two things follow from that definition. Memory is stateful in a strong sense: the same query at two times may legitimately return different answers, and the difference is information rather than error. Memory is also observed rather than inspected. An agent does not read the store. It calls an operation and receives an answer. Both properties are the defining properties of the systems coalgebra was designed for (15, 5), which is why the identification of memory with coalgebraic state is natural rather than decorative.

Banu takes the identification as the first row of a four-row correspondence between Zhou’s pillars and the ArchAgents Architecture triple $(G, \mathrm{Know}, \Phi)$ of de los Riscos, Corbacho and Arbib (1, 14). In that correspondence memory is modelled as a coalgebra for a polynomial functor, a pair $(S, \varphi)$ with $\varphi \colon S \to \mathcal{P}(S)$. The reference implementation is said to carry bitemporal records, so that the question “what did the agent believe at time $t$” has an answer. The correspondence is stated at that level of detail and validated against a single reference implementation, which the author identifies as a limitation of the work (1, Section 7.2). The identifiers named there, including BiTemporalMemory and RunContext, belong to that reference implementation. They do not occur in ContextFS at a93035d, and this paper does not use them (Remark 7.3).

Cao argues the wider motivation for externalizing memory on complexity grounds (2). The argument contrasts systems whose decision logic is fixed in source with systems that generate it at run time, and treats the growth of interaction paths against roughly constant human capacity as the reason the second kind displaces the first. We take that as context, not as a premise. Nothing below depends on it.

2.2 Coalgebras

We use only the elementary theory, in the form set out by Rutten (15) and Jacobs (5), and record it here to fix notation rather than to introduce it. Fix the category $\mathbf{Set}$. For a functor $F \colon \mathbf{Set}\to \mathbf{Set}$, an $F$-coalgebra is a pair $(X, c)$ with $c \colon X \to F X$, and a homomorphism $f \colon (X, c) \to (Y, d)$ is a function with $d \circ f = F f \circ c$. These form a category $\mathbf{Coalg}(F)$. A final $F$-coalgebra is a terminal object $(\nu F, \iota)$ of that category. When it exists, each $(X, c)$ carries a unique homomorphism $[\![-]\!]_{c} \colon X \to \nu F$, the behaviour map. An $F$-bisimulation between $(X, c)$ and $(Y, d)$ is a relation $\mathcal{B} \subseteq X \times Y$ carrying an $F$-coalgebra structure making both projections homomorphisms.

Two standard facts are used. First, every finitary $\mathbf{Set}$-endofunctor, that is, one preserving filtered colimits, is accessible and therefore has a final coalgebra. Second, when $F$ preserves weak pullbacks, bisimilarity coincides with behavioural equivalence, so two states have equal behaviour exactly when some bisimulation relates them. Both are in (15, 5).

The homomorphism condition carries the weight below. If $c$ says what can be observed at a state and where the state can go, then $d \circ f = F f \circ c$ says that observing at $f(x)$ agrees with observing at $x$. It also says that the successors of $f(x)$ are the $f$-images of the successors of $x$. Several results below are failures of exactly this condition for maps one would like to be homomorphisms, such as “restrict the store to one namespace”.

2.3 Bitemporal data

The temporal database literature distinguishes two independent time dimensions (6, 17). Valid time is when a fact is asserted to hold in the modelled world. Transaction time is when the system recorded the assertion. A relation is bitemporal when each tuple carries timestamps in exactly one valid-time and one transaction-time dimension. The distinction is not decoration. It is what separates two situations that a single-axis log conflates: a fact about the past that we learn late, and a fact about the present that has just changed.

For an agent the distinction has an operational reading. Transaction time answers “what did the system have on file at $t$”. Valid time answers “what was actually the case at $t$”. Their combination answers “what did the system believe at $t_{2}$ about the state of the world at $t_{1}$”, which is the question an audit of an agent’s decision requires. We use the series symbols $\tau_{v}, \tau_{t}$ for the two axes.

2.4 Notation

$\mathbb{T}$ is a linear order. For a set $X$ we write $X_{\bot} = X + \{\bot\}$, $X^{\ast}$ for the set of finite sequences over $X$, and $\mathcal{P}_{\mathrm{fin}}(X)$ for the set of finite subsets of $X$. For sets $X, Y$ we write $X \rightharpoonup_{\mathrm{fin}} Y$ for the set of finite partial functions and $\mathrm{dom}(f)$ for the domain of $f$. Repository names are set as ContextFS; code identifiers and paths as memory_lineage.py. All ContextFS line references are to commit a93035d.

3 The formal model

3.1 Identifiers, records, relations

Neither closure condition is imposed on $S$. Both are properties that a realisation may or may not maintain, and Section 5 reports which of them ContextFS maintains.

We define $\uplus$ with this side condition because disjointness of record identifiers is what a reading of ContextFS’s own tenancy boundary suggests, and because seeing precisely where it is too weak is one of the results of Section 6. It is not the operator we end up recommending. Proposition 6.4 shows that $\uplus$ does not preserve lineage behaviour, and Definition 6.5 refines it to the operator that does. The refinement requires disjointness of the identifiers a store mentions in either component rather than only in its record map. A reader who wants the compositional structure alone, without the diagnosis, may take Definition 6.5 as the definition and Proposition 6.6 as its property.

$\uplus$ places no condition on edges. Two stores with disjoint record domains may carry edges pointing into each other’s records, and their union will too. This is deliberate: the implementation places no such condition either (Proposition 5.30).

3.2 The operation alphabet

3.3 The store coalgebra

Definition 3.15 is the only thing later Parts need from this Part in order to speak about memory as a component. It deliberately says nothing about record schemas: schema validation belongs to the $\mathrm{Know}$ component in the sense fixed by Part IV, not to the state space.

3.4 The lineage coalgebra

The store coalgebra models what the API does. It does not directly model what a lineage query returns, because a lineage query is about one memory, not about the whole store. We therefore give a second coalgebra, on the identifiers of a fixed store.

Concretely, $[\![i]\!]^{-}_{s}$ is the ancestry unfolding of $i$: the record at $i$, together with the labelled ancestry unfoldings of everything $i$ was derived from, to any depth. This is the object a lineage query approximates, and it is the object Theorem 5.7 says is stable.

3.5 Bitemporal store observations

3.6 The laws

We now fix what it means for a lineage realisation to be well behaved. The laws are chosen so that each can be settled for a candidate implementation by reading its source, and so that each failure has an operational consequence rather than only an aesthetic one.

L1 and L7 are structural: they say the carrier grows and stays connected. L2 and L3 are redundancy laws: they say that two ways of recording the same fact do not diverge. L4 and L5 are locality laws: they say an operation depends only on what it names and on what its interface admits to reading. L6 is the temporal law.

Two remarks on the statement of L4. Its first clause is restricted to $A_{\nu}(s)$ deliberately. Asking $\pi_{\nu}$ to be an endomorphism for the whole alphabet would make the law false for any realisation whatever, since $\mathsf{recall}(i)$ for $i$ outside the fibre returns a record before restriction and an error after it. A law that no realisation can satisfy tells one nothing about the realisation at hand. The interesting question is whether operations that stay inside a namespace have effects that stay inside it, and that is clause (i). Clause (ii) is the separate question of whether an operation can pull payload across the boundary, and it is the clause that fails below. The seven laws are not independent in a logical sense, but no one of them entails another for the implementation we examine, and each is settled separately in Section 5.

3.7 The derivation schema

The positive results of Section 5 are theorems about any realisation whose derivation operations have the following shape. Isolating that shape as a hypothesis lets the mathematics be proved once, independently of any repository, and lets the reading of the source enter at exactly one point (Lemma 5.6).

S4 is the load-bearing clause. A derivation call may attach an ancestry-labelled edge only to an identifier it has just created. It may attach an edge to a pre-existing identifier only in the descendant direction, or with a label outside the ancestry vocabulary altogether. Everything in Section 5.2 follows from that clause.

4 The system

ContextFS is a memory layer for coding agents, written in Python. At commit a93035d its state lives in a SQLite database, with an optional vector store for similarity search and an optional graph database for edge queries. SQLite is the authoritative store on every write path (storage_router.py, save, line 89). Three surfaces expose the same operations: a Python facade (core.py, class ContextFS, line 34), a Model Context Protocol server (mcp/fastmcp_server.py) and a command line (cli/memory.py). Throughout this paper, ContextFS paths are relative to src/contextfs/ in the repository at /Users/mlong/Documents/Development/contextfs-ai/contextfs, and line numbers are those of commit a93035d.

4.1 Model to code

Table 1 gives the correspondence. Every identifier in the right-hand column was read at a93035d before being listed.

4.2 The relation vocabulary

Listing 1 shows the head of the label enumeration. At a93035d it has twenty-two members, of which twenty appear in the inverse table of EdgeRelation.get_inverse and two, DEPENDS_ON and IMPLEMENTS, do not and therefore fall through the table’s default.

Listing 1. src/contextfs/storage_protocol.py, lines 32-49 with the class docstring and blank lines elided, commit a93035d. The first six of the twenty-two labels.

class EdgeRelation(str, Enum):
    # Evolution relationships
    EVOLVED_INTO = "evolved_into"
    EVOLVED_FROM = "evolved_from"
    # Merge relationships
    MERGED_INTO = "merged_into"
    MERGED_FROM = "merged_from"
    # Split relationships
    SPLIT_INTO = "split_into"
    SPLIT_FROM = "split_from"

4.3 Derivation

Listing 2 is the core of $\mathsf{evolve}$. Three features matter below. A new Memory is constructed rather than the original mutated. The ancestry is written into the new record’s metadata unconditionally. The two edges are written inside an exception handler that logs and continues.

Listing 2. src/contextfs/memory_lineage.py, lines 147-182 abridged, commit a93035d. Four constructor keyword arguments (summary, source_repo, project, source_tool) are elided.

evolved = Memory(
    content=new_content, type=original.type, tags=tags,
    namespace_id=original.namespace_id,
    metadata={**original.metadata,
              "evolved_from": memory_id,
              "evolution_timestamp": datetime.now(timezone.utc).isoformat(),
              "change_reason": reason.value})
self._storage.save(evolved)
try:
    self._storage.add_edge(from_id=evolved.id, to_id=memory_id,
                           relation=EdgeRelation.EVOLVED_FROM)
    self._storage.add_edge(from_id=memory_id, to_id=evolved.id,
                           relation=EdgeRelation.EVOLVED_INTO)
except Exception as e:
    logger.warning(f"Failed to create evolution edges: {e}")

merge and split follow the same shape: construct new records, write merged_from or split_from into metadata, then attempt the edge pairs inside a handler. supersede writes only edges, with the timestamp in the edge metadata.

Listing 3 shows the attribute selection performed by merge under the default union strategy. The namespace and type of the merged record are selected here and in the constructor call at line 256, and both selections are the subject of results in Section 5.

Listing 3. src/contextfs/memory_lineage.py, two non-adjacent excerpts, commit a93035d: lines 298-307 (the union branch of _apply_merge_strategy, with its comments elided) and line 256 (the namespace argument of the merged record's constructor). The two are separated below by an inserted marker line.

if strategy == MergeStrategy.UNION:
    all_tags = [tag for m in memories for tag in m.tags]
    combined_meta = {}
    for m in memories:
        combined_meta.update(m.metadata)
    types = [m.type for m in memories]
    final_type = max(set(types), key=types.count)
### line 256, in the merged record's constructor:
            namespace_id=memories[0].namespace_id,

4.4 Observation

Two observation paths exist and they are not the same. recall resolves an identifier against SQLite by prefix (Listing 4). Timeline.at answers the timed question over an in-memory version list (Listing 5).

Listing 4. src/contextfs/storage_router.py, lines 310-326 abridged, commit a93035d.

def _recall_from_sqlite(self, memory_id: str) -> Memory | None:
    conn = sqlite3.connect(self._db_path)
    cursor = conn.cursor()
    try:
        cursor.execute(
            "SELECT * FROM memories WHERE id LIKE ? AND deleted_at IS NULL",
            (f"{memory_id}
        )
        row = cursor.fetchone()
        if row:
            return self._row_to_memory(row)
        return None
    finally:
        conn.close()

Listing 5. src/contextfs/types/versioned.py, lines 238-263 abridged, commit a93035d.

def at(self, timestamp: datetime) -> VersionEntry[S] | None:
    ts = timestamp
    if ts.tzinfo is None:
        ts = ts.replace(tzinfo=timezone.utc)
    result = None
    for entry in self.entries:
        entry_ts = entry.timestamp
        if entry_ts.tzinfo is None:
            entry_ts = entry_ts.replace(tzinfo=timezone.utc)
        if entry_ts <= ts:
            result = entry
        else:
            break
    return result

Timeline.at compares against a single timestamp field of VersionEntry (types/versioned.py:117). There is no second time field to compare against, which is the content of Theorem 5.27.

4.5 The agent-facing surface

Listing 6 shows the tail of the facade’s evolve. The reason parameter of MemoryLineage.evolve is not among the arguments forwarded, so the default ChangeReason.OBSERVATION is used. The Model Context Protocol tool (mcp/fastmcp_server.py:623) and the command line (cli/memory.py:247) call this same facade method and likewise do not expose a change reason.

Listing 6. src/contextfs/core.py, lines 1545-1554, commit a93035d.

if preserve_tags is None:
            preserve_tags = self.config.lineage_preserve_tags

        return self._lineage.evolve(
            memory_id=memory_id,
            new_content=new_content,
            summary=summary,
            preserve_tags=preserve_tags,
            additional_tags=additional_tags,
        )

5 Law checking

Throughout this section $(S, \alpha)$ is the lineage realisation given by ContextFS at a93035d under the correspondence of Table 1, with $\mathcal{R}^{-}= \{\texttt{EVOLVED\_FROM}, \texttt{MERGED\_FROM}, \texttt{SPLIT\_FROM}\}$. Every claim about the code is a claim about the source at that commit.

5.1 L1, record monotonicity

5.2 Stable ancestry

L1 says records survive. It does not say that what can be observed about a record survives, and in general it does not: evolve adds an EVOLVED_INTO edge out of the original, so the original’s outgoing edge set changes. The content of the following theorem is that the change is confined to the descendant direction.

The hypothesis of ancestry closure needs justifying rather than assuming, because Proposition 5.30 below shows that L7 fails: not every store of $S$ is ancestry-closed. What rescues the theorem is that ancestry closure is an invariant of the fragment the theorem is about, so the relevant stores are not merely hypothetical.

The asymmetry is the useful content. A consumer of ContextFS may cache the ancestry of a memory and rely on it. It may not cache the descendants. In the terms of the series, this is the structural property the memory layer contributes to any composite that contains it, and Section 6 states what a skill or a harness is entitled to conclude from it.

5.3 L2, edge and record agreement

5.4 L3, inverse closure

5.5 L4, namespace locality

The two clauses of L4 come apart, and which one holds is the useful information.

5.6 L5, resolution independence

5.7 Merge up to bisimilarity

L5 concerns one field of the merged record. The wider question is what algebraic laws merge obeys. The obvious answer, that it obeys none since every call allocates a fresh identifier, is an artefact of comparing states on the nose. The right comparison for a coalgebra is behavioural, and under it one of the three candidate laws holds.

5.8 L6, bitemporality

The result is stronger than counting timestamp fields. The store contains created_at, updated_at, several timestamp metadata keys, timestamps on VersionEntry, and a temporal ordering implicit in the ancestry graph. The theorem quantifies over every function of the whole store, so none of those representations can recover valid time for the recording map $\Psi$.

5.9 L7, lineage referential integrity

5.10 Summary

Table 2 collects the results. The passing clauses are enforced by the shape of the code, and what fails would require a check the code does not perform. Monotonicity holds because the derivation methods construct new objects and never assign to retrieved ones; inverse closure holds because the two writes are adjacent statements; confinement holds because every constructed record takes its namespace from a named argument. Construction locality, resolution independence, bitemporality and referential integrity would each require an explicit comparison, an explicit tie-break, an extra field, or a constraint, and none is present. Counted by clause, three hold and five fail.

6 Composition with adjacent layers

6.1 Layer contribution

A composite that contains a memory coalgebra gains one structural property that is not available from a stateless component: an observation that survives further activity. The following corollary states the form a consumer can use.

The hypothesis matters. Corollary 6.1 covers derivation calls only, so a composite that also issues $\mathsf{save}$ under an existing identifier, or a deletion, is outside it; by Proposition 5.2 both of those can change an ancestry that a consumer has already read.

6.2 Memory composition

Before asking how memory composes with skills or with a harness, we ask how it composes with itself, since a harness that hosts several agents hosts several stores. The candidate operation is $\uplus$ of Definition 3.5, and the question is whether operations are stable under enlarging the surrounding store.

The lineage observation fails to compose for a different reason, which is worth separating from the identifier question because it survives resolution by equality.

Proposition 6.4 says that domain-disjoint union is the wrong composition operator for isolation: two tenants with disjoint record identifiers may still interfere, because one’s dangling edge can acquire a target from the other. The repair is to strengthen the side condition, and with the stronger one the composition behaves.

The conclusion for composition is narrow and usable: memory stores compose by disjoint union for every operation that names full identifiers, and do not compose for the one operation that resolves abbreviations. A harness that shares one store across tenants must either resolve identifiers by equality or partition the identifier space, and namespaces do not partition it, because Listing 4 does not filter on namespace_id.

6.3 Composition with skills

Part II treats skills as operations of a coloured operad and takes the memory carrier as one of the colours a skill may consume and produce. What this Part supplies is Definition 3.15, the type $\mathsf{Mem}$ of a handle on the carrier, and nothing else: in particular it does not supply a schema-indexed family of colours, because record schemas belong to the $\mathrm{Know}$ component in the sense fixed by Part IV rather than to the state space.

Two of the results above have direct consequences for a skill composite. A skill that reads the ancestry of a memory early in a composite and uses it late is sound by Corollary 6.1, provided no step of the composite deletes a record or saves under an existing identifier. A skill composite that is scoped to a namespace does not thereby scope its memory effects to that namespace, by Proposition 5.18 and Remark 5.19: a merge issued inside the composite may name arguments in another namespace and will file the result in the namespace of its first argument. Scoping a composite is therefore not the same as scoping the state it touches, which is exactly the kind of gap the operadic reading of Part II cannot see, because operad substitution constrains the composition of operations and not the effects of the operations composed.

Part II does carry one mechanism that bears on this (10). Its operations are graded by an effect class, and as stated there an operation whose input colour is $\mathsf{Mem}$ is not pure, so the grading determines where such an operation may be scheduled relative to its siblings. That grading orders memory-touching operations relative to one another. It does not bound which records they touch, which is what Proposition 5.18 is about, so the two mechanisms are complementary rather than overlapping.

6.4 Composition with the harness

A harness surrounds a model with memory, tools, wiring and policy, and the Architecture triple $(G, \mathrm{Know}, \Phi)$ is one categorical account of that layer (14, 1). We use only the boundary fixed in Section 1.4: $\mathrm{Know}$ is a collection of checkable statements $\mathrm{cert}$, and $S$ is the coalgebraic state. Applied to ContextFS, the schema registry (types/registry.py, class SchemaRegistry, line 23) and the structured-data validation performed by Memory’s model validator (schemas.py:1411) are $\mathrm{Know}$-level: they are checks on records rather than records. The record store and the edge set are $S$.

What Theorem 5.27 contributes to that discussion is a limit on what a $\mathrm{Know}$-level check over memory can be: no check evaluated against a ContextFS store at a93035d can have the form “at transaction time $\tau_{t}$ the system believed $P$ of the world at valid time $\tau_{v}$”, because the store does not distinguish the second parameter.

The boundary has a consequence on both sides. As stated in Part IV (12), the harness carries a projection of session content into its own store, which is state but is neither a certificate nor a memory coalgebra in the sense of Definition 3.14: it has no derivation operations and no lineage edges. The same negative reading applies in the protocol layer, where, as stated in Part III (11), the append-only operation chain of CatDB is a wire-level ordering discipline and not a structure map $\alpha \colon S \to F S$. We agree with both readings. What makes a store a memory coalgebra on this account is not persistence and not an ordering on writes; it is the presence of derivation operations whose lineage is observable, which is what Definition 3.7 asks for and what neither of those two stores has.

One cross-cutting dependency runs against the presentation order. A skill may call a memory operation at run time, so the companion treatment of skills depends on this one operationally, while nothing here depends formally on any companion. At the pinned commits this is a composition of models rather than of running code: AgentHero at 1c3ad24 declares no dependency on ContextFS, as reported in companion work on the harness (12).

7 Limits and counterexamples

Four laws fail in Section 5. Further limits concern the cost of repairing the temporal gap, the second unpersisted memory model in ContextFS, and the part of the system the coalgebraic reading does not reach at all.

7.1 Bitemporal repair

Theorem 5.27 is a statement about a record schema, not about an architecture, and the corresponding repair is small. We state it as a proposition about the model so that it is clear the lineage machinery survives unchanged.

7.2 Repository memory models

The analysis above concerns the persisted model: records in SQLite, edges in memory_edges, derivation through MemoryLineage. ContextFS also contains a second, richer memory model in types/versioned.py, and at a93035d the two do not meet.

The second model is the one that would satisfy more of Definition 3.21. VersionEntry (line 87) carries a reason drawn from the four-valued ChangeReason and an author; Timeline (line 175) keeps entries sorted by timestamp and offers at, since and by_reason; VersionedMem (line 306) adds an authoritative-version pointer and a checkable invariant, is_consistent (line 576), which tests that timestamps are monotone, that all entries share a memory identifier, and that no version identifier repeats. That invariant is exactly the kind of internal consistency L2 and L3 ask for, and it is stated and checkable in the source.

It is, however, not reachable from the store. A VersionedMem is constructed on demand by Memory.as_versioned (schemas.py:1995) or Mem.as_versioned (types/memory.py:278), both of which call VersionedMem.from_memory (types/versioned.py:359); that constructor builds a timeline containing at most one entry, derived from the single record it is given, and only when that record has non-empty structured_data (lines 383–396). No code path in storage_router.py or memory_lineage.py at a93035d persists a Timeline or a VersionEntry, and the memories table (core.py:203--220) has no column for one. The alternative constructor VersionedMem.from_lineage (line 402) reconstructs a timeline from lineage history dictionaries, so the richer model is designed to be derived from the poorer one rather than to replace it.

The consequence for this paper is a scope statement. The results of Section 5 are about the persisted model, which is the one an agent reaches through the facade, the Model Context Protocol server and the command line. They are not claims about types/versioned.py, whose is_consistent may well hold of every timeline it constructs. The consequence for the system is a question rather than a defect: the module that reasons about why a belief changed is the module whose output is not written down.

7.3 Missing run-scoped state

7.4 Coalgebraic scope

The most useful limit to state is the one where the model has nothing to say. ContextFS is not only a lineage store; it is a retrieval system, and retrieval is how an agent actually uses it. ContextFS.search (core.py:968) and StorageRouter.search (storage_router.py:435) route queries to a full-text index and, when configured, to a vector store. Neither is an observation of $(m_{s}, E_{s})$ in the sense of Definition 3.14, and the reason is visible in the write path. StorageRouter.save (line 89) commits the record to SQLite first, described in the source as authoritative, and then attempts the vector-store write inside try: ... except Exception as e: logger.warning(...) (lines 103–106), followed by an optional graph synchronisation under a second handler (lines 109–113). The vector index is therefore not determined by the record store along every path in the code, and even where it is, the result of a similarity query depends on an embedding function and on index parameters that are not part of the state.

One could enlarge the state space to include the index. That would be honest but not useful: the enlarged state would have no laws, because nothing in Definition 3.21 constrains an approximate nearest-neighbour structure, and the enlarged coalgebra’s behaviours would distinguish states that no consumer can distinguish. The better description is that ContextFS has two faces. The lineage face is a coalgebra with checkable laws and one proved stability property. The retrieval face is a ranking function over the same records, and the vocabulary that fits it is information retrieval, not universal coalgebra. Reporting the correspondence for the first face and declining it for the second is the scoped claim of Section 1.1 applied honestly to this pillar.

8 Related work

8.0.0.1 Coalgebra for systems.

The identification of state-based systems with coalgebras for a $\mathbf{Set}$-endofunctor, and of behavioural equivalence with the kernel of the map into a final coalgebra, is Rutten’s (15); Jacobs’s book is the standard extended treatment (5). Our two functors are unremarkable within that framework: $F X = (\mathrm{Out}\times X)^{A^{+}}$ is a deterministic machine with input and output, and $H X = \mathrm{Rec}_{\bot} \times \mathcal{P}_{\mathrm{fin}}(\mathcal{R}\times X)$ is a finitely branching labelled transition system with state observations. What is specific here is the use to which the framework is put. We do not construct a final semantics for ContextFS; we use finality only in Corollary 5.12, and the substantive work is the identification of the sub-functor $H^{-}$ for which the inclusion of existing identifiers is a homomorphism. Restricting a labelled transition system to a sub-alphabet in order to recover a homomorphism that fails on the full alphabet is a standard move; applying it to separate the immutable and mutable directions of a lineage graph appears not to have been done for agent memory.

8.0.0.2 Temporal databases.

Valid time and transaction time as independent dimensions, and the definition of a bitemporal relation as one timestamped in exactly one of each, are due to the temporal database community; Jensen and Snodgrass give the consensus semantics (6) and Snodgrass’s book the practical treatment (17). Theorem 5.27 is a negative result relative to that literature, and it is worth being clear about what is and is not new in it. That an append-only log with one clock cannot answer valid-time queries is not new. What the theorem adds is the precise form of the failure for a system whose designers describe it as history preserving: the recording map identifies histories that differ in valid time, so the deficiency is in the schema and not in the query implementation, and no improvement to Timeline.at could recover the distinction.

8.0.0.3 Immutability and merge.

The design pattern of deriving new records rather than mutating old ones, and of treating the accumulated log as the system of record, is argued for at length by Helland (4). ContextFS’s derivation operations follow it. The merge operation is closer to the conflict-free replicated data type literature (16). The failure identified in Proposition 5.20 has a familiar form: the result depends on something other than the states being merged. The comparison has to be made at the right level, though. Asking for idempotency on the nose is a category error for an operation that allocates a fresh identifier on every call, and the correct question for a coalgebra is whether the resulting states are behaviourally equivalent. Proposition 5.24 settles that question positively: under an observation blind to allocation, merging the same arguments twice yields a store bisimilar to merging them once. Proposition 5.25 settles the other direction negatively, and identifies the two order-sensitive fields responsible. The difference from a replicated data type is therefore not that ContextFS’s merge fails the lattice laws outright, but that it satisfies one of them only after quotienting and fails the other by design, since it records provenance in argument order.

8.0.0.4 Typed agent memory.

A prior paper by the present author describes a typed memory layer for an agent operating system in Elixir, with schema registries, causal versioning and a graph relationship manager (8). That work and this one share a name for their reference implementation and little else: it is a design paper about a different runtime, it argues from the type system rather than from coalgebraic laws, and it makes no bitemporal claim. It is cited here as prior art by the same author, and its numbering is unrelated to this series: its Part III is a memory paper, this series’ Part III is about protocols.

8.0.0.5 The four pillars and the Architecture triple.

Zhou et al. supply the pillar taxonomy (20); de los Riscos, Corbacho and Arbib supply the Architecture triple (14); Banu proposes the correspondence between them and validates it against one reference implementation (1). Meng et al. give the alternative enumerative taxonomy of harness components (9), and Liu’s typed lambda calculus for agent composition is a different formal route to the same territory (7). Cao’s argument for why externalization is happening at all is economic and complexity-theoretic rather than structural (2). This paper contributes one row of the correspondence, checked against a system that was not built with the correspondence in mind, and reports the row as partial; the remaining three rows and the question of where the correspondence stops paying for itself are taken up in companion work (10, 11, 12, 19).

8.0.0.6 Operads and wiring.

Companion treatments of skills and protocols use the operad of wiring diagrams and its typed refinements (10, 11, 18, 3). We mention the line only to place the boundary: the memory coalgebra composes with itself by the partial monoid of Proposition 3.6, and the operadic machinery those Parts need is not required here.

9 Open problems

Each problem has an explicit criterion for resolution.

1. The second axis. Proposition 7.1 shows a valid-time field is sufficient to make the observation non-degenerate. It does not show what the derivation operations should do with valid time when their arguments disagree. If merge receives three records with three valid-time instants, no choice among “earliest”, “latest” and “the interval spanned” is forced by the model, and the correct answer plausibly depends on the record type. Settled by: a merge rule for valid time whose induced observation satisfies a stated law, together with a proof that the law fails for the other candidate rules.

2. A merge that reads only what it is given. Proposition 5.20 identifies a tie-break that reads an ambient enumeration order. A one-line change repairs that merge path but not L5 globally, because prefix recall has a second order-dependent choice (Proposition 6.3). Deterministic resolution would be required as well. The merge change does not settle the algebraic question, which Proposition 5.24 and Proposition 5.25 leave in an odd state: idempotent up to allocation-blind bisimilarity, and not commutative, because the merged record records its sources in argument order. Whether a lineage merge should be commutative at all is genuinely unclear, since argument order is provenance. Settled by: either an argument-order-blind merge whose provenance is recovered from the edge set rather than from the content, together with a proof that it is commutative up to Definition 5.23, or a proof that no such merge can distinguish histories the current one distinguishes.

3. One ancestry representation. Proposition 5.14 and Remark 5.15 describe two representations, two fallbacks and two entry shapes. The question is not which to keep, since keeping the edges and deriving the metadata is the obvious answer, but what to do about stores already written under the current scheme, where the two representations may already disagree and there is no record of which is right. Settled by: a reconciliation procedure whose output is a store satisfying L2, together with a statement of what it does when the two representations conflict.

4. Identifier resolution and composition. Proposition 6.3 makes the frame property conditional on resolution by equality, and Remark 6.8 gives the scale at which the condition starts to bite. The open question is whether a namespace-scoped resolution rule restores Proposition 6.2 in full, given that Proposition 5.18 shows namespaces are not respected by every operation. Settled by: either a proof that prefix resolution scoped to a namespace satisfies the frame property, or a counterexample of the same shape as Proposition 5.18.

5. Persisting the version model. Section 7.2 describes a module whose invariant is_consistent is exactly the internal-agreement property L2 and L3 approximate, and which is never written down. Whether the persisted lineage graph and a persisted timeline can be kept in agreement, and at what cost, is open. Settled by: a mapping from lineage graphs to timelines together with a proof that it takes stores satisfying L1 to L3 to timelines satisfying is_consistent.

6. Deletion. Every result in Section 5.2 carries the hypothesis that the operation is a derivation call, and Proposition 5.2 shows why. A memory system that must support erasure cannot be monotone, so the question is what weakening of Theorem 5.7 survives a deletion operation that is required to remove content while retaining the shape of the ancestry. Settled by: a coalgebra on stores-with-tombstones for which the analogue of Theorem 5.7 holds and under which erased records are not recoverable.

10 Conclusion

For ContextFS at commit a93035d, the coalgebraic model establishes that a record’s ancestry is invariant under later derivation on the ancestry-closed fragment, while its descendants may change. Five law clauses fail with named source witnesses, and the retrieval subsystem lies outside the useful scope of the coalgebraic account.

Three failures share one cause: merge typing, prefix resolution, and deletion consult an enumeration order that no interface declares. L5 exposes that hidden dependency directly. The strongest conclusion is therefore local: the model earns its cost where it converts implementation details into falsifiable stability and independence claims, and should not be extended to retrieval ranking merely to preserve a uniform vocabulary.

11 Code evidence

Every code-backed claim in the body has a row below. Repository ContextFS is at /Users/mlong/Documents/Development/contextfs-ai/contextfs, commit a93035d; agent-os is at /Users/mlong/Documents/Development/agentherowork/agent-os, commit 61cb399. ContextFS paths in the third column are relative to src/contextfs/; the one agent-os path is relative to the repository root. Statements in the last column are implementation-level claims established by reading the file at the stated path and lines at the stated commit, not reports of runtime behaviour.

References

[1] B. Banu. Harness engineering as categorical architecture. arXiv:2605.12239, 2026.

[2] Z. Cao. The end of software engineering: how AI agents are fundamentally restructuring the software paradigm. arXiv:2606.05608v1, 2026. Retitled “Agentic software: how AI agents are restructuring the software paradigm” in a later version; citations here are to v1.

[3] B. Fong and D. I. Spivak. Seven sketches in compositionality: an invitation to applied category theory. arXiv:1803.05316, 2018.

[4] P. Helland. Immutability changes everything. Communications of the ACM, 59(1):64–70, 2016. DOI 10.1145/2844112.

[5] B. Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science 59. Cambridge University Press, 2016. ISBN 9781107177895.

[6] C. S. Jensen and R. T. Snodgrass. Semantics of time-varying information. Information Systems, 21(4):311–352, 1996. DOI 10.1016/0306-4379(96)00017-8.

[7] Q. Liu. $\lambda_{A}$: a typed lambda calculus for LLM agent composition. arXiv:2604.11767, 2026.

[8] M. Long. The AI operating system, Part III: memory layer, a typed filesystem for persistent agent cognition. YonedaAI Research Collective, 2026.

[9] Q. Meng, Y. Wang, L. Chen, W. Wu, Y. Li, W. Jiang, Q. Wang, C. Lu, Y. Gao, Y. Wu, and Y. Hu. Agent harness for large language model agents: a survey. Preprints, 2026. DOI 10.20944/preprints202604.0428.v2.

[10] M. Long. Operadic skill composition. Unpublished Part II manuscript in the Agentic Engineering repository, The YonedaAI Collaboration, 2026. https://github.com/YonedaAI/agent-engineering.

[11] M. Long. Typed protocol wiring. Unpublished Part III manuscript in the Agentic Engineering repository, The YonedaAI Collaboration, 2026. https://github.com/YonedaAI/agent-engineering.

[12] M. Long. Harness architecture. Unpublished Part IV manuscript in the Agentic Engineering repository, The YonedaAI Collaboration, 2026. https://github.com/YonedaAI/agent-engineering.

[13] Python Software Foundation. The Python language reference: PYTHONHASHSEED and hash randomisation. https://docs.python.org/3/using/cmdline.html#envvar-PYTHONHASHSEED, accessed 2026.

[14] P. de los Riscos, F. J. Corbacho, and M. A. Arbib. Working paper: towards a category-theoretic comparative framework for artificial general intelligence. arXiv:2603.28906, 2026.

[15] J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. DOI 10.1016/S0304-3975(00)00056-6.

[16] M. Shapiro, N. Preguiça, C. Baquero, and M. Zawirski. Conflict-free replicated data types. In Stabilization, Safety, and Security of Distributed Systems (SSS 2011), LNCS 6976, pages 386–400. Springer, 2011. DOI 10.1007/978-3-642-24550-3_29.

[17] R. T. Snodgrass. Developing Time-Oriented Database Applications in SQL. Morgan Kaufmann, 2000.

[18] D. I. Spivak. The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits. arXiv:1305.0297, 2013.

[19] M. Long. The End of Software Engineering and the Rise of Agentic Engineering. Unpublished synthesis manuscript in the Agentic Engineering repository, The YonedaAI Collaboration, 2026. https://github.com/YonedaAI/agent-engineering.

[20] C. Zhou, H. Chai, W. Chen, et al. Externalization in LLM agents: a unified review of memory, skills, protocols and harness engineering. arXiv:2604.08224, 2026.