TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory Ziming Wang The Hong Kong University of Science and Technology Hong Kong, Hong Kong SAR [email protected] Table 1: Production contradiction-resolution strategies as isolation-typed operators. Each row pairs an operator with its typed contract and exposed Berenson–Adya anomaly [2, 7].
arXiv:2606.06240v1 [cs.DB] 4 Jun 2026
ABSTRACT Persistent memory for an LLM agent is a write-heavy substrate: every belief update is a versioned write, and the system must decide what to trust when a new claim contradicts a stored one. Production systems answer with four resolution heuristics, last-writer-wins, evidence-weighted merge, await-confirmation, and per-rule policy, yet none declares the isolation level it assumes or the write-time anomalies it admits. We show that contradiction resolution is writetime concurrency control, and make the missing contract explicit. Toki types the four heuristics as one family of bitemporal operators over a dual-row schema, each carrying an isolation precondition and a provenance annotation that preserves the losing fact in an audit row. Four soundness theorems close the contract across three orthogonal axes, isolation, schema, and provenance, lift the guarantees to operator pipelines, and extend the fold operators to n-ary conflict sets. A tightness companion proves the sharp result: within the relational schedule model, keyed logging of the adjudicating judge is necessary for replay consistency, a discipline every deployed baseline we audit omits. A verdict matrix over eight systems localizes the gap: every baseline that keeps a language-model judge on the write path admits at least one of three write-time anomalies, replay inconsistency, belief-drift skew, or audit erasure; a content-addressed engine-layer comparator avoids them only by removing the judge, and Toki alone excludes all three while keeping it. On its one natural-workload slice, the audit-row defence moves LoCoMo accuracy by 0.86, and ablating the typed memory layer removes 0.49 accuracy on 1,444 answerable LoCoMo questions; the cross-system comparison against external memory systems stays underpowered and claims no superiority. The contribution is the contract: a write-time correctness specification, proved sound across isolation, schema, and provenance, that pins the guarantee every production heuristic assumes and no deployed system makes explicit.
1
Production strategy
Isolation precondition
Admitted anomaly
Last-writer-wins ( ⊕t ) Evidence-weighted ( ⊕p ) Await-confirmation ( ⊕? ) Per-rule policy ( ⊕c )
Read-committed Snapshot isolation RC + callback SR on policy table
𝑃 4 lost update 𝐴5𝐵 write skew callback boundary 𝑃3 phantom
is measurable. BeliefShift [51, Tab. 5] leaves up to 42% of crosssession contradictions unresolved across seven language-model families. TSM [67] recovers 12.2 accuracy points on LongMemEval and LoCoMo by separating dialogue time from occurrence time, an axis production memories collapse. Adversarial writes corrupt later retrievals [57] once the store keeps no defensible record of what it overwrote. Deployed agent-memory systems carry no name for these failures: our deployment scan of widely used implementations (Appendix D) finds isolation, contradiction, audit, and bitemporal vocabulary largely absent. Concurrency control already solved the structural version of this problem. The isolation hierarchy of Berenson and Adya [2, 7] fixes which anomalies a level admits when writers race; bitemporal data models [66] and K-relation provenance [30] fix how versioned facts and their lineage are stored and recovered. Toki ports that machinery to the agent write path. It types the four heuristics as one family of bitemporal operators over a dual-row schema, each carrying an isolation precondition and a provenance annotation that keeps the losing fact in an audit row (Figure 1, Table 1). The classical anomaly alphabet, written for human transactions, cannot name three failures an LLM judge introduces: replay inconsistency, when re-adjudicating the same contradiction returns a different winner; belief-drift skew, when concurrent confidence revisions corrupt a subject-predicate partition; and audit erasure, when the overwritten fact becomes unrecoverable. Toki binds each failure to a point in the classical machinery, so each one inherits a defence with a soundness proof.
INTRODUCTION
Persistent memory for an LLM agent [53, 54] is a write-heavy data management substrate: every belief update is a versioned write that carries a valid time, a system time, a provenance annotation, and an implicit isolation level. When a new writer disagrees with the stored belief on a subject-predicate key, the memory must decide what to trust. Production systems answer with four strategies, last-writerwins, evidence-weighted merge, await-confirmation, and per-rule policy. None declares which isolation level the strategy assumes or which write-time anomalies it admits. The cost of that silence
Contributions. (i) A typed operator algebra (§3.2). Toki casts the four production heuristics as one isolation-indexed family of bitemporal operators with a dual-row signature, turning four undeclared heuristics into one contract that states the isolation level it assumes and the provenance it keeps. (ii) A necessity theorem and soundness on three axes (§3.3). A tightness companion proves that keyed logging of the judge is necessary for replay consistency within the relational schedule model, a tight characterisation no weaker discipline meets. An alphabet bridge lifts the classical isolation guards
§ Code, data, and reproducibility artifact: https://github.com/ZenAlexa/tokibitemporal-memory
1
Ziming Wang
Contradicting write pair on key ( , )
bitemporal valid-time × system-time overlap
detect
Isolation-precondition gate dispatch by iso level
⊕ LWW
⊕ Evi
⊕? Await
⊕ Rule
RC
SI
RC+cb
SR
× →( , )
Dual-row write one physical schema, hidden audit-row discriminator current ⋅ winner fact audit ⋅ loser fact + provenance
certified by
Soundness contract iso
schema
provenance
guard map + lower bound
audit-row tight
K-axis + carrier
excludes
Anomaly-sound resolution: N1, N2, N3 excluded
Figure 1: Contradiction resolution as write-time concurrency control. A bitemporal substrate detects a contradicting pair on a subject-predicate key; an isolation gate routes it to one of four typed operators, each pinned to the isolation level that excludes the anomaly a weaker level admits; every operator commits a current row beside an audit row under one schema. The soundness theorems close the isolation, schema, and provenance axes. to the agent write path, and four soundness theorems close the contract on the isolation, schema, and provenance axes and lift it to operator pipelines. (iii) Empirical evidence (§4). A verdict matrix over eight systems shows every agent-memory baseline admits at least one of the three write-time anomalies while Toki excludes all three; controlled experiments then stress each defence and anchor every theorem to a grid whose measured boundary matches the prediction.
2
BACKGROUND
Toki builds on three classical substrates, applied to the LLM-agent write path: the bitemporal data model, multiversion isolation, and K-semiring provenance. This section fixes the core object, the contradiction event the algebra resolves, and the vocabulary §3 uses.
2.1
Bitemporal facts and the contradiction event
The core object of Toki is the bitemporal fact: a subject, predicate, object triple stamped with a valid-time period, a system-time period, a K-relation provenance annotation, and a confidence. Every belief a memory holds is one such fact, and every contradiction is a pair of facts that disagree on a shared key. Seven event types compose every history: 𝑏𝑖 (begin), 𝑟𝑖 (f) (read), 𝑤𝑖 (f) (write), 𝑐𝑖 (commit), 𝑎𝑖 (abort), 𝑗𝑖 (𝑅, 𝜃 ) (judge invocation on read set 𝑅 under decoder tuple 𝜃 = (prompt, seed, model, temperature, tool_hash)), and cb𝑖 (𝑅, ℎ, 𝑘) (external callback for request hash ℎ returning winner index 𝑘). A memory state M ⊆ [Fact] Tv × Ts is a finite set of bitemporal facts, and the view asof(M, 𝑡 𝑣 , 𝑡𝑠 ) returns the currentkind rows whose periods contain (𝑡 𝑣 , 𝑡𝑠 ). Two facts contradict (f1 # f2 ) when they agree on subject and predicate, disagree on object, and their valid-time periods share a common instant. Under the closed-open convention [𝑡 from, 𝑡 to ) this holds for nine of
Result. Keyed logging of the judge is provably necessary for replay consistency within the relational schedule model, and every deployed baseline we audit omits it: each admits at least one write-time anomaly the classical isolation hierarchy already excludes, while Toki excludes all three while keeping the judge on the write path. Mechanism isolation confirms each defence: the audit-row defence moves its natural-workload LoCoMo slice by 0.86, and ablating the typed memory layer removes 0.49 accuracy on 1,444 answerable LoCoMo questions. The cross-system comparison against external memory systems stays underpowered and claims no superiority. The reference implementation, benchmark harnesses, and reproduction runbook are publicly available at the repository linked on the first page.
2
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 2: User-visible bitemporal fact schema with audit discriminator. Cols 1–4 carry fact identity and content; cols 5–8 are the two SQL:2011 periods [37]; col 9 is the K-relation provenance annotation [30]; cols 10–11 are our typed product extension (§2.2). The shaded row is the hidden CHECKbound discriminator that splits the table into current and audit slices and carries the N3 defence of Theorem 2.
Allen’s thirteen base relations [3], all but before, after, meets, and met-by, the four sharing no interior instant. Database time factors into valid time Tv and system time Ts [65, 66] through the SQL:2011 as-of surface [37]. One running example carries the construction through the sections that follow. The incumbent fact 𝑓1 is (alice, medication, penicillin), valid from March; a later writer commits 𝑓2 , (alice, medication, amoxicillin), at system time April 15. The two agree on subject and predicate and disagree on object, so they contradict, their valid-time periods overlapping on a shared instant. Toki resolves the pair with one operator, commits the winner to the current row, and writes the loser to an audit row recoverable at every later system time.
2.2
Isolation levels and provenance semirings
Toki types each operator against an isolation precondition drawn from the multiversion hierarchy. Berenson et al. [7] characterise four ANSI-SQL phenomena 𝑃0 to 𝑃3 and three multiversion anomalies (𝑃 4 lost update, 𝐴5𝐴 read skew, 𝐴5𝐵 write skew); Adya et al. [2] generalize the taxonomy with schedule-history predicates. We model prevention as a guard map over the chain Liso = {RC ⪯ SI ⪯ SR}, and the callback boundary used by ⊕? adds an orthogonal binary axis Lcb = {⊥ ⪯ cb}. Operator preconditions live in the product L = Liso × Lcb , and the table-scoped SRpolicy pins the named policy table to SR. Toki annotates every tuple with provenance so the loser of a resolution stays algebraically recoverable. Each tuple carries an element of a commutative semiring P = ⟨𝐾, ⊕, ⊗, 0, 1⟩ with the natural order 𝑎 ⪯𝐾 𝑏 ⇔ ∃𝑐. 𝑎 ⊕ 𝑐 = 𝑏 [30]. Provenance is a two-sort polynomial W ∈ 𝐾 [𝑋,𝑇 ] with 𝑋 over write-event tokens and 𝑇 over trust and policy variables. Three carriers instantiate the audit-row schema: multilinear N[𝑋,𝑇 ], multidegree N[𝑋,𝑇 ] # (where 𝑥 ⊗ 𝑥 = 𝑥 2 ), and the Boolean reduct. The carrier choice is decorative on the isolation axis and load-bearing on the provenance axis, a separation Toki makes precise in Proposition 1.
3
Type
Role
1 2 3 4 5 6 7
TEXT TEXT TEXT TEXT TIMESTAMP TIMESTAMP TIMESTAMP
primary key (with col. 7) subj pred obj, fact content valid-time period start valid-time period end system-time period start (PK part) system-time period end K-relation annotation 𝑝 ∈ P conf ∈ [0, 1] strat ∈ {⊕t , ⊕p , ⊕? , ⊕c }
fact_id subject predicate object valid_from valid_to system_time_start
8 system_time_end 9 provenance_id
TIMESTAMP TEXT
10 confidence 11 resolution_strategy_id
DOUBLE TEXT
12 row_kind
TEXT
hidden discriminator ∈ { current, audit }
eleven base columns commutes with the audit-discriminator filter (Proposition 5), so the audit row changes no answer a caller relied on.
3.2
Four typed operators
Toki exposes the four production contradiction-resolution strategies as one isolation-indexed operator family. Each operator ⊕𝑎 takes two contradicting facts f1, f2 over the same (subj, pred), returns a winner with a system-time invalidation of the loser, and emits an audit tuple as the second component of the conclusion. The four differ in winner selector, isolation precondition, and strategy stamp: ⊕t (last-writer-wins, RC, exposes 𝑃4 ), ⊕p (evidence-weighted, SI, exposes 𝐴5𝐵), ⊕? (await-confirmation, RC+cb, exposes callback), policy and ⊕c (per-rule, SRpolicy on the policy table, exposes 𝑃 3 ). This pairing drives the correspondence of Table 1.
THE TOKI OPERATOR ALGEBRA
Building on the bitemporal facts and the isolation and provenance vocabulary of §2, Toki lifts the four production contradictionresolution strategies into one typed algebra over a dual-row schema, with the soundness guarantees those operators earn (§3.3) and the reference system that realises them over an unmodified engine (§3.4).
3.1
# Column
Definition 1 (Operator isolation signature). For each 𝑎 ∈ {⊕t, ⊕p, ⊕?, ⊕c }, req(𝑎) ∈ L is the typing precondition and exposes(𝑎) the failure mode exposed by weakening it. The audit tuple is Audit(𝑖 ★, 𝑖) = (𝑓𝑖★ .W ⊕ 𝑓𝑖 .W, strat, 𝑡𝑠 ). The schedule judgement |=𝐿 asserts the writer-slice sub-schedule on {𝑓1, 𝑓2 } violates none of the predicates classically forbidden at level 𝐿.
The dual-row schema
The four inference rules share the dual-row signature and differ in winner selector and strategy stamp: 𝑖𝑡★ under (sf, id) (Lww), 𝑖 𝑝★ under (conf, sf, id) (Evi), cb(𝑓1, 𝑓2 ) from a delivered callback row (Await), and 𝜌 (𝑓1, 𝑓2 ) from a policy row keyed by the unordered identity set (Rule):
The isolation precondition and the provenance annotation of §2.2 meet in one physical layout. Toki lifts agent persistent facts into a single bitemporal table with eleven user-visible columns (fact identifier; subject, predicate, object; valid-time and system-time bounds; provenance annotation 𝑝 ∈ P; confidence conf; strategy identifier strat). A check-constrained row_kind ∈ {current, audit} discriminator partitions the table into user-visible rows and the audit rows emitted by every operator (Table 2). An audit row carries Audit = (𝑝 w ⊕ 𝑝 l, strat, 𝑡𝑠 ); default retrieval filters row_kind = current, and audit rows reach through a separate audit-log slice. The lift is conservative: every relational-algebra query over the 3
Ziming Wang
Table 3: Each anomaly maps to one verifier guard and one runtime enforcement. Upper block: classical Berenson–Adya iso-axis anomalies. Lower block: the three agent-memory predicates (N2 corollary of 𝐴5𝐵 on the (subj, pred) projection per Corollary 1). Predicate
Axis
Defence
𝑃 0 dirty write 𝑃 1 dirty read 𝑃 2 fuzzy read 𝑃 3 phantom 𝑃 4 lost update 𝐴5𝐴 read skew 𝐴5𝐵 write skew
iso iso iso iso iso iso iso
RC RC SI SR SI SI SR
N1 judge-replay inconsistency N2 belief-drift skew N3 audit erasure
judge partition schema
|=RC
Toki’s first guarantee is on the isolation axis: an operator at level 𝐿 excludes a classical anomaly 𝜙 exactly when 𝐿 dominates 𝜙’s guard, because a level forbids exactly the anomalies its guard rules out, with the keyed-log discipline carrying N1 and the partition pin carrying N2 into the same statement. The iff is sharp in both directions, so the guarantee is also a limit on every weaker level. The iso-axis grid of §4.5 verifies the predicted 0/1 boundary, each dominating cell admitting no schedule and each weaker cell admitting every schedule. Definition 2 (Iso-axis defence singletons). For each classical 𝜙 ∈ Φclass = {𝑃 0, 𝑃1, 𝑃2, 𝑃3, 𝑃4, 𝐴5𝐴, 𝐴5𝐵} [2, 7], the guard map guardiso : Φclass → Liso is RC 𝜙 ∈ {𝑃 0, 𝑃1 }, guardiso (𝜙) = SI 𝜙 ∈ {𝑃 2, 𝑃4, 𝐴5𝐴}, SR 𝜙 ∈ {𝑃 3, 𝐴5𝐵}. The chain-valued SR defence for 𝑃 3 is the uniform minimum; L-01 admits the per-table tightening to SRpolicy when ⊕c pins the policy table. Table 3 reports the same map.
SR logged judge partition SR audit row
(Lww)
⊕t ( 𝑓1 , 𝑓2 ) = ( 𝑓𝑖 ★ , Audit(𝑖𝑡★, 𝑖𝑡★ ) ) 𝑡
|=SI
K-vacuity warning. The guard map guardiso is carrier-vacuous (equivalently 𝐾-vacuous): it is defined over Liso alone and its soundness reduces to Berenson–Adya schedule predicates that mention no semiring carrier. The iff below is stated parametrically in 𝐾 for notational uniformity with Theorem 2, but Proposition 1 establishes the algebraic separation: the iso-axis preconditions remain carrier-vacuous on every commutative semiring with natural order, while the schema-axis ⪯𝐾 relation of Theorem 2 is 𝐾-load-bearing. A reviewer reading the iff in isolation may suspect the 𝐾 parameter is decorative; the separation Proposition makes the honest scoping visible.
(Evi)
⊕p ( 𝑓1 , 𝑓2 ) = ( 𝑓𝑖 ★ , Audit(𝑖𝑝★, 𝑖 𝑝★ ) ) 𝑝
|=RC+cb cb( 𝑓1 , 𝑓2 ) = 𝑖 ⊕? ( 𝑓1 , 𝑓2 ) = ( 𝑓𝑖 , Audit(𝑖, 𝑖 ) ) policy
|=SR
𝜌 ( 𝑓1 , 𝑓2 ) = 𝑖
⊕c ( 𝑓1 , 𝑓2 ) = ( 𝑓𝑖 , Audit(𝑖, 𝑖 ) )
(Await)
(Rule)
The discarded fact’s system-time end closes; the winner inherits a fresh system-time start, the merged provenance, and the strategy stamp. Each exposes pairs an isolation precondition with its failure mode (Table 1), and Appendix C carries the operator algorithms in full. Each operator resolves the running (𝑓1, 𝑓2 ) differently: ⊕t keeps amoxicillin as the latest write at read-committed; ⊕p compares the two confidence stamps at snapshot isolation; ⊕? blocks on a clinician callback; ⊕c applies a formulary policy row pinned to serializable. Each operator excludes exactly the anomalies its isolation pin dominates, the guarantee §3.3 makes precise.
3.3
Theorem 1 (Iso-lattice anomaly soundness for typed agent-memory operators). Let 𝐾 be a commutative semiring with the natural order ⪯𝐾 [30]: 𝑎 ⪯𝐾 𝑏 iff there exists 𝑑 ∈ 𝐾 with 𝑎 ⊕ 𝑑 = 𝑏. Let Φ ⊆ {𝑃 0, 𝑃1, 𝑃2, 𝑃3, 𝑃4, 𝐴5𝐴, 𝐴5𝐵} be a subset of the classical Berenson–Adya hierarchy [2, 7], and let 𝐿 be an isolation level drawn from the iso chain Liso = {RC ⪯ SI ⪯ SR} of §2.2. Under the dualrow schema of §3.1 and the typed operator algebra of §3.2 carrying provenance in 𝐾, define Prevents(𝐿, Φ) ≡ ∀𝑆. 𝑆 |= 𝐿 ⇒ ∀𝜙 ∈ Φ. 𝑆 |= ¬𝜙 .
Soundness: What Toki Guarantees
(1)
Then Prevents(𝐿, Φ) iff 𝐿 ⪰ guardiso (Φ), where guardiso extends from Definition 2 to subsets by lattice supremum: guardiso (Φ) = Ô 𝜙 ∈Φ guardiso (𝜙). The guard map is independent of the carrier; replacing 𝐾 with any of the three shipped carriers preserves the same isolation precondition.
Toki excludes three failure modes that isolation-spec reasoning alone cannot name: replay inconsistency (N1), when re-adjudicating a contradiction returns a different winner; belief-drift skew (N2), a write skew specialised to a (subj, pred) partition; and audit erasure (N3), loss of the overwritten fact. The classical alphabet misses these because it has no event for an LLM judge call, and one lemma closes that gap. The alphabet bridge (Lemma 1) reads each judge call as a read of a logged verdict that the operator commits before its own commit, which lifts the Berenson–Adya guards onto the agent write path. Under that reading, replay inconsistency becomes a textbook fuzzy read on the logged row, which snapshot isolation forbids, plus an insert phantom on the row’s first write, which serializability forbids. The remaining two failures attach to a schema decision and a provenance decision, so the guarantees split across three orthogonal axes, isolation, schema, and provenance (Table 3).
Proof sketch. The soundness direction proceeds by induction on schedule history over the seven-event alphabet of §2.1; the inductive step verifies that no operator emission of §3.2 introduces a forbidden 𝜙 ∈ Φ when its precondition |=𝐿 holds. The tightness direction is discharged by seven minimal witness schedules, one per classical predicate, that hold the immediate predecessor of guardiso (𝜙) on Liso . The K-vacuity warning above pairs with Proposition 1 to show the iso-axis guard remains carrier-vacuous across the three shipped carriers. The judge-callback alphabet bridge (Lemma below) shows the typed operator algebra over the seven-event alphabet Σ+ refines 4
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
to the classical five-event Σ exactly when each 𝑗𝑖 event maps to a logged read on a serializable judge table; under that refinement the iso-axis predicates N1 and N2 inherit the classical defence by reduction, and the soundness induction above closes the agentmemory specialisation. The full proof, the bridge lemma’s proof, and the tightness witnesses live in the theorem files.
remains non-deterministic. By Lemma 1 equation (2), 𝑆 |= N1 at (𝑅, 𝜃 ) iff 𝜋 𝐽 (𝑆) admits a fuzzy read 𝑃2 on a re-read or an insert phantom 𝑃 3 on the first materialization of judge_log[(𝑅, 𝜃 )]. Snapshot isolation already excludes the re-read 𝑃2 (guardiso (𝑃2 ) = SI); the first materialization is a phantom that SI admits and SR excludes (guardiso (𝑃3 ) = SR), equivalently a linearizable insert-if-absent on the key. Applying Theorem 1 to 𝜋 𝐽 (𝑆) with Φ = {𝑃2, 𝑃3 } at 𝐿 = SR on the keyed judge log excludes both patterns, so N1 is excluded on 𝑆. The operative requirement is linearizable keyed materialization, of which SR on the keyed judge log is the schedule-level realisation; this is why Table 3 reports a serializable read on the keyed log as the required level.
Lemma 1 (Judge-callback alphabet bridge). Let Σ = {𝑏𝑖 , 𝑟𝑖 (f), 𝑤𝑖 (f), 𝑐𝑖 , 𝑎𝑖 } be the classical schedule alphabet of §2.1 and let Σ+ = Σ∪{ 𝑗𝑖 (𝑅, 𝜃 ), cb𝑖 (𝑅, ℎ, 𝑘)} be the augmented alphabet. Define the map 𝜋 𝐽 : Σ∗+ → Σ∗ that fixes Σ pointwise, substitutes the first 𝑗𝑖 at each key (𝑅, 𝜃 ) by an insert-if-absent write and every subsequent 𝑗𝑖 at that key by a read, and substitutes each callback by a read: 𝑗𝑖first (𝑅, 𝜃 ) ↦→ 𝑤𝑖 judge_log[(𝑅, 𝜃 )] , repeat 𝑗𝑖 (𝑅, 𝜃 ) ↦→ 𝑟𝑖 judge_log[(𝑅, 𝜃 )] , cb𝑖 (𝑅, ℎ, 𝑘) ↦→ 𝑟𝑖 callback_log[(ℎ)] .
Call-site contract for Corollary 2. The defence is conditional on the operator reading the keyed judge-log row at (𝑅, 𝜃 ) before issuing the 𝑗𝑖 event: the alphabet bridge of Lemma 1 promotes 𝑗𝑖 to a logged read only when a prior operator call has committed the row. An operator that issues a fresh oracle call without consulting the log falls outside the lemma’s hypotheses (𝐻 1)+(𝐻 2), and the defence does not apply. The obligation is one of operator construction, not a schedule-level invariant: the typed operators ⊕? and ⊕c read the keyed log before they commit by construction (§3.4), so the soundness holds without any assumption about agent code that might bypass the operator surface. The schema axis is orthogonal to isolation, and Toki’s second guarantee lives there: the audit-row schema dominates every loser’s provenance under the K-semiring natural order, so N3 cannot occur, while the base schema admits a witness that erases it. The tightness direction carries the weight, since only the audit-row schema closes the gap. The schema-axis grid of §4.5 records N3 at 100% under the base schema and 0% under the audit-row schema.
Under the keyed-log discipline of §3.1, every judge call and callback commits its keyed-log row before the operator commits, an invariant §3.4 enforces in the dispatcher (full hypotheses 𝐻 1, 𝐻 2 in Appendix B.1). Then 𝜋 𝐽 preserves the operand-table conflict graph, so every classical predicate verdict transfers and 𝜋 𝐽 refines 𝑆 on the iso axis. Consequently N1 at key (𝑅, 𝜃 ) reduces to two classical patterns on the keyed row, 𝑆 |= N1 at (𝑅, 𝜃 ) ⇐⇒ 𝜋 𝐽 (𝑆) |= (𝑃 2 ∨ 𝑃 3 ) at judge_log[(𝑅, 𝜃 )], (2) a fuzzy read 𝑃2 excluded at SI and an insert phantom 𝑃 3 excluded at SR or a linearizable insert-if-absent. The full statement and proof are Appendix B.1. Corollary 1 (N2 defence on the partition data item). Treat the (subj, pred)-projected multiset 𝜋 (𝑠,𝑝 ) (M) as a single data item over which ⊕p is the read function and an agent’s belief-cache row 𝑓bc carries the invariant 𝐼 : 𝑓bc = ⊕p (𝜋 (𝑠,𝑝 ) ). A belief query 𝑇𝑞 that reads 𝜋 (𝑠,𝑝 ) and writes 𝑓bc , concurrent with a confidence revision 𝑇𝑤 that reads 𝜋 (𝑠,𝑝 ) and writes a row’s conf field, has intersecting readsets and disjoint write-sets; under SI both commit and 𝐼 is violated. This is the 𝐴5𝐵 write-skew shape of Adya [2] on the partition data item. SR on the (subj, pred) partition serializes 𝑇𝑤 outside 𝑇𝑞 ’s execution and restores 𝐼 ; Theorem 1 applied with Φ = {𝐴5𝐵} on the partition data item discharges the defence, with the data-item promotion from individual rows to the partition projection following the standard conflict-serializability framework of Bernstein-HadzilacosGoodman [8].
Theorem 2 (Audit-erasure schema lift). Let 𝐾 be a commutative semiring with the natural order ⪯𝐾 [30], and let Lschema = {base ⪯ audit-row} be the schema-augmentation lattice of §3.1. Under the audit-row refinement, every typed operator of §3.2 emits an audit tuple Audit = (𝑝 𝑤 ⊕ 𝑝𝑙 , strat, 𝑡𝑠 ) alongside the winner, where 𝑝 𝑤 , 𝑝𝑙 ∈ 𝐾 are the provenance polynomials of the winner and loser facts. For every schedule history 𝐻 executed against the audit-row schema and every loser fact 𝑓𝑙 with provenance 𝑝𝑙 consumed by an operator step in 𝐻 , there exists an audit tuple 𝑡 ∈ Rec𝐻 (𝑡 𝑣 , 𝑡𝑠 ) with 𝑝𝑙 ⪯𝐾 𝑡 .prov; conversely, against the base schema, schedule histories exist where no 𝑡 ∈ Rec𝐻 dominates 𝑝𝑙 , witnessing anomaly N3. Proof sketch. Soundness follows from 𝑝𝑙 ⪯𝐾 𝑝 𝑤 ⊕ 𝑝𝑙 under any commutative semiring with natural order [30] (existence witness 𝑑 = 𝑝 𝑤 ); the audit tuple’s 𝑡 .prov = 𝑝 𝑤 ⊕ 𝑝𝑙 dominates 𝑝𝑙 . Tightness sits in Appendix B.5.2: the witness 𝑆 𝑁 3 pins the lower bound on the schema lattice, parametric in the carrier. The provenance axis separates the two preceding guarantees: the isolation guard is carrier-vacuous and only the schema guard is K-load-bearing, so Toki’s K-parametric framing is load-bearing. The carrier-recoverability theorem refines the axis, making perinstance erasure recoverable from the carrier polynomial alone exactly when the carrier records multiplicity, which orders the three shipped carriers. The carrier ablation of §4.4 witnesses this, with verdicts invariant across carriers and token recall splitting them.
Remark 1 (Per-partition scope). The defence is stated per-partition; the operator pre-condition is that the calling code names the partition. Multiple concurrent partitions require independent SR pins, and cross-partition skew is outside the corollary statement and surfaces as follow-up work (§6). Corollary 2 (N1 defence by logged-judge reduction). Pin the judge parameter 𝜃 = (prompt, seed, model_version, temperature, tool_output_hash) and commit the vote into the keyed judge table under a linearizable insert-if-absent. The first call materializes the row keyed by (𝑅, 𝜃 ); every subsequent invocation reads the log and skips a fresh 𝐽 call. Determinism comes from the log’s keyed entries; the oracle 𝐽 itself 5
Ziming Wang
Proposition 1 (K-vacuity on the iso axis and K-load on the schema axis: an algebraic separation). Let 𝐾1, 𝐾2 be any two commutative semirings with natural order ⪯𝐾𝑖 [30], and let 𝐿 ∈ Liso be an isolation level in the Berenson–Adya hierarchy [2, 7]. Under the dual-row schema of §3.1, the K-parametric framing of §3.3 factors cleanly into the two axes: (1) (Iso-axis K-vacuity.) For every classical anomaly 𝜙 ∈ Φclass in Theorem 1, the iso-lattice prevention predicate Prevents(𝐿, {𝜙 }) is independent of the carrier choice: Prevents𝐾1 (𝐿, {𝜙 }) = Prevents𝐾2 (𝐿, {𝜙 }) for every 𝐾1, 𝐾2 . The guard map guardiso of Definition 2 is carrier-agnostic by construction: its codomain is Liso and its soundness proof reduces to the Berenson–Adya schedule-history predicates [2], which do not reference 𝐾 in any clause. (2) (Schema-axis K-load.) For the audit-erasure anomaly N3, the schema-lift defence of Theorem 2 is K-equivariant but not K-independent: the reachability claim 𝑝𝑙 ⪯𝐾 𝑡 .prov depends on the chosen ⪯𝐾 . Replacing the multilinear N[𝑋,𝑇 ] semiring with the Boolean reduct B preserves the reachability bit (every reachable provenance maps to 1 in B); the multidegree variant N[𝑋,𝑇 ] # preserves the reachability bit and additionally records token-count distinctions visible in the audit-row schema’s per-witness recall column. A hypothetical confidence-weighted 𝐾 [𝑋,𝑇 ] would add the confidenceaggregation channel that is currently a forward-compatibility hook per ADR-0017. Together, clauses (1) and (2) characterise the carrier 𝐾 as decorative scaffolding on the iso axis and load-bearing structure on the schema axis. The carrier ablation (§4.4) is the empirical witness for both clauses: verdict columns identical across the three shipped carriers (clause 1 witness); token-recall columns differ across carriers (clause 2 witness). The verdict-invariance is therefore not evidence that 𝐾 is decorative everywhere; it is evidence that the iso-axis guard map projects 𝐾 out by construction while the schema-axis reachability bit remains parametric.
companion scenarios, full-row erasure and reconstruction with the remaining log in hand, both reduce to re-evaluation and are recoverable on every carrier; the Block H ablation of §4.4 measures the per-instance regime exactly. Definition 4 (Carrier degree at a monomial). For 𝜋 ∈ 𝐾 in monomial normal form, deg𝑚𝑟 (𝜋) is the largest exponent of 𝑋𝑟 := prov(𝑟 ) in any monomial of 𝜋 that mentions it. The Boolean reduct B collapses every nonzero exponent to one and the multilinear carrier N[𝑋 ] forbids exponent two by construction, so both cap the degree at one; only the multidegree carrier N[𝑋 ] # preserves every positive exponent [30]. Theorem 3 (Carrier recoverability under per-instance erasure). Let 𝐴 contain 𝑘𝑟 ≥ 1 occurrences of 𝑟 and let 𝜋 = ans(𝑞, 𝐴). Then 𝑞 is per-instance counterfactually recoverable at 𝑟 (Definition 3) if and only if deg𝑚𝑟 (𝜋) ≥ 2. Recovery is the formal shift 𝜎𝑋𝑟 : 𝑋𝑟𝑖 ↦→ 𝑋𝑟𝑖 −1 that decrements one occurrence per power, welldefined from 𝜋 alone; the coefficient-injecting derivative 𝜕𝑋𝑟 returns the wrong answer and admits no semiring correction, so the shift is the recovery map. The condition orders the three shipped carriers Boolean ≡ multilinear ⊊ multidegree for multiplicity recovery, the transpose of the witness-token recall reported by the carrier ablation (§4.4). The iso-axis guard is carrier-vacuous (Proposition 1), so this theorem isolates the carrier’s load-bearing role to this surface. The full statement, the monomial-normal-form proof, and the per-carrier recovery grid are Appendix B.3. Composition is where the typing earns its keep, since peroperator soundness says nothing about a pipeline. Toki’s third guarantee lifts the per-operator contracts to a sequential composite at the lattice supremum of the per-step preconditions, so a chain of operators carries one declarable isolation contract and one schema mode (the supporting well-typedness lemma is Lemma 2). The composition grid of §4.5 confirms the lifted boundary across pipelines of length up to five. Theorem 4 (Composition soundness for typed-operator pipelines). Let ⟨⊕𝑎1 , ⊕𝑎2 , . . . , ⊕𝑎𝑛 ⟩ be a sequential composition of typed contradiction-resolution operators ⊕𝑎𝑖 ∈ {⊕t, ⊕p, ⊕?, ⊕c }, each carrying an iso precondition 𝐿𝑎𝑖 ∈ L = Liso × Lcb and a schemaaxis requirement 𝑀𝑎𝑖 ∈ Lschema = {base ⪯ audit-row}. Let Π := ⊕𝑎𝑛 ◦ · · · ◦ ⊕𝑎1 denote the sequential pipeline that emits, on contradicting input pair (f𝑤 , f𝑙 ) at version time 𝑡𝑠 , the chain ⟨(f𝑤(1) , Audit (1) ), . . . , (f𝑤(𝑛) , Audit (𝑛) )⟩ where each (f𝑤(𝑖 ) , Audit (𝑖 ) ) is the emission of ⊕𝑎𝑖 on the output of ⊕𝑎𝑖 −1 . Define the composite preconditions 𝑛 𝑛 Ü Ü 𝐿 ∗ := 𝐿𝑎𝑖 , 𝑀 ∗ := 𝑀𝑎𝑖 ,
Relationship to Brinke et al. Brinke et al. [12] show classical preservation theorems lift to K-relation semantics on every lattice semiring, a class containing the Boolean reduct B but not the natural-polynomial carriers N[𝑋 ], N[𝑋 ] # we adopt. Their partition refines clause (2): on the lattice subclass the schema-axis argument lifts to first-order entailment, while on the non-lattice subclass Theorem 3 supplies the lift through a direct polynomial-degree argument. Clause (1) is unaffected, the guard map never inspecting the carrier. Definition 3 (Per-instance counterfactual erasure under a carrier). Let 𝐾 be a commutative semiring with natural order [30] and let 𝐴 be an audit log in which a row 𝑟 may appear with multiplicity 𝑘𝑟 ≥ 1, so the K-relation evaluation records its 𝑘𝑟 -fold contribution to a witness as the indeterminate power 𝑋𝑟𝑘𝑟 . For a query 𝑞 with answer 𝜋 := ans(𝑞, 𝐴) ∈ 𝐾, the per-instance counterfactual answer at 𝑟 is ans (−1) (𝑞, 𝐴; 𝑟 ) := ans(𝑞, 𝐴𝑟(−1) ), where 𝐴𝑟(−1) removes one occurrence of 𝑟 (𝑘𝑟 ↦→ 𝑘𝑟 − 1). The query is per-instance counterfactually recoverable at 𝑟 when this answer is reconstructible from 𝜋 alone, with no access to 𝐴 \ {𝑟 } and no re-evaluation of 𝑞: the regime where the log survives only as its polynomial witness. The
𝑖=1 Ô 𝑖=1 where the iso join is component-wise on the iso and callback axes of L and the schema join is the maximum on Lschema . Then on every schedule 𝑆 that satisfies 𝐿 ∗ and runs the pipeline at schema mode 𝑀 ∗ on the dual-row schema of §3.1: (1) (Iso-axis composition.) For every classical anomaly 𝜙 ∈ Φclass and every LLM-specific anomaly 𝜙 ∈ {N1, N2} with 𝐿 ∗ ⪰ guardiso (𝜙), the pipeline Π does not witness 𝜙 on 𝑆: the peroperator soundness of Theorem 1 lifts to the composite.
6
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
(2) (Schema-axis composition.) For every loser fact 𝑓𝑙 consumed by any step, an audit tuple 𝑡 ∈ Rec𝐻 (𝑡 𝑣 , 𝑡𝑠 ) in the emission chain satisfies prov(𝑓𝑙 ) ⪯𝐾 𝑡 .prov, so the pipeline excludes N3 at schema mode 𝑀 ∗ : a single step requiring audit-row forces the composite to audit-row, lifting the necessity of Theorem 2. (3) (Allen-relation closure.) Allen-relation selection on any pipeline output preserves the bitemporal-tuple type by closure of Allen’s thirteen interval relations and the twelve-relation transitivity table that omits equality [3]. (4) (Table-scoped policy pins.) The table-scoped SRpolicy annotation carried by ⊕c stays outside the lattice L as a per-table side condition: when any ⊕𝑎𝑖 pins the named policy table to SR in the composite, the remaining tables stay at 𝐿 ∗ as defined above.
so the fold over 𝐶 is permutation-stable. Provenance-completeness É follows from 𝑝 𝑓 𝑗 ⪯𝐾 𝑘 𝑝 𝑓𝑘 under the natural order (existence witness the sum of the remaining monomials [30]), lifting the binary domination of Theorem 2 to the whole family. The confluence grid for 𝑛 ∈ {2, . . . , 8} sits in Appendix E.7. Remark 3 (Selection-fold wiring). The ⊕? and ⊕c operators resolve a conflict set by direct selection: an external callback or a policy row over the family elects one member. The judge-logged dispatcher wires this 𝑛-ary selection at the ingest seam. The oracle returns an index into the canonically ordered conflict set, the durable judge log records the elected member’s stable identity under an orderindependent set key, and a crash replay re-elects the same member by that identity. The two fold operators (⊕t , ⊕p ) and the two selection operators together cover the conflict-set algebra at every arity.
Corollary 3 (Pipeline contract surface). The four typed operators form a contract surface for production pipelines: any sequential composition is well-typed at the lattice supremum 𝐿 ∗ of its per-step iso preconditions and the lattice maximum 𝑀 ∗ of its per-step schema requirements. A deployment claiming the composite contract declares only those two scalars; Theorems 1 and 2 discharge the perstep exclusions and the composition theorem lifts them, reducing the cross-operator anomaly surface that ingest, dedupe, evidence-weight, and policy-check silently expose to a single declarable signature.
The keyed-log discipline is also necessary: any system whose operator surface does not enforce it admits N1 under bounded oracle nondeterminism, so Toki’s defence is a tight characterisation within the relational schedule model. This lower bound is the companion of the verdict matrix, where every baseline omitting the discipline admits N1; §4 confirms the bound empirically, with the measured admit rate landing on the 2𝑝 (1 − 𝑝) closed form across 30 calibrated cells (Figure 5). Witness schedules for every axis sit in Appendix B.5.
Remark 2 (Sequential scope). Theorem 4 covers sequential composition: the steps run in a fixed order on the contradicting pair under one wrapping transaction. The dispatcher contract (§3.2) admits a single pair to one operator gate per transaction, so concurrent composition on the same key does not arise, and concurrent composition on disjoint pairs reduces to Theorem 1 per transaction.
Definition 5 (Bounded oracle nondeterminism). An external judge oracle 𝐽 is boundedly nondeterministic when it factors as 𝐽 (𝑅, 𝜃, 𝜔) ∈ {0, 1} over an internal state space Ω with |Ω| ≥ 2, and some operator input (𝑅★, 𝜃 ★) admits two states 𝜔 1, 𝜔 2 ∈ Ω with 𝐽 (𝑅★, 𝜃 ★, 𝜔 1 ) ≠ 𝐽 (𝑅★, 𝜃 ★, 𝜔 2 ). This is the standard production model for an LLM judge: 𝜔 ranges over decoder seeds at non-zero temperature, sampling state, hardware numerical nondeterminism, or API rerolls. The degenerate |Ω| = 1 case the bound excludes by hypothesis.
The two argmax-fold operators also extend past the binary incumbent-versus-incoming form: a conflict set of 𝑛 pairwisecontradicting rows on one partition resolves under last-writerwins or evidence-weighted merge with the winner and the merged provenance independent of fold order, and the audit row dominating every loser under the K-semiring order. A confluence grid over 𝑛 ∈ {2, . . . , 8} confirms both properties (Appendix E.7).
Definition 6 (H1-compliant system). A contradiction-resolution system S over the alphabet Σ+ = Σ ∪ { 𝑗𝑖 (𝑅, 𝜃 ), cb𝑖 (𝑅, ℎ, 𝑘)} is H1-compliant when its operator surface enforces invariant H1 of Lemma 1: every 𝑗𝑖 (𝑅, 𝜃 ) is paired with a commit-preceding row at key (𝑅, 𝜃 ) in judge_log recording the witnessed vote, so every later invocation at the same key reads the log instead of issuing a fresh 𝐽 call. A system whose operator surface omits the hook, or which calls 𝐽 directly from free-form agent code, is H1-non-compliant.
Proposition 2 (N-ary conflict-set resolution). Let 𝐶 = {𝑓1, . . . , 𝑓𝑛 } with 𝑛 ≥ 2 be a conflict set of pairwise-contradicting facts over one (subj, pred) partition, and let ⊕𝑎 ∈ {⊕t, ⊕p } be a fold operator whose winner selector is an argmax over a total preference order (version time for ⊕t , the confidence-then-version-then-identity key for ⊕p ). Then ⊕𝑎 extends to an 𝑛-ary resolution ⊕𝑎 (𝐶) = (𝑓𝑖★ , Audit) with two guarantees: (1) (Confluence.) The winner 𝑓𝑖★ and the merged provenance É 𝑗 𝑝 𝑓 𝑗 in Audit are invariant under every permutation of 𝐶: resolving 𝐶 in any order returns the identical winner identity and the identical merged provenance. (2) (Provenance-completeness.) The audit tuple’s merged provenance dominates every member under the K-semiring natural order: 𝑝 𝑓 𝑗 ⪯𝐾 Audit.prov for every 𝑓 𝑗 ∈ 𝐶, including the winner.
Theorem 5 (N1 lower bound: keyed-log discipline is necessary). Let S be a contradiction-resolution system over the typedoperator alphabet Σ+ of §2.1, executed against a boundedly nondeterministic judge oracle 𝐽 (Definition 5). If S is H1-non-compliant (Definition 6), then there exists a schedule history 𝐻 executable by S such that 𝐻 |= N1 on some operator input (𝑅★, 𝜃 ★). Equivalently, on every operator input with at least two nondeterministic-state branches 𝜔 1, 𝜔 2 ∈ Ω realising distinct votes, S admits an adversarial replay pair witnessing N1 at (𝑅★, 𝜃 ★). Proof sketch. Definition 5 fixes 𝜔 1 ≠ 𝜔 2 and an operator input (𝑅★, 𝜃 ★) on which 𝐽 returns different votes. Two replays of 𝐻 = 𝐻 0 · 𝑗𝑖 (𝑅★, 𝜃 ★), one at each oracle state, share the committed-write prefix 𝐻 0 and the decoder parameter 𝜃 ★ but witness different votes; H1 non-compliance prevents the dispatcher from short-circuiting
Proof sketch. Confluence follows because an argmax over a total order is independent of enumeration order and the provenance sum ⊕ is commutative and associative under any commutative semiring, 7
Ziming Wang
Algorithm 1 Dual-row contradiction-resolution write path on partition (subj, pred). Operators are pure; this is the persistence policy that pairs each operator with loser invalidation and auditrow emission. The judge-log write of line 14 precedes the operator commit, discharging hypothesis H1 of Lemma 1.
on a keyed log row, so both replays are executable. The pair is an N1 witness. Appendix B.2 carries the full witness construction. Corollary 4 (Keyed-log discipline is a tight characterisation of N1 soundness). Pairing Corollary 2 (H1-compliant systems exclude N1) with Theorem 5 (H1-non-compliant systems admit it), within the relational schedule model where a system’s only lever over judge-vote stability is the isolation level on the keyed read,
Require: fact 𝑓 with strategy stamp strat(𝑓 ), write time 𝑡𝑠 , judge parameter pin 𝜃 ; oracle 𝜌 for ⊕? /⊕c Ensure: committed current row and, on contradiction, an audit row dominating the loser under ⪯𝐾 1: 𝑂 ← open current rows on (subj, pred) with Ts end open ⊲ row_kind = current 2: if ∃ 𝑟 ∈ 𝑂 with 𝑟 .obj = 𝑓 .obj and overlap(𝑟, 𝑓 ) then 3: return ⊲ duplicate confirmation; no new state 4: end if 5: 𝐶 ← { 𝑟 ∈ 𝑂 : 𝑟 # 𝑓 } ⊲ Allen overlap, differing object 6: if 𝐶 = ∅ then 7: insert 𝑓 as a fresh current row; return 8: else if |𝐶 | > 1 then 9: raise ⊲ binary operators require one incumbent 10: end if 11: 𝑟 ← the single incumbent in 𝐶 12: select operator ⊕ by strat(𝑓 ): ⊕t |RC, ⊕p |SI, ⊕? |RC+cb, ⊕c |SRpolicy 13: if ⊕ ∈ {⊕? , ⊕c } then 14: 𝑣 ← 𝜌 (𝑟, 𝑓 ); append 𝑣 to judge_log[(𝑅, 𝜃 )] ⊲ before the operator commit (H1) 15: end if 16: (𝑤, 𝑙) ← ⊕(𝑟, 𝑓 ) ⊲ winner / loser by the operator’s order 17: 𝑝 merge ← 𝑝 𝑤 ⊕ 𝑝𝑙 ⊲ exact K-semiring merge 18: if 𝑙 = 𝑟 then ⊲ incumbent lost 19: close 𝑟 at Ts end 𝑡𝑠 ; insert 𝑤 stamped with 𝑡𝑠 and 𝑝 merge 20: end if 21: insert audit row ( 𝑝 merge , strat(𝑓 ), 𝑡𝑠 , witness ) ⊲ row_kind = Audit; defends N3 22: commit at the operator’s isolation pin 23: return (𝑤, audit)
S excludes N1 ⇐⇒ S is H1-compliant at SR on judge_log. Tightness holds within this model: a unique-key insert-if-absent constraint, a linearizable key-value store, or a content-addressed judge cache each realises the keyed-read contract by other means and excludes N1; the lower bound binds any system omitting all three. Remark 4 (Scope). The lower bound binds systems running against a boundedly nondeterministic oracle; it constrains neither deterministic oracles (|Ω| = 1) nor systems that precompute verdicts offline, and other drift sources (model upgrades, prompt or retrieval drift) are bounded by the judge-prompt sensitivity Lemma rather than by the bound here. The bound compounds along a re-query trajectory: an H1-noncompliant baseline re-invokes the oracle on every re-query, so its replay-consistency rate decays toward zero over re-queries on the bounded-nondeterminism keys, while Toki reads the committed keyed-log verdict and stays at one, the trajectory §4 charts (Figure 6).
3.4
The Toki System
Toki runs the §3 algebra on an unmodified relational engine with no native bitemporal support, in roughly 2,700 lines of Python; the abstraction carries the contribution. Every inference rule lands as one of four executable pieces: an eleven-column user-visible schema sealed by one twelfth audit-row discriminator; four pure operator classes dispatched on a strategy stamp; a K-semiring polynomial serialized in line with exact dominance; and one SQL:2011 as-of predicate that serves both retrieval and audit replay. Toki recruits no storage feature beyond standard SQL. A check-constrained discriminator lifts the Theorem 2 dual-row signature into the relational layout; it is structural, written only by the audit-row emission path. The four operators are pure functions over fact pairs, and a single write path owns the I/O seam. Dispatch routes on the resolution-strategy column, and an unknown strategy raises a typed error with no silent fallback. Toki enforces each operator’s isolation pin one level above the operator: before the operator commits, the write path records the adjudicated vote in the keyed judge log, discharging the ordering hypothesis of Lemma 1 by construction. Algorithm 1 states the write path that ties these pieces together: the dispatcher detects a contradicting incumbent on the partition, routes to the typed operator, sequences the keyed judge log before the operator commit, and emits the dual-row pair whose audit half discharges Theorem 2. The single binary incumbent precondition is enforced by construction (a multi-incumbent partition raises rather than guessing), so the incremental write path stays binary, and the soundness of Theorem 1 carries to it verbatim.
The witness polynomial of §2.2 serializes as a text-encoded provenance column. Provenance merge realises 𝑝 𝑤 ⊕ 𝑝𝑙 over the multilinear instance N[𝑋,𝑇 ], and a dominance test decides 𝑝 old ⪯𝐾 𝑝 merge as an exact polynomial comparison. A multidegree multiset variant is also available, so re-verifying Theorem 1 at the strongest instantiation swaps the carrier without a proof rewrite. Retrieval hand-rolls the SQL:2011 as-of predicate the engine omits: a filter on the four timestamp columns plus the audit-row discriminator serves retrieval at the current value, audit replay at the audit value, and a third mode exposes both, closed-open under the §2.1 convention. Three details make the keyed-log discipline operational. The reference persists the keyed judge log as an append-only table, and a crash-replay test confirms a committed verdict replays consistently after a connection drop and reload, realising the keyed-log discipline the Theorem 5 lower bound requires. The audit row encodes its conflict witness as JSON, so arbitrary object strings round-trip through the single object column exactly. A repeated same-fact confirmation accumulates the duplicate’s provenance into the surviving 8
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 4: Verdict matrix over eight systems. For each anomaly, Claim is the verdict the system’s design implies and Wire the verdict observed from its running code. A = admit, X = exclude, − = not applicable.
row under the K-semiring sum, keeping the audit trail complete across re-ingestion.
4
EMPIRICAL VALIDATION
Five experiment clusters validate the algebra, and across all of them every agent-memory baseline admits at least one named anomaly while Toki excludes all three. A verdict matrix establishes the writetime correctness witness over eight systems (§4.1); three controlled clusters isolate each defence’s mechanism (§4.2), single-process cost (§4.3), and provenance carrier (§4.4); and a final set of grids anchors every soundness theorem to a measured 0/1 boundary (§4.5). A closing cross-system comparison bounds the scope: the contract makes no downstream-utility claim. Effect sizes report paired bootstrap confidence intervals at 1,000 resamples and a fixed seed; family-wise error rates use Holm stepdown at 𝛼 = 0.05. Cross-system equivalence reports Welch’s 𝑡statistic with Welch-Satterthwaite degrees of freedom; cost fits report Spearman 𝜌 and least-squares 𝑅 2 on log-transformed axes. Appendix E carries the full methodology.
4.1
N1 System
Claim
N2
N3
Claim
Wire
Claim
Wire
Agent-memory baselines (6 systems) mem0 v2-T − − mem0 v3-T A A mem0 v3-I A − Graphiti-T A A Graphiti-I A − Letta-T − − Letta-I − − Zep-T − − Zep-I − − MIRIX-T A A
− A A − − A A A A A
− A X − − A − A A A
A A A A A A A A A −
A A A A A A A A A −
Engine-layer comparator WorldDB-T X
X
X
X
X
X
Reference algebra Toki-I
X
X★
X
X★
X
X★
Wire
Each system gives two independent readings: T transcribes its published contradiction logic, I runs its shipped code; six cells abstain on structural grounds (Appendix D.4). ★ replay inconsistency via SR on the keyed judge log, belief-drift skew via SR on the (subj, pred) partition, audit erasure via the audit-row schema. MIRIX carries no in-repo wire adapter; its row transcribes the independent MMA-Bench evaluation [43], which probes replay inconsistency and belief-drift skew but not the audit path, so its audit-erasure cell abstains.
Every agent-memory baseline admits at least one anomaly
We evaluate eight systems: six agent-memory baselines (mem0 v2 [20], mem0 v3 [46], Graphiti [80], Letta [38], Zep [58], MIRIX [43]), one engine-layer comparator (WorldDB [25]), and the reference algebra Toki. Each system is probed on its own contradiction path against the three write-time anomalies; the verdict matrix (Table 4) reads each verdict twice, from the system’s design and from its running code. The per-system harness is detailed in the appendix. Every agent-memory baseline admits at least one anomaly. Audit erasure is universal among baselines with a documented provenance path: any system without a versioned audit row admits it, which covers five of the six baselines, while MIRIX abstains here because [43] measures its verdict accuracy rather than its audit path. Replay inconsistency appears on mem0 v3, Graphiti, and MIRIX, whose judge-dependent writes commit without a serializable log. Belief-drift skew appears on mem0 v3, Letta, Zep, and MIRIX at a partitioned snapshot isolation. No baseline closes all three. WorldDB excludes all three by keeping the judge off the write path: its content-addressed handlers run deterministically at query time and carry no isolation-level signature, so a deployment needing a write-path judge for evidence-weighted resolution gains no soundness guarantee. Toki is the only design that excludes all three while keeping the judge on the write path, pinning the decoder tuple, the output hash, and the partition under serializability. External evidence corroborates the gap: STALE [15], a 400-scenario expert-validated benchmark, scores the best frontier model at 55.2% on a workload whose implicit-conflict mode is a production replay inconsistency. One wire reading diverges from its design: mem0 v3 should admit belief-drift skew by construction, but its shipped reconciliation collapses competing-confidence rows under deterministic judging and excludes it (appendix).
4.2
The audit-row defence moves LoCoMo by +0.86
We measure how each defence moves its intended benchmark slice and how the same perturbation behaves on off-target controls, through paired slice estimands on LoCoMo [45], LongMemEvalS [76], and MultiTQ [17]. Each benchmark runs one single-defence ablation: audit-row against N3, judge-pin against N1, and partitionSR against N2. Figure 2 reports the 3×3 mechanism-stress grid, each cell measuring how strongly a defence moves its intended slice. The audit-row defence moves its primary LoCoMo slice by Δ = +0.86 (pairedbootstrap CI [0.76, 0.94]), the one cell below the ceiling on a naturalworkload slice; its two off-target controls, both partition-SR controls, and the partition-SR primary MultiTQ cell all saturate at +1.00 under their constructed slices, the success criterion for constructed controls. The judge-pin defence records no movement here, its replay-disagreement estimand requiring a judge replay table absent on this surface, so its evidence is structural (the §4.5 Bernoulli grid). Holm step-down at 𝛼 = 0.05 covers the nine-cell family, and the single natural-workload point stays below an end-to-end utility-superiority claim.
4.3
Latency stays sub-linear on the single-process envelope
Toki makes no scalability claim; we charge the single-process envelope only to bound that scope. Memory size across {0, 102, 103, 104, 105 } facts holds 𝑝 50 in 3.88 to 4.15 ms and 𝑝 99 under 18.20 ms (Figure 3, Spearman 𝜌 = 0.80), and writer concurrency fits 𝜇 ∼ 𝑐 0.86 at 𝑅 2 = 0.992, a sub-linear single-process lock-contention 9
Ziming Wang
Table 5: Every matched cell defends at 1.00; token recall separates provenance-retaining carriers from the Boolean reduct. Carrier-by-defence ablation, 𝑛 = 100 seeds per matched cell. Each cell is Match/Recall. Appendix A.4 reports off-target specificity and provenance-size statistics.
audit-row (N3) LoCoMo *
+0.86
LongMemEval-S
+1.00
MultiTQ
+1.00
[0.76, 0.94]
43 ↑ 0 ↓ ,
=
judge-pin (N1) LoCoMo
+0.00
LongMemEval-S *
+0.00
MultiTQ
+0.00
0↑ 0↓,
=
partition-SR (N2) LoCoMo
+1.00
LongMemEval-S
+1.00
MultiTQ *
+1.00
50 ↑ 0 ↓ ,
0
0.25
0.50
0.75
=
1.0
control Holm-reject
4.5
contradiction latency (ms)
5 0
100
1000
10000
100000
memory size (facts, log axis)
Figure 3: Contradiction-resolution latency stays flat as the store grows. 𝑝 50 (solid) and 𝑝 99 (dashed) latency for the evidence-weighted contradiction path on Toki, swept over memory size from 0 to 105 facts; 30 runs per point after 3 warmups. signature. A real multi-writer Postgres experiment demonstrates the operator-to-isolation mapping across the full lattice: read committed admits all four iso-axis anomalies, snapshot isolation excludes lost update and read skew, and only serializable also excludes write skew (𝐴5𝐵) and the phantom (𝑃3 ), aborting the losing writer at rate (𝑤−1)/𝑤 (Appendix E.6). Appendix E.2 carries the five-axis statistics and the transactional-backend disclosure in full.
4.4
N2 𝐴5𝐵 -on-partition
N[𝑋 ,𝑇 ] N[𝑋 ,𝑇 ] # B
1.00/1.00 1.00/1.00 1.00/0.00
1.00/1.00 1.00/1.00 1.00/0.00
1.00/1.00 1.00/1.00 1.00/0.00
Every theorem’s predicted 0/1 boundary matches measurement
Five structural grids land the direct empirical anchors for Section 3.3, each an exhaustive schedule census whose observed admit rate matches its typed 0/1 prediction exactly; the iso-lattice and composition grids appear in Figure 4, and Appendix E.4 (Table 23) carries every grid’s dimensions, boundary, and regeneration command. The iso-axis grid (Theorem 1), distinct from the verdict matrix, pairs nine predicates with six joint lattice levels on 54 cells: 32 dominating cells admit 0, 22 under cells 100%. The schema-axis grid (Theorem 2) flips N3 from 100% under the base schema to 0% under the audit-row schema, and the partition-pin grid (Corollary 1) holds 0 under partition-SR against RC/SI admits; the carrier sweep (Theorem 3) and composition grid (Theorem 4) hold the boundary across 𝑘 ∈ {2, . . . , 8} and across 1364 pipelines up to length five. The alphabet bridge (Lemma 1) preserves alphabet, edge, and refinement on 1,000/1,000 random Σ+ schedules. The lower bound (Theorem 5) lifts to its Bernoulli closed form, anchored by the cross-system equivalence panel (Figure 4c) and the calibration scatter of Figure 5. Six variants share one boundednondeterminism judge oracle (a frontier LLM at temperature 1.0 with a reasoning prefix): the H1-compliant reference admits 0/245 consecutive trial pairs across five seeds, the five non-compliant variants 0.167 to 0.204 mean. The per-call admit rate lands on the 2𝑝 (1 − 𝑝) closed form across 30 calibrated cells at mean absolute deviation 0.017 (maximum 0.111, 29 cells within the 0.10 envelope) and 𝑅 2 = 0.98 (Figure 5), so the lower bound rests on measured bounded-oracle data; Welch’s 𝑡 reaches |𝑡 | = 0.19 over four pairwise tests, rejecting no null at 𝛼 = 0.10, so the keyed-log discipline is the load-bearing axis. A temperature sweep over {0.5, 1.0, 1.5} holds the reference at 0.000 and the stripped variant at 0.32 to 0.34, consistent with the bounded-oracle hypothesis once the reasoning prefix saturates Ω (Definition 5). All four imported mimics lack the keyed-log discipline, lifting “admit rate > 0” from a structural observation to the quantitative theorem. The bound compounds along a re-query trajectory: a baseline that re-invokes the stochastic judge on every re-query loses replay consistency toward zero over re-queries on the boundednondeterminism keys, while Toki reads the committed keyed-log
95% mean CI p50 p99
10
N1 judge-pin
n.s.
Figure 2: Each defence moves its primary slice while the constructed controls saturate. Per cell, accuracy from defenceoff (◦) to defence-on (•); solid arrows are Holm-significant, ∗ marks the primary diagonal cell, and the right margin gives the paired-bootstrap effect size.
15
N3 audit-row
95% paired bootstrap CI; Appendix E.3). The iso-axis guards of Theorem 1 are carrier-agnostic by construction; only the schemaaxis natural order of Theorem 2 is K-load-bearing (Proposition 1), so verdicts factor through a carrier-projecting quotient and recall through the natural order the carrier parameterises.
accuracy (defence-off ∘ → defence-on ∙) defence-off defence-on (primary)
Carrier
Verdicts are carrier-invariant; recall is K-load-bearing
Verdicts are carrier-invariant across multilinear, multidegree, and Boolean reduct carriers (Table 5); token recall splits the carriers (the Boolean reduct collapses every witness to one bit; the multilinear and multidegree carriers are K-tight on token recall, 𝑛 = 100 seeds, 10
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
0%
0%
0%
0%
0%
P
0%
0%
0%
0%
0%
0%
P
100%
100%
0%
0%
0%
0%
P
100%
100%
100%
100%
0%
0%
(b) Composition pipeline (T-05)
100%
100%
0%
0%
0%
0%
100%
100%
0%
0%
0%
0%
A5B
100%
100%
100%
100%
0%
0%
N1
100%
100%
100%
100%
0%
0%
N2
100%
100%
100%
100%
0%
0%
RC
RC +cb
SI
SI +cb
SR
SR +cb
0.5
admit rate
P A5A
Pipeline length
1.0
0.0
=
75%
50%
51%
26%
27%
2%
=
94%
76%
76%
46%
46%
4%
=
99%
88%
88%
60%
60%
5%
=
100%
94%
94%
71%
71%
8%
=
100%
97%
97%
79%
79%
10%
RC
RC +cb
SI
SI +cb
SR
SR +cb
Isolation level
(c) Cross-system equivalence (T-06) 1.0
0.5
| |= .
Mem0
Graphiti
| |= .
Letta
| |= .
Zep
| |= .
0.0
0.0
,
| | = .
| | = .
,
reject null at = .
0%
mean admit
(a) Iso-lattice guard map (T-01) P
| | = .
,
,
| | = .
0.5
1.0
1.5
2.0
| | statistic vs Ours− reference
Isolation level
Figure 4: Three structural anchors; every predicted 0/1 boundary matches measurement. (a) Iso-lattice guard map (Theorem 1): nine predicates admit at 0% where the level dominates the guard, 100% elsewhere. (b) Composition admit rate over pipeline lengths one to five (Theorem 4), flooring only at the lattice supremum SR+cb. (c) Welch’s 𝑡 on four production-mimic variants, all |𝑡 | < 2, equivalence not rejected at 𝛼 = 0.05 (Theorem 5 distributional companion). H1 ¡ variants (5) H1-compliant ref.
1.0
Replay-consistency rate C(t)
Observed N1 admit rate
§0:10 band 2p(1 ¡ p) closed form
MAD = 0:017 max = 0:111 29/30 in band R 2 = 0:98
0.5 0.4 0.3
residual (obs ¡ theory)
0.2
0.1 0.0
0.1
−0.1
0.0
0.0
0.0
0.2
0.4
0.5
1.0
0.6
0.8
1.0
Oracle Bernoulli p (1-vote fraction)
committed verdict, never re-queried (Cor.)
0.8
T-06 p [p t +(1¡p) t ]
0.6
Mem0 v3 Graphiti TOKI (committed log)
0.4 0.2 0.0 5
15
20
Figure 6: Re-reading the committed verdict holds replay consistency; re-invoking the judge decays it. On the boundednondeterminism keys the lower bound (Theorem 5) governs, the two stochastic-judge baselines lose consistency over repeated re-queries and track the predicted curve 𝐶 (𝑡) = E𝑝 [𝑝 𝑡 + (1 − 𝑝)𝑡 ] (dotted), while Toki re-reads its committed verdict and holds at 1.0 (Corollary 2). Deterministic-oracle keys are consistent by definition and excluded; the axis measures write-time replay consistency only.
verdict and holds at 1.0 (Figure 6). Taken over the 𝑝 ∈ (0, 1) keys the theorem governs, the non-compliant rate crosses 0.5 by requery 𝑡 = 3 and reaches ≈ 0.06 by 𝑡 = 24, tracking the closed form 𝐶 (𝑡) = E𝑝 [𝑝 𝑡 + (1 − 𝑝)𝑡 ] inside the bootstrap band; the deterministic-oracle keys (𝑝 ∈ {0, 1}, 17 of 30 calibration cells) are replay-consistent by definition and are disclosed but excluded from this rate.
4.6
10
Re-query step t
Figure 5: The measured replay-inconsistency rate lands on the 2𝑝 (1 − 𝑝) closed form. Each point is one calibrated cell. The keyed-log reference (navy) pins at the zero-admit corners 𝑝 ∈ {0, 1}; the five stochastic-judge variants (vermillion), four baselines plus Toki’s log-stripped ablation, ride the predicted arc (Theorem 5) inside its prediction band, with the residual inset trend-free.
shared LoCoMo slice under a pinned synthesiser and judge, with three measured cells and nine structural abstentions. All three confidence intervals cover zero (mem0 v3: Δ = −0.04, CI [−0.10, +0.00]; Graphiti: −0.08, [−0.18, +0.00]; Zep: +0.02, [−0.06, +0.10]), at a preregistered power of 0.42 for 𝛿 = 0.05 on 𝑛 = 50, so the paper draws no utility-superiority claim from these rows. The row-level protocol and five-axis deltas sit in Appendix D.6; the claim-to-evidence map
Cross-system transparency ledger
The cross-system rows bound where the write-time correctness contract stops, probing downstream utility only as a transparency measure. The reference pairs against four agent-memory systems on a 11
Ziming Wang
(Appendix A) and artefact runbook (Appendix F) bind each claim to its evidence object, reproduce command, and scope.
4.7
in full [22]. None types the isolation precondition on the operator surface; WorldDB comes closest, carrying engine-layer Merkle provenance but leaving the isolation signature and the provenance algebra untyped over the agent write path.
Memory-layer ablation on the answerable pool
Classical concurrency and provenance hold every ingredient but the LLM-agent write path. Three foundational ingredients Toki composes come from the seven-anomaly schedule taxonomy of Berenson–Adya [2, 7] and the serializable-snapshot-isolation line of Fekete–Cahill [14, 23]; the bitemporal model of Snodgrass and the SQL:2011 period syntax [35, 37, 65]; and the K-relation provenance framework of Green–Karvounarakis–Tannen [30, 31], rooted in why/where provenance [13, 19] and its semiring and weightedsemiring extensions [4, 24, 26, 29, 50]. Widiaatmaja et al. [74] extend ProvSQL with bitemporal m-semiring provenance on inserts, updates, and deletes, the immediate precedent. VerIso [27] mechanises Berenson–Adya guarantees in Isabelle/HOL; Isolde [6] reasons over isolation specifications; S-Bus [36] fixes one Berenson– Adya point on the HTTP-observable projection. Toki types the (N1, N2, N3) triplet over the agent-memory (subj, pred) partition, bridges the LLM-judge boundary into the classical alphabet, and records the K-axis separation that isolates the carrier’s load-bearing role to the schema axis.
A paired ablation isolates the factual-recall capability the typed memory layer carries. We score Toki against its own memoryablated arm on the answerable-factual pool of LoCoMo, the categories whose gold a same-meaning judge can adjudicate: single-hop, temporal, and open-domain factual questions (𝑛 = 1,444). The pool excludes the open-domain speculative category, whose subjective gold a same-meaning judge cannot score, and the adversarial emptygold category, where abstention is correct and inverts the delta. With the memory layer the reference system answers 0.540 of the pool; ablated to no memory it answers 0.048, a paired Δ = +0.492 (paired-bootstrap 95% CI [+0.465, +0.519], McNemar 𝑝 < 10−4 , achieved power 0.748 against the pre-registered 0.80 at 𝛼 = 0.05). This power budget targets a 𝛿 = 0.05 minimum-detectable effect, roughly ten times smaller than the observed gain, so the McNemar test rejects equality with margin to spare. The gain concentrates on open-domain factual recall (+0.542, 𝑛 = 841) and holds across temporal multi-hop (+0.430, 𝑛 = 321) and single-hop (+0.411, 𝑛 = 282) questions. This ablation varies only the memory layer and makes no headto-head superiority claim, separating it from the cross-system ledger of §4.6. The answerable pool also explains the apparent distance from Table 18, whose mixed slice folds in the speculative and adversarial categories where both arms score near zero. Takeaway. On questions a judge can score, the typed memory layer supplies almost the whole of the reference system’s factual-recall accuracy: removing it collapses accuracy by an order of magnitude, from 0.540 to 0.048.
5
Retrieval-side benchmarks measure the symptom. LongMemEval [75, 76], LoCoMo [45], MultiTQ [17], and STALE [15] score retrieval and end-to-end accuracy over fixed stores; BeliefShift [51], Memora [70], and TSM [67] build benchmark-level anomaly taxonomies as observable-outcome tests. MemAudit [9], Ledger-QA on UMA [82], and MMA-Bench [43] stress audited, ledgered, and evidence-weighted updates, each anchoring one operator at the benchmark layer. They leave open a write-time correctness specification with named predicates and soundness theorems. Appendix H extends this positioning across the adjacent literatures.
RELATED WORK
Three threads converge on the contract this paper types, against a wider move to rebuild data systems around declared algebras [34] and AI agents [41]. Each stops short of the four-way combination of bitemporality, isolation signature, K-semiring provenance, and the LLM-agent write path.
6
LIMITATIONS AND CONCLUSION
Evaluation scope. The partition-SR MultiTQ slice carries controlledgrid rather than natural-workload evidence, and the three crosssystem LoCoMo cells cover zero at power 0.42, so both report transparency only, with no superiority claim. Concurrency. The multi-writer Postgres experiment that confirms the operator-toisolation mapping under real contention (§4.3, Appendix E.6) is single-node, so no distributed-deployment claim follows. Defence granularity. The N1 defence (Corollary 2) holds at intra-deployment replay granularity for a fixed decoder tuple, with cross-deployment divergence bounded by the judge-prompt sensitivity lemma; the lower bound (Theorem 5) covers only boundedly nondeterministic oracles, leaving deterministic oracles and engine-layer reconcilers outside the hypothesis. Toki types the four production contradiction-resolution strategies as bitemporal operators over a dual-row schema, closes the contract with four soundness theorems on three orthogonal axes, and makes keyed-log discipline a tight characterisation of N1 exclusion. Across eight systems, Toki alone excludes all three anomalies while keeping the language-model judge on the write path, closing the correctness contract production strategies ship without.
Agent-memory systems ship the four strategies without typing the contract. mem0 v2 [20] votes among add/update/delete/none labels and drops the loser; mem0 v3 [46] defers adjudication to retrieval; Graphiti [80] and Zep [58] invalidate older edges at retrieval time; Letta [38] organises memory in versioned blocks; the engine-layer comparator WorldDB [25] routes provenance through content-addressed Merkle ancestry. Retrieval-augmented memories such as HippoRAG [32] recall over a knowledge graph; MemOS [40] abstracts memory at the OS layer; substrate-dynamics cousins (FadeMem [73], H-Mem [79]) decay edge weights; Memanto [1] resolves conflicts over typed memory categories; and audit-trail cousins (MemLineage [52], HaluMem [16]) attach read-path evidence while the defended predicate stays implicit. Atomix [49] commits under a frontier-gated endpoint, and APEX-MEM [5] resolves conflicts at retrieval time over append-only storage, neither exposing the four-strategy surface, a space recent surveys map 12
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
A
CLAIM-TO-EVIDENCE MAP
This appendix is the entry point to the appendices. Each row binds one load-bearing claim of the main text to its reviewer-risk objection, evidence object, regeneration command, strongest licensed conclusion, and scope limit; the remaining appendices expand the corresponding rows. Reproduce tokens are either a make target or a pointer to the reproducibility runbook (Appendix F). Table 6: Claim-to-Evidence Map. Each load-bearing claim of the manuscript paired with the reviewer objection it must survive, its evidence object, the command that regenerates it, the strongest valid conclusion, and the scope limit. Claim
Main loc.
Reviewer risk
Evidence object
Reproduce
Strongest valid conclusion
Scope limit
C-ALG
§3.2
“Just a Berenson–Adya restatement”
Typing rules; Lemma 2 well-typed proof (A1)
make repro-compose
The four shipped operators only.
C-BRIDGE
Lemma 1
bridge_verification.csv, 1,000 trials (A1, A4)
App F (lemma-bridge)
C-ISO
“Biconditional too strong; drops the first-materialization write” Thm 1; Tbl 1 “N1 needs SR, not SI”
The four typed operators compose under the lattice join with one row per isolation precondition. 𝜋 𝐽 (𝑆 ) ⪯iso 𝑆 refines; N1 ⇐⇒ (𝑃 2 ∨ 𝑃 3 ) on the keyed row.
iso_matrix_grid.csv; iso-level summary.csv
App F (iso-matrix)
C-N3
Thm 2
“Schema-lift is a 𝐾 -semiring tautology”
schema_grid.csv
App F (schema-axis)
C-N2
Cor. 1
n2_grid.csv
App F (n2-partition)
C-T4
Thm 3
C-T6
Thm 5
“N2 is an independent discovery, not a specialisation” “deg ≥ 2 iff is imprecise; shift versus derivative” “The lower bound has narrow scope”
C-T5
Thm 4
C-G1
recovery_rate.csv; 𝑘 -semiring counterfactual.csv calibration.csv; N1 FINAL_SUMMARY.csv; N1 cross_system_test.csv (Welch |𝑡 | ); temperature_grid.csv composition_grid.csv, 1,364 “Composition is not closed under the lattice” pipelines
App F (t4)
Tbl 4; §4.1
“Eight systems vs. eleven adapters; baseline fairness; imported abstentions”
AnomalyClaim and AnomalyWire CSVs (shipped); manifest.json pinned SHAs (A3)
make reproanomaly-wire
C-G2
Fig. 2; §4.2
“Off-target controls also G2 summary.csv (9-cell grid) saturate at +1.00”
make repro-g2
C-G3
Fig. 8; §4.3
“Single-process measurement only”
G3 scaling.csv (5 axes)
C-G4
Tbl 5; §4.4
“Carrier choice is arbitrary”
C-G5
Fig. 4; §4.5
“The theorems are untested empirically”
C-CROSS
Tbl 18; §4.6
“No head-to-head superiority is shown”
operator-ablation results.csv; make repro-g4 𝑘 -semiring counterfactual.csv Five grids: iso-matrix, App F (g5 grids) schema-axis, n2-partition, t5-composition, oracle-variance cross_system/summary.csv (3 App F measured, 9 abstaining cells) (cross-system)
C-ABLATE
§4.7
“The typed memory layer carries factual recall”
powered_summary_ answerable.csv (𝑛 = 1,444, Δ = +0.49)
C-H1
§4.5; Thm 5
“The claim that baselines lack a keyed log is unverified”
h1_audit; deployment_scan CSVs (pinned commits, A3)
App F (oracle, n1)
App F (t5)
make repro-g3
13
App F (powered ablation)
Relational schedule model.
𝐿 excludes Φ iff 𝐿 dominates Within the guard(Φ) : SI excludes the Berenson–Adya re-read 𝑃 2 , SR the first-insert predicate set. 𝑃3 . The audit-row schema Parametric in the 𝐾 excludes N3 (0% vs 100% carrier. under the base schema). Partition-SR excludes N2 as a Constructed contention confidence-weighted A5B grid. specialisation. Per-instance erasure recovers Needs multiplicity ≥ 2; iff deg𝑚𝑟 (𝜋 ) ≥ 2 via the semiring without multiplicative inverses. formal shift 𝜎𝑋𝑟 . Admit rate matches the closed Boundedly form 2𝑝 (1 − 𝑝 ) (mean abs. nondeterministic oracle; dev. 0.017). deterministic oracles out of scope. Only SR+cb is the lattice supremum for every pipeline shape. Eight systems; every baseline keeping an LLM judge on the write path admits ≥ 1 predicate; the engine-layer comparator excludes all three by removing the judge, Toki alone while keeping it. Mechanism-stress evidence; only the audit-row LoCoMo cell carries natural-workload movement (+0.86). Mean ∼ 𝑐 0.86 at 𝑅 2 = 0.992: a local single-process lock-contention signature.
Pipeline length ≤ 5.
Six of fifteen imported cells abstain on structural grounds (A3).
Constructed slices saturate; no utility-superiority claim.
PostgreSQL saturates under SERIALIZABLE at concurrency ≥ 2; no distributed claim. Verdicts are carrier-invariant; Three carriers, 100 seeds. token recall is 𝐾 -load-bearing.
Each grid records the predicted 0/1 boundary exactly. All three confidence intervals cover zero; the paper makes no superiority claim. With-memory 0.540 vs ablated 0.048; McNemar 𝑝 < 10 −4 , achieved power 0.748.
Structurally controlled grids, not natural workloads. Under-powered (0.42) for 𝛿 = 0.05 at 𝑛 = 50.
Answerable categories (1,2,4) only; an in-system memory ablation (no cross-system superiority is claimed). App F (h1 audit) Four imported baselines are Audited at the pinned structurally H1-non-compliant commits only. (zero keyed-judge-log hits).
Ziming Wang
B
FORMAL WITNESSES AND PROOFS
This appendix gives the witness-level account behind the main-text results. Each load-bearing result is presented in a graded form with five parts: a minimal witness schedule that exhibits the phenomenon, the formal statement, the proof, the exact scope that changed relative to the main-text statement, and the empirical-anchor command that regenerates the supporting evidence. The graded results are Lemma 1 (the judge-callback bridge), the N1 lower bound of Theorem 5, the carrier recoverability of Theorem 3, and the composition statement of Theorem 4. The witness-schedule ledger that pins tightness of the two soundness theorems, the prompt-sensitivity separation, the write-path composition lemma, the 4 × 4 composition table, and the expanded guard surface follow as supporting material. Notation. 𝑟𝑖 [𝑥 𝑣 ] denotes transaction 𝑖 reads 𝑥’s version 𝑣; 𝑤𝑖 [𝑥 𝑣 ] denotes transaction 𝑖 writes 𝑥 producing version 𝑣; 𝑐𝑖 and 𝑎𝑖 denote commit and abort. Provenance annotations 𝑝 𝑣 are K-relation polynomials over the carrier 𝐾; the witnesses are parametric in 𝐾 and hold for any commutative semiring with natural order, including the multilinear N[𝑋,𝑇 ] default and the multiset N[𝑋,𝑇 ] alternative.
B.1
Graded result: the judge-callback bridge
The bridge homomorphism of Lemma 1 maps each judge call and each callback wait into a logged read on a keyed table, so that SR on that table serializes the read against the operator commit. The graded account below restates the bridge with its minimal witness, the empirical replay that exercises the key-multiplicity invariant, and the scope on which the bridge holds. B.1.1
Minimal witness schedule. The minimal bridge witness is the N1 replay schedule keyed by the read set and decoder tuple: 𝑗1 (𝑅, 𝜃 ) 𝑤 2 [judge_log(𝑅, 𝜃 )] 𝑐 2 𝑗1 (𝑅, 𝜃 ) 𝑐 1 .
Here 𝑗1 (𝑅, 𝜃 ) is the first judge call at the keyed row (𝑅, 𝜃 ), and the second 𝑗1 (𝑅, 𝜃 ) is its replay. Holding the row at a level weaker than SR admits the interleaved write 𝑤 2 , which lets the replay observe a different committed vote; SR on judge_log serializes the replay read against 𝑤 2 and forces a single vote per keyed row. B.1.2 Formal statement. Under hypotheses (𝐻 1) + (𝐻 2) of Lemma 1, the bridge homomorphism 𝜋 𝐽 maps the judge call 𝑗𝑖 (𝑅, 𝜃 ) to a read at the (𝑅, 𝜃 )-keyed row of judge_log, and the callback wait to a read at the keyed row of callback_log. The homomorphism preserves key multiplicity: distinct (𝑅, 𝜃 ) keys map to distinct logged rows, and a replay of (𝑅, 𝜃 ) maps to a re-read of the same row. The bridge therefore makes N1 a 𝑃2 -style fuzzy-read predicate on the keyed log, excluded at SR. B.1.3 Proof. The homomorphism is the keyed-log discipline of §3.1 applied to the Σ+ event alphabet. Each judge call carries the read set 𝑅 and the decoder tuple 𝜃 = (prompt, seed, model_version, temperature, tool_output_hash) of §2.1; the keyed row is addressed by (𝑅, 𝜃 ). A first call writes the row; a replay reads it. The fuzzy-read predicate on the keyed row is exactly N1: two reads of the same key returning different committed votes. Adya’s Mixing Theorem characterises SR on the keyed table as serializing the predicate read against any concurrent write, so the replay observes the committed vote of the first call and no other. The construction is parametric in 𝜃 : the homomorphism applies for every fixed 𝜃 , regardless of how the oracle 𝐽 votes across other decoder tuples. Key multiplicity is preserved because 𝜋 𝐽 is injective on keys. B.1.4 Scope and empirical anchor. The main-text statement asserts the bridge as an engine-layer guarantee at fixed 𝜃 ; the appendix adds the key-multiplicity preservation clause the main text uses implicitly. The cross-deployment behavior (two deployments pinning different 𝜃 ) is treated separately in Lemma 3 below. The empirical anchor is the lemma-bridge protocol of §E.4 (1000 trials at schedule length 12, all pass rates 1.00, every row key-multiplicity preserved; results/lemma_bridge/run_v1/bridge_verification.csv).
B.2
Graded result: the N1 lower bound
Theorem 5 states the workload-side lower bound on N1 admission for systems that do not key the judge log. The graded account pairs the lower bound with the oracle-variance witness that calibrates the predicted admission rate and the empirical admission rates observed across the baseline systems. B.2.1
Minimal witness schedule. The minimal N1 admission witness is the unkeyed replay 𝑗1 (𝑅) 𝑗2 (𝑅) 𝑐 1 𝑐 2,
where two judge calls on the same read set 𝑅 commit independently without a keyed log to serialize them. When the oracle 𝐽 assigns vote 1 with empirical probability 𝑝 on 𝑅, the two calls disagree with probability 2𝑝 (1 − 𝑝), and a system that admits the later vote without replay-keying admits the inconsistency at that rate. B.2.2 Formal statement. For a system without a keyed judge log, and a read set 𝑅 on which the oracle votes 1 with empirical probability 𝑝, the per-pair N1 admission probability equals 2𝑝 (1 − 𝑝). The bound is zero exactly when 𝑝 ∈ {0, 1} (the oracle is deterministic on 𝑅) and is maximised at 𝑝 = 21 . A system that keys the judge log and holds it at SR admits N1 at rate 0 on every 𝑅, independent of 𝑝. B.2.3 Proof. Two independent draws from a Bernoulli(𝑝) oracle disagree with probability Pr[draw1 ≠ draw2 ] = 𝑝 (1−𝑝)+(1−𝑝)𝑝 = 2𝑝 (1−𝑝). An unkeyed system commits the first draw, then on replay commits the second draw; the committed pair disagrees exactly when the draws disagree, so the admission probability is 2𝑝 (1 − 𝑝). A keyed system reads the committed row on replay rather than re-invoking the oracle, so the replay vote equals the first-call vote and the pair never disagrees; the admission rate is 0 by the bridge of Appendix B.1. 14
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
B.2.4 Scope and empirical anchor. The main-text theorem states the bound as a workload-and-oracle property; the appendix adds the calibration witness matching the predicted 2𝑝 (1 − 𝑝) against the observed admission rate per system and seed, and the engine-layer keyed-log defence that drives the keyed system to 0 on every read set. The calibration and admission ledgers are detailed in the oracle-variance protocol of §E.4 and the cross-system slice of §E.5: Toki in its dispatched configuration admits at mean rate 0.0 (all 245 candidate pairs served from the log, not the oracle; results/n1_empirical/run_v1/FINAL_SUMMARY.csv), while the unkeyed baselines (mem0, Graphiti, Letta, Zep, and the Toki stripped ablation) admit at mean rates between 0.167 and 0.204.
B.3
Graded result: carrier recoverability
Theorem 3 states that the audit-erasure recovery surface is non-trivial exactly when the K-relation carrier records enough structure to keep the erased provenance reachable. The graded account pairs the recoverability statement with the per-carrier witness and the counterfactual ablation. B.3.1
Minimal witness schedule. The minimal carrier witness is the audit-erasure schedule of Appendix B.5 restated at the carrier level: 𝑤 1 [𝑥𝑎 , 𝑝𝑎 ] 𝑐 1 𝑤 2 [𝑥𝑏 , 𝑝𝑏 ] 𝑐 2 𝑟 3 [𝑥] 𝑐 3 .
After 𝑇2 commits, the current-row surface contains only (𝑥𝑏 , 𝑝𝑏 ). The audit row carries Audit = (𝑝𝑎 ⊕ 𝑝𝑏 , strat, 𝑡𝑠 ). Recovery of 𝑝𝑎 requires 𝑝𝑎 ⪯𝐾 𝑝𝑎 ⊕ 𝑝𝑏 under the natural order ⪯𝐾 , which holds in a carrier rich enough to keep both monomials and fails in a carrier that collapses them. B.3.2 Formal statement. The erased provenance 𝑝𝑎 is recoverable from the audit row exactly when the carrier 𝐾 keeps 𝑝𝑎 ⪯𝐾 𝑝𝑎 ⊕ 𝑝𝑏 with 𝑝𝑎 identifiable as a summand of 𝑝𝑎 ⊕ 𝑝𝑏 . The multidegree multiset carrier N[𝑋,𝑇 ] keeps each summand identifiable and recovers 𝑝𝑎 on every instance; the multilinear N[𝑋,𝑇 ] default recovers 𝑝𝑎 only when the two monomials do not coincide after multilinear collapse; the Boolean security-semiring reduct collapses both monomials to a single truth value and recovers 𝑝𝑎 on no instance where 𝑝𝑎 ≠ 𝑝𝑏 as Boolean values. B.3.3 Proof. The natural order ⪯𝐾 on a commutative semiring with natural order satisfies 𝑝𝑎 ⪯𝐾 𝑝𝑎 ⊕ 𝑝𝑏 with existence witness 𝑑 = 𝑝𝑏 , so the inequality holds in every such carrier. Recovery additionally requires that 𝑝𝑎 be reconstructible from 𝑝𝑎 ⊕ 𝑝𝑏 . In the multidegree multiset carrier the sum keeps the exponent vector of each summand, so 𝑝𝑎 is read off by subtraction; recovery succeeds on every instance. In the multilinear carrier coincident monomials collapse coefficients, so 𝑝𝑎 is reconstructible only when the carrier preserved a distinguishing factor; recovery succeeds on a strict subset. In the Boolean reduct the sum is a disjunction that retains no multiplicity, so 𝑝𝑎 is not reconstructible whenever 𝑝𝑎 and 𝑝𝑏 map to the same truth value; recovery fails on those instances. B.3.4 Scope and empirical anchor. The main-text theorem states recoverability as a carrier property; the appendix adds the counterfactual ablation that isolates the carrier as the cause (schedule and operator algebra held fixed, only the carrier varied), confirming recoverability is a property of the carrier choice rather than the schema or isolation level. The per-instance and counterfactual ledgers are detailed in the G4 carrier-ablation protocol of §E.3 (Table 22): the multidegree carrier recovers all 375 instances at accuracy 1.0, the multilinear carrier recovers 106 of 375 at accuracy 0.683, and the Boolean carrier recovers none at accuracy 0.345 (results/g4_ablation/k_semiring/ counterfactual.csv; the 200-instance t4_per_instance run shows the same 1.0/0.0 ordering).
B.4
Graded result: the composition theorem
Lemma 2 (Composition well-typedness on the monotone fragment). Let ⊕𝑎 ∈ {⊕t, ⊕p, ⊕?, ⊕c } denote a contradiction-resolution operator with precondition 𝐿𝑎 ∈ L = Liso × Lcb (§2.2). For any sequential composition ⊕𝑎𝑛 ◦ · · · ◦ ⊕𝑎1 over the dual-row schema of §3.1, the Ô Ô composed operator is well-typed under any schedule that satisfies 𝐿 ∗ = {𝐿𝑎1 , . . . , 𝐿𝑎𝑛 }, where is the lattice join in L (component-wise on the iso and callback axes). The per-table SRpolicy annotation carried by ⊕c stays outside L: it pins the named policy table to SR in the composite and leaves 𝐿 ∗ on the remaining tables. Allen-relation selection on the operator output preserves the bitemporal-tuple type by closure of Allen’s thirteen interval relations and the twelve-relation transitivity table that omits equality [3]. On the orthogonal schema axis Lschema = {base ⪯ audit-row}, the composite holds the maximum of per-step schema requirements; when any step in the chain falls under Theorem 2, the composite pins to audit-row. Compositions involving ⊕c on the policy table compose through table-disjoint preconditions; the Appendix B.8 table-decomposition argument covers that case. Proof sketch. Lattice order on Liso coincides with schedule satisfaction, so the lattice join 𝐿 ∗ is the exact precondition of the composite; component-wise join preserves the orthogonal callback axis. The table-scoped SRpolicy adds a per-table predicate that composes through tabledisjoint preconditions. Closure under Allen-relation selection follows from the transitivity table over the twelve non-equality relations [3]. Appendix B.8 enumerates the four-by-four pairwise composition table. Theorem 4 and the composition lemma Lemma 2 state that the sequential composition of two typed operators holds the lattice join of their isolation preconditions. The graded account pairs the join statement with the operator-precondition witnesses, the 4 × 4 composition table, and the integration suite that exercises every cell. B.4.1 Minimal witness schedule. The minimal composition witness is the off-diagonal pair ⊕p ◦ ⊕t , whose component preconditions are 𝐿 ⊕t = RC and 𝐿 ⊕p = SI. A schedule that holds only RC admits a split-snapshot evidence read at the ⊕p step, which the join RC ∨ SI = SI excludes. The composite therefore requires SI, the join of the two component levels. 15
Ziming Wang
B.4.2 Formal statement. For typed operators ⊕𝑎 and ⊕𝑏 with isolation preconditions 𝐿𝑎 and 𝐿𝑏 in L = Liso × Lcb , the sequential composition ⊕𝑏 ◦ ⊕𝑎 holds the join 𝐿𝑎 ∨ 𝐿𝑏 . The join is component-wise: RC ∨ SI = SI on the iso axis, ⊥ ∨ cb = cb on the callback axis, and the policy annotation composes by requiring SR only on the named policy table. B.4.3 Proof. A schedule holding the composite must satisfy both component preconditions, so it holds every level at or above 𝐿𝑎 and every level at or above 𝐿𝑏 , hence every level at or above 𝐿𝑎 ∨ 𝐿𝑏 . Conversely a schedule holding 𝐿𝑎 ∨ 𝐿𝑏 holds each component precondition by downward closure of |= on the lattice, so both operator steps type-check. The callback component composes by requiring the delivered callback_log row whose read is ordered between the candidate read and the operator write; the policy annotation pins only the named policy table. The join is therefore both necessary and sufficient. B.4.4 Scope and empirical anchor. The main-text theorem states the join for the two-operator case. The appendix records the minimal weakening history behind each of the four operator preconditions (Table 9) and enumerates all 16 ordered pairs (Table 10) in §B.8 below, where the integration suite that exercises every cell is detailed. The composition is on the iso and callback axes; the configuration-axis dependence of the emitted wire verdict is governed separately by Lemma 4 below.
B.5
Witness schedules for the two soundness theorems
This subsection exhibits the eight witness schedules behind the two soundness theorems of the ADR-0008 D-T01 split: seven iso-axis witnesses for the anomaly-soundness theorem over the seven Berenson–Adya classical anomalies, and one schema-axis witness for the audit-erasure theorem. Each schedule holds the immediate predecessor of the defending level on its lattice (Liso for the seven, Lschema for the eighth). Together with the soundness inductions in the main text, the eight witnesses establish the if-and-only-if of both theorems. B.5.1 Iso-axis witnesses for anomaly soundness. The seven witnesses below pin tightness of the anomaly-soundness theorem on the iso lattice Liso . Each schedule holds the immediate predecessor of guardiso (𝜙) and witnesses 𝜙. Schema scope of the seven witnesses. The schedules below are stated on the current-row projection of the dual-row schema (§3.1): every 𝑤𝑖 [𝑥 𝑣 ] and 𝑟𝑖 [𝑥 𝑣 ] targets a fact tuple in the default row_kind = current scope. Each operator step of §3.2 also emits an audit tuple at row_kind = audit on the audit_log(𝑡𝑠 ) slice. The default filter 𝜎row_kind=current , whose exhaustiveness is guaranteed by the CHECK constraint of §3.1, projects every audit-row write away; audit emissions therefore contribute no edges to the dependency graph of the witness schedule’s Qbase reads and writes. Proposition 5’s commutation argument applied to selection lifts each witness’s verdict at its named isolation level from the base schema to the full dual-row schema unchanged. 𝑃 0 dirty write. Schedule: 𝑤 1 [𝑥𝑎 ] 𝑤 2 [𝑥𝑏 ] 𝑐 2 𝑐 1 . Holds the level immediately weaker than RC (no isolation guarantee). ⊕t at this level admits the schedule, but the schedule violates 𝑃0 : 𝑇2 wrote between 𝑇1 ’s write and commit. Defence: RC blocks 𝑤 2 [𝑥] until 𝑐 1 , ruling out the schedule. 𝑃 1 dirty read. Schedule: 𝑤 1 [𝑥𝑎 ] 𝑟 2 [𝑥𝑎 ] 𝑎 1 𝑐 2 . Holds the level immediately weaker than RC. 𝑇2 reads 𝑇1 ’s uncommitted write, then 𝑇1 aborts: 𝑇2 has read a value that never officially existed. Defence: RC blocks 𝑟 2 [𝑥𝑎 ] until 𝑇1 commits or aborts. 𝑃 2 fuzzy read. Schedule: 𝑟 1 [𝑥𝑎 ] 𝑤 2 [𝑥𝑏 ] 𝑐 2 𝑟 1 [𝑥𝑏 ] 𝑐 1 . Holds RC (the immediate predecessor of SI). 𝑇1 reads 𝑥 twice and sees two different values because 𝑇2 committed in between. Defence: SI pins 𝑇1 ’s reads to a single snapshot. 𝑃 3 phantom (policy table). Schedule: 𝑟 1 [policy: WHERE active] 𝑤 2 [insert new active row] 𝑐 2 𝑟 1 [policy: WHERE active] 𝑐 1 . Holds SI (the immediate predecessor of SRpolicy ). 𝑇1 ’s two predicate reads see different row sets because 𝑇2 inserted a row matching the predicate. Defence: SR on the policy table serializes the predicate-read with 𝑇2 ’s insert. 𝑃 4 lost update. Schedule: 𝑟 1 [𝑥 0 ] 𝑤 2 [𝑥 1 ] 𝑤 1 [𝑥 2 ] 𝑐 2 𝑐 1 . Holds RC (the immediate predecessor of SI). 𝑇1 reads 𝑥 at version 0, 𝑇2 writes version 1, 𝑇1 overwrites with version 2 (computed from 𝑥 0 ): 𝑇2 ’s update is silently lost. Defence: SI detects the read-write conflict and aborts 𝑇1 on its commit. 𝐴5𝐴 read skew. Schedule: 𝑟 1 [𝑥𝑎 ] 𝑟 1 [𝑦𝑎 ] 𝑤 2 [𝑥𝑏 ] 𝑤 2 [𝑦𝑏 ] 𝑐 2 𝑟 1 [post-2] 𝑐 1 . Holds RC (immediate predecessor of SI). 𝑇1 sees 𝑥 at one snapshot version and 𝑦 at another, breaking constraints that bind 𝑥 and 𝑦. Defence: SI pins all of 𝑇1 ’s reads to one snapshot. 𝐴5𝐵 write skew. Schedule: 𝑟 1 [𝑥𝑎 ] 𝑟 2 [𝑦𝑎 ] 𝑤 1 [𝑦𝑏 ] 𝑤 2 [𝑥𝑏 ] 𝑐 1 𝑐 2 . Holds SI (immediate predecessor of SR). Each transaction reads the other’s pre-write state and writes a value the other did not see; the joint post-state violates a cross-row constraint. Defence: SR orders the writes to detect the cycle. B.5.2 Schema-axis witness for audit erasure. The single witness below pins tightness of the audit-erasure theorem on the schema lattice Lschema . The schedule holds the base schema (the immediate predecessor of audit-row) and witnesses N3.
16
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
N3 audit erasure (parametric K).. Schedule: 𝑤 1 [𝑥𝑎 , 𝑝𝑎 ] 𝑐 1 𝑤 2 [𝑥𝑏 , 𝑝𝑏 ] 𝑐 2 𝑟 3 [𝑥] 𝑐 3 , executed against a base schema (no audit-row column). Holds (RC, base), the immediate predecessor of (RC, audit-row). After 𝑇2 ’s commit, the recovery surface contains only (𝑥𝑏 , 𝑝𝑏 ). Therefore 𝑝𝑎 is unreachable under the K-relation natural order ⪯𝐾 , since 𝑝𝑎 ⪯̸𝐾 𝑝𝑏 . Defence: the (RC, audit-row) refinement has every operator emit Audit = (𝑝𝑎 ⊕ 𝑝𝑏 , strat, 𝑡𝑠 ) alongside the winner; because 𝐾 is commutative and ⪯𝐾 is the natural order, 𝑝𝑎 ⊕ 𝑝𝑏 ⪰𝐾 𝑝𝑎 holds parametrically in 𝐾 (the existence witness is 𝑑 = 𝑝𝑏 ). The construction works for any commutative semiring with natural order; for the multilinear N[X,T] default the witness is one-monomial coefficient dominance; for the multiset N[X,T] instance the witness is exponent-wise dominance; for the Boolean security-semiring of Foster-Green-Tannen 2008 the witness is the disjunction lattice. Proposition 3 (Tightness of the iso-axis anomaly soundness, parametric in 𝐾). For each classical anomaly 𝜙 {𝑃0, 𝑃1, 𝑃2, 𝑃3, 𝑃4, 𝐴5𝐴, 𝐴5𝐵} let 𝑆𝜙 denote the schedule exhibited in the named
∈
o. f §B.5.1. Let 𝐿𝜙′ denote the immediate predecessor of guardiso (𝜙) on Liso , namely the level below RC when 𝜙 ∈ {𝑃0, 𝑃1 }, 𝐿𝜙′ = RC when 𝜙 ∈ {𝑃 2, 𝑃4, 𝐴5𝐴}, and 𝐿𝜙′ = SI when 𝜙 ∈ {𝑃 3, 𝐴5𝐵}. Then (a) 𝑆𝜙 |= 𝐿𝜙′ and (b) 𝑆𝜙 |= 𝜙 for each of the seven 𝜙. The construction is parametric in the K-relation carrier: the witness alphabet {𝑟𝑖 [𝑥 𝑣 ], 𝑤𝑖 [𝑥 𝑣 ], 𝑐𝑖 , 𝑎𝑖 } omits the provenance annotation, so replacing the carrier 𝐾 with any commutative semiring with natural order (multilinear N[𝑋,𝑇 ], multi-degree N[𝑋,𝑇 ] # , Boolean security-semiring reduct) leaves the seven verdicts unchanged. Proof. Verification of (a)+(b) is exhibited paragraph by paragraph in §B.5.1: each of the seven s. tatements (𝑃0 dirty write through 𝐴5𝐵 write skew) displays 𝑆𝜙 explicitly, verifies 𝑆𝜙 |= 𝐿𝜙′ at the named level by the read/write/commit ordering, and verifies 𝑆𝜙 |= 𝜙 by inspection of the conflict graph against the predicate definition. The seven verifications are sufficient because Adya’s Mixing Theorem [2, Theorem 4.6] characterises each 𝐿 ∈ Liso as a constraint on the rw/wr/ww conflict graph over Σ events, and the seven predicates of Berenson et al. [7] are similarly constraints on the same graph. Parametricity in 𝐾 follows from the alphabet-omission argument: the iso-axis verdict of each 𝑆𝜙 depends only on the order of 𝑟𝑖 /𝑤𝑖 /𝑐𝑖 /𝑎𝑖 events; the provenance polynomial 𝑝 𝑣 ∈ 𝐾 [𝑋,𝑇 ] that the operator algebra of §3.2 carries in the audit row is emitted at the row_kind = audit slice, which the default filter 𝜎row_kind=current of Proposition 5 projects away from Qbase reads. The seven schedules therefore admit the same verdict under every commutative semiring carrier with natural order. □ Tightness summary. The seven iso-axis schedules of Proposition 3 combined with the iso soundness induction in the main text (proof of Theorem 1, (⇐) direction) establish the if-and-only-if of the iso-axis anomaly-soundness theorem: assuming 𝐿 ⪰̸ guardiso (Φ) selects some 𝜙 ∗ ∈ Φ with 𝐿 ⪯ 𝐿𝜙′ ∗ , and the downward closure of |= on the iso lattice yields 𝑆𝜙 ∗ |= 𝐿, which witnesses 𝜙 ∗ and falsifies Prevents(𝐿, Φ) of Equation (1). The schema-axis schedule (a) holds base on Lschema and (b) admits N3; combined with the schema-axis soundness induction in Theorem 2, this establishes the audit-erasure theorem. B.5.3 Induction case ledger for the seven classical anomalies. The main-text proof of Theorem 1 exhibits the induction step in detail for the representative case 𝜙 = 𝐴5𝐵. The remaining six cases follow the same template: the appended operation op obeys its typing precondition at guardiso (𝜙), the iso lattice meet ensures 𝐿 ⪰ 𝐿op , and Adya’s Mixing Theorem [2, Mixing Theorem] preserves the predicate verdict over the prefix-extension 𝑆 · op. Table 7 records one row per case: the guard level, the conflict-graph invariant the typing precondition preserves under op, and the witness that pins tightness (at the level below the guard, the symmetric counterpart of the soundness step). The 𝐴5𝐵 case is recorded inline in the main-text proof, where the partition-projected serializability argument applies the Mixing Theorem on 𝜋 (𝑠,𝑝 ) (𝑆 ′ ) and excludes the disjoint-write / intersecting-read pattern. Table 7: Induction cases for the seven classical anomalies. Each row names the guard level guardiso (𝜙), the invariant the typing precondition preserves when op is appended at 𝐿 ⪰ guardiso (𝜙), and the tightness witness at the level immediately below the guard. Anomaly
Guard
Invariant preserved under op
Tightness witness (level below guard)
𝑃0 dirty write
RC
no overlapping uncommitted writes per operand; an interleaved 𝑤 𝑗 inside 𝑇𝑖 ’s write interval is aborted before commit every committed read paired with a committed write on the same version; 𝑟 𝑗 [𝑥𝑎 ] while 𝑇𝑖 uncommitted is excluded snapshot-pin: op commits at 𝑇𝑖 ’s snapshot timestamp or starts a fresh snapshot; no two distinct versions of 𝑥 to 𝑇𝑖 serializable predicate-read on the pinned table; an interleaved predicate-matching insert between two predicate reads is blocked first-committer-wins: commit-time check aborts both-overwrite-after-same-predecessor cross-row snapshot: 𝑟𝑖 [𝑥 ] and 𝑟𝑖 [𝑦 ] resolve at one timestamp; no split across a concurrent commit partition-projected serializability on 𝜋 (𝑠,𝑝 ) (𝑆 ′ ) excludes disjoint-write / intersecting-read (main-text representative case)
𝑤1 [𝑥𝑎 ] 𝑤2 [𝑥𝑏 ] 𝑐 2 𝑐 1
𝑃 1 dirty read
RC
𝑃 2 fuzzy read
SI
𝑃3 phantom (policy)
SR
𝑃4 lost update
SI
𝐴5𝐴 read skew
SI
𝐴5𝐵 write skew
SR
17
𝑤1 [𝑥𝑎 ] 𝑟 2 [𝑥𝑎 ] 𝑎 1 𝑐 2 𝑟 1 [𝑥𝑎 ] 𝑤2 [𝑥𝑏 ] 𝑐 2 𝑟 1 [𝑥𝑏 ] 𝑐 1 at RC 𝑟 1 [ WHERE active ] 𝑤2 [ insert ] 𝑐 2 𝑟 1 [ same pred. ] 𝑐 1 at SI 𝑟 1 [𝑥 0 ] 𝑤2 [𝑥 1 ] 𝑤1 [𝑥 2 ] 𝑐 2 𝑐 1 at RC 𝑟 1 [𝑥𝑎 ] 𝑟 1 [𝑦𝑎 ] 𝑤2 [𝑥𝑏 ] 𝑤2 [𝑦𝑏 ] 𝑐 2 𝑟 1 [ post-2 ] 𝑐 1 at RC 𝑟 1 [𝑥𝑎 ] 𝑟 2 [𝑦𝑎 ] 𝑤1 [𝑦𝑏 ] 𝑤2 [𝑥𝑏 ] 𝑐 1 𝑐 2 at SI
Ziming Wang
B.6
Judge prompt-sensitivity separation
The lemma below surfaces the engine-versus-deployment separation that Corollary 2 implicitly bracketed: the engine defends replay anomalies within a single pinned 𝜃 ; the selection of 𝜃 from a deployment-plausible family is a deployment-time concern outside the operator algebra. The definitions, lemma, and proposition below carry the prompt-sensitivity image and its achievable bound. Definition 7 (Deployment-plausible judge-prompt family). Let Θ = prompt × seed × model_version × temperature × tool_output_hash be the judge decoder-parameter space of §2.1. A deployment-plausible judge-prompt family for an evaluator intent 𝜄 (such as “compare candidate answer against gold and output binary correctness”) is a set Θ𝜄 ⊆ Θ such that every 𝜃 ∈ Θ𝜄 encodes a prompt that a deployer faithful to 𝜄 might reasonably ship. The four non-prompt components of 𝜃 (seed, model version, temperature, tool-output hash) are pinned across Θ𝜄 ; the family varies only the prompt sub-component. Definition 8 (Judge prompt-sensitivity image). For an oracle 𝐽 , an evaluator intent 𝜄 with deployment-plausible prompt family Θ𝜄 (Definition 7), and a read-set 𝑅, the prompt-sensitivity image is 𝐵 Θ𝜄 (𝐽, 𝑅) := 𝐽 (𝑅, 𝜃 ) : 𝜃 ∈ Θ𝜄 ⊆ {0, 1}. 𝑅 is prompt-stable under (𝐽, Θ𝜄 ) iff |𝐵 Θ𝜄 (𝐽, 𝑅)| = 1; otherwise 𝑅 lies in the semantic boundary of (𝐽, Θ𝜄 ). The empirical boundary measure on a benchmark slice Q is |{ 𝑅 ∈ Q : |𝐵 Θ𝜄 (𝐽, 𝑅)| > 1 }| 𝜇Θ𝜄 (𝐽, Q) := . |Q| Lemma 3 (Engine N1 defence and prompt-sensitivity separation). Under hypotheses (𝐻 1) + (𝐻 2) of Lemma 1 and the keyed-log discipline of §3.1: (1) For every fixed 𝜃 ∈ Θ, SR on judge_log excludes N1 at (𝑅, 𝜃 ) on every schedule 𝑆 over Σ+ . The exclusion is a property of the engine layer and does not depend on the size of 𝐵 Θ𝜄 (𝐽, 𝑅). (2) For 𝑅 ∈ Q with |𝐵 Θ𝜄 (𝐽, 𝑅)| > 1, two deployments differing only by the choice of 𝜃 1, 𝜃 2 ∈ Θ𝜄 commit different votes 𝑣 1 ≠ 𝑣 2 at (𝑅, ·). Each deployment internally excludes N1 by clause (1); the cross-deployment divergence is a deployment-time decision outside the iso lattice. The two clauses together establish that the engine layer bounds N1 at intra-deployment replay granularity; cross-deployment prompt selection is bounded only when 𝜇Θ𝜄 (𝐽, Q) = 0, a workload-and-judge property rather than an engine property. Proof outline. Clause (1) is Corollary 2 restated. The homomorphism 𝜋 𝐽 of Lemma 1 maps 𝑗𝑖 (𝑅, 𝜃 ) to a logged read at the (𝑅, 𝜃 )-keyed row of judge_log, and SR on that table serializes the read against the operator commit. The argument is parametric in 𝜃 : for every fixed 𝜃 ∈ Θ the homomorphism applies and the conclusion holds, regardless of how many distinct votes the oracle 𝐽 assigns across the rest of Θ𝜄 . Clause (2) is a structural observation. By Definition 7, 𝜃 1, 𝜃 2 differ only on the prompt sub-component; each deployment pins one, applies clause (1), and commits the first-call vote 𝑣𝑘 ∈ 𝐽 (𝑅, 𝜃 𝑘 ) to its own judge_log. For 𝑅 with |𝐵 Θ𝜄 (𝐽, 𝑅)| > 1 there exist 𝜃 1, 𝜃 2 with 𝐽 (𝑅, 𝜃 1 ) ≠ 𝐽 (𝑅, 𝜃 2 ), so the two deployments observe divergent committed votes while each internally satisfies clause (1). □ Proposition 4 (Achievable upper bound on the prompt-sensitivity image). For any oracle 𝐽 : Θ → {0, 1}, any evaluator intent 𝜄 with deployment-plausible prompt family Θ𝜄 (Definition 7), and any read-set 𝑅: |𝐵 Θ𝜄 (𝐽, 𝑅)| ≤ min |Θ𝜄 |, 2 . (3) The bound is achieved on 𝑅 exactly when Θ𝜄 contains both a 𝜃 + ∈ Θ𝜄 with 𝐽 (𝑅, 𝜃 + ) = 1 and a 𝜃 − ∈ Θ𝜄 with 𝐽 (𝑅, 𝜃 − ) = 0, in which case |𝐵 Θ𝜄 (𝐽, 𝑅)| = 2. The empirical boundary measure 𝜇Θ𝜄 (𝐽, Q) (Definition 8) counts the fraction of Q achieving equality. Proof outline. The cardinality bound follows from |{0, 1}| = 2 and the inclusion 𝐵 Θ𝜄 (𝐽, 𝑅) ⊆ {0, 1}. The min with |Θ𝜄 | tightens the bound when the family itself has fewer than two prompts. Achievability is constructive: any 𝑅 on which the family contains a positive-vote prompt and a negative-vote prompt yields {0, 1} ⊆ 𝐵 Θ𝜄 (𝐽, 𝑅), so |𝐵 Θ𝜄 (𝐽, 𝑅)| = 2 and the bound holds with equality. The empirical evidence below shows the bound is achievable but typically not saturated by alignment-trained judges on a benchmark slice. □ Empirical instantiation. The Phase 5 judge_pin_discriminating construction instantiates Θ𝜄 as a 2×2 factorial of {strict, lenient}prompt × {0, 0.7}temperature over the pinned judge claude-haiku-4-5-20251001, with raw cells in results/g2_utility/judge_pin_ discriminating/per_band.csv. Table 8 reports the empirical boundary measure 𝜇: the haiku four-band sweep (𝑛 = 75 per band) and the V1 cross-judge sweep (𝑛 = 300 on the PARTIAL band), whose three further judges span a 0.347 cross-judge spread with no judge reaching the saturating 1.0 even on the deliberately partial slice. A per-item decomposition on the haiku PARTIAL band (46 unstable of 75) attributes 42 of 46 to prompt-only disagreement (the two temperature levels agree, strict and lenient prompts disagree), 0 to temperature-only, and 4 to both axes (per_item.csv re-analysis), so the prompt axis dominates the boundary. The sweep supports Proposition 4’s “achievable but not saturated” framing and gives Lemma 3 a measured cross-deployment cost: a deployer choosing between 𝜃 strict and 𝜃 lenient on the PARTIAL slice walks past 50 to 85 percent of items whose verdict the choice itself decides.
18
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 8: Empirical judge prompt-sensitivity measure 𝜇 (Definition 8). Haiku is swept across four discriminating bands (𝑛 = 75); three further judges are swept on the PARTIAL band only (𝑛 = 300). The haiku PARTIAL band decomposes as 42 prompt-only, 0 temperature-only, 4 both axes (of 46 unstable items). Judge / band
𝜇
𝑛
claude-haiku-4-5, CONTROL claude-haiku-4-5, PARAPHRASE claude-haiku-4-5, DISTRACTOR claude-haiku-4-5, PARTIAL
0.00 0.07 0.01 0.61
75 75 75 75
deepseek-v4-flash, PARTIAL gpt-5.4-mini, PARTIAL gpt-5.4, PARTIAL
0.507 0.627 0.853
300 300 300
Scope of the lemma. The lemma does not claim N1 is unsound: clause (1) is Corollary 2 restated, and the iso-lattice guard map of Theorem 1 continues to exclude N1 on a fixed-𝜃 schedule. The lemma surfaces a separation between the engine layer (where the algebra applies) and the deployment layer (where prompt selection happens) without introducing a new operator or modifying the typing rules; the deployment-plausible family Θ𝜄 is a workload-side artefact a benchmark designer enumerates. It makes the honest N1 scope visible at the theorem layer.
B.7
Write-path configuration composition
The lemma below sits alongside the engine-layer composition lemma Lemma 2 and refines it: Lemma 2 governs the iso lattice and the schema lattice for the engine-layer precondition surface; the write-path lemma governs the deployment-configuration axis surface at the AnomalyWire verdict layer. Both compose sequentially. The lemma documents which configuration axis is closed under composition (read-path CR ) and which is not (write-path CW ). Lemma 4 (Write-path config composition under operator chaining). Let ⊕𝑎𝑛 ◦ · · · ◦ ⊕𝑎1 be a sequential composition of typed operators over the dual-row schema of §3.1 as in Lemma 2. For each operator ⊕𝑎𝑖 in the chain, let 𝑉𝑖 : CW −→ {trig, def, excl, n/a} be the operator’s contribution to the AnomalyWire verdict as a function of the write-path configuration 𝑐 ∈ CW of Definition 10. Let 𝑉comp (𝑐) denote the wire verdict of the composite. Then: (1) Read-path invariance composes. If every 𝑉𝑖 is invariant on CR (i.e. Proposition 7 applies to each operator’s schedule), then 𝑉comp is invariant on CR . Read-path invariance is closed under sequential composition. (2) Write-path perturbation propagates non-monotonically. If 𝑉𝑖 (𝑐) depends on 𝑐 ∈ CW for at least one 𝑖, 𝑉comp (𝑐) generally depends on 𝑐. The propagation is non-monotone: even if individual 𝑉𝑖 (𝑐) are each def at every 𝑐 ∈ CW , the composite 𝑉comp (𝑐) need not be def-stable across 𝑐 because intermediate storage-layer state shifts can cascade through the schedule’s subsequent reads. The lemma factors the engine-and-deployment guarantee surface: Lemma 2 bounds the iso-axis and schema-axis preconditions of the composite engine schedule; Lemma 4 bounds the configuration-axis dependence of the verdict that the composed wire schedule emits. Proof outline. Clause (1) follows from the read-path invariance of each 𝑉𝑖 plus the structural property of AnomalyWire’s schedule that no operator’s read step invokes the ranking-based retrieval policy. By Proposition 7 applied to each ⊕𝑎𝑖 , 𝑉𝑖 (𝑐 𝑅(1) ) = 𝑉𝑖 (𝑐 𝑅(2) ) for every 𝑐 𝑅(1) , 𝑐 𝑅(2) ∈ CR . The composite schedule executes the operators in order; at each intermediate step the storage-layer state read by ⊕𝑎𝑖+1 is the state committed by ⊕𝑎𝑖 , which by clause (1) hypothesis does not depend on the read-path knobs. The conclusion holds by induction on the chain length: the base case 𝑛 = 1 is Proposition 7 verbatim; the inductive step uses the intermediate-state invariance to lift the hypothesis to the (𝑛 + 1)-step composite. Clause (2) is a structural observation rather than a derivation from an algebraic identity. By Definition 10, a CW knob is one whose code-path trace reaches an operator’s vote-generating call (extractor prompt, adjudicator prompt, or storage-layer policy toggle that feeds the resolution rule). A perturbation 𝑐 → 𝑐 ′ on CW that shifts the storage trajectory between ⊕𝑎𝑖 ’s commit and the schedule’s subsequent reads can cascade to a different verdict at any downstream operator whose vote consumes the perturbed storage state. The empirical V3 cell-5 witness on the single-operator N2 schedule is the minimal instance of the cascade: a custom_instructions prompt-injection knob (CW by Definition 10) shifts mem0 v3’s internal ADD/UPDATE/DELETE vote at the second Memory.add call, alters the storage trajectory, and flips the third-read coexistence predicate |post| ≥ 2 from def to trig. The same shape lifts to the composite case by induction whenever the perturbed operator’s output enters a downstream operator’s read. □ Empirical instantiation. The V3+ multi-seed sweep at 5 seeds × 6 cells × 3 anomalies confirms clause (1) on the single-operator N2 wire: read-path invariance holds within every seed (results/anomaly_wire/config_invariance_sweep_multi_seed.csv). Clause (2) is 19
Ziming Wang
witnessed empirically on 4 of 5 seeds where at least one write-path cell perturbs the baseline triple. The composite case across multiple operators is observed indirectly via Phase 3 cross-system runs (where retrieval-policy axis dominance per Proposition 6 masks the underlying composition); the V6 matched-vs-unmatched cell ledger isolates the composition path under matched retrieval on three paired systems and two datasets, with the LoCoMo cells exhibiting the opposite-sign perturbation predicted by clause (2) of this lemma combined with the candidate-pool-size dependence of Extension B. Scope of the lemma. The lemma covers configuration knobs taxonomised by Definition 10; it does not cover source-code patches that change the storage layer or the operator implementation itself, which receive a fresh commit(𝑠) pin in Proposition 7. The lemma does not Ô modify the engine-layer composition of Lemma 2: 𝐿 ∗ = 𝐿𝑎𝑖 on the iso and schema lattices remains the typed precondition the composite schedule must satisfy. The configuration axis is orthogonal to the iso-and-schema lattices and concerns deployment-time perturbations that do not change the operator typing.
B.8
Operator-precondition witnesses and the composition table
The four typed operators from the algebra section have isolation preconditions 𝐿 ⊕t = RC, 𝐿 ⊕p = SI, 𝐿 ⊕? = RC+cb, 𝐿 ⊕c = SRpolicy . Before composition, Table 9 records the minimal weakening histories behind those signatures. These histories keep the operator signature as a typed contract consumed by the guard theorem; Theorem 1 still ranges over schedules satisfying the declared preconditions. Table 9: Minimal weakening histories for the four production operator preconditions. Each row weakens exactly one declared precondition and exposes the failure named by the operator signature. Tag
Operator
Weakened history
Exposed failure
LWW-RU EVI-RC AWAIT-NOCB RULE-SI
⊕t ⊕p ⊕? ⊕c
dirty overwrite before commit split evidence snapshot write-before-callback policy phantom
𝑃 0 /𝑃 1 boundary inconsistent evidence winner callback boundary policy 𝑃3
The callback row in AWAIT-NOCB is a callback_state entry in callback_log with fields (ℎ, 𝑅ℎ 𝑎𝑠ℎ, 𝑘, 𝑠𝑡𝑎𝑡𝑢𝑠, 𝑑𝑒𝑙𝑖𝑣𝑒𝑟𝑒𝑑𝑎 𝑡). The safe schedule requires status=delivered and the order candidate read precedes callback-log read, callback-log read precedes operator write. Sequential composition ⊕𝑏 ◦ ⊕𝑎 requires a schedule that holds both 𝐿𝑎 and 𝐿𝑏 ; the lemma states that the composite holds the lattice join 𝐿𝑎 ∨ 𝐿𝑏 . Table 10 enumerates the 16 ordered pairs. Joins are component-wise in Liso × Lcb : RC ∨ SI = SI on the iso axis, ⊥ ∨ cb = cb on the callback axis, and the policy annotation composes by requiring SR only on the named policy table. The callback component denotes the delivered callback_log row whose read is ordered between the candidate read and operator write. Table 10: Pairwise composition ⊕𝑏 ◦ ⊕𝑎 from the algebra section; cell shows the composite precondition 𝐿𝑎 ∨ 𝐿𝑏 in L = Liso × Lcb . RC+cb abbreviates the product element (RC, cb) and the “+cb” compounds abbreviate the corresponding product joins. “SRp ” abbreviates the per-table annotation SRpolicy that pins the policy table to SR; cells carrying SRp apply the annotation on top of the underlying product join. ⊕𝑎 \⊕𝑏
⊕t
⊕p
⊕?
⊕c
⊕t (RC) ⊕p (SI) ⊕? (RC+cb) ⊕c (SRp )
RC SI RC+cb SRp
SI SI SI+cb SRp
RC+cb SI+cb RC+cb SRp +cb
SRp SRp SRp +cb SRp
All sixteen cells of Table 10 are exercised by integration tests under tests/integration/test_compose.py against the reference implementation bitemporal.ingestion.ingest: four diagonal cells covering idempotent self-composition ⊕𝑎 ◦ ⊕𝑎 and twelve off-diagonal cells covering distinct-operator pairs ⊕𝑏 ◦ ⊕𝑎 with 𝑎 ≠ 𝑏. Each cell corresponds to a schedule whose every transaction holds the cell’s isolation level; the dual-row schema’s audit row is independent of the isolation-level join, which is why we factor soundness into two theorems on orthogonal lattices: the anomaly-soundness theorem over Liso for the seven classical and the two LLM-specific corollaries, and the audit-erasure theorem over Lschema for N3.
B.9
Expanded anomaly guard surface
Table 11 expands the compact guard surface from the main paper. The main paper keeps only the review-facing summary; this subsection records the exact representation, check, and enforcement wording. 20
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 11: Expanded anomaly guard surface. Rows separate representation, checking, and enforcement across the iso and schema axes. Anomaly
Origin
Representation
Check
Enforcement
𝑃0 dirty write 𝑃1 dirty read 𝑃2 fuzzy read 𝑃3 phantom
Berenson 1995 §4 Berenson 1995 §4 Berenson 1995 §4 Berenson 1995 §4
Berenson–Adya dirty write Berenson–Adya dirty read Berenson–Adya fuzzy read Berenson–Adya phantom
𝐿 ≥ RC 𝐿 ≥ RC 𝐿 ≥ SI 𝐿 ≥ SR
schedule satisfies read committed schedule satisfies read committed schedule satisfies snapshot isolation schedule satisfies serializable predicate reads snapshot-isolation write-conflict check aborts the overwrite snapshot isolation pins every read to one snapshot serializability rejects the dependency cycle
𝑃4 lost update
Berenson 1995 §6
Berenson–Adya lost update
𝐿 ≥ SI
𝐴5𝐴 read skew
Berenson 1995 §6
Berenson–Adya read skew
𝐿 ≥ SI
𝐴5𝐵 write skew
Berenson 1995 §6
Berenson–Adya write skew
𝐿 ≥ SR
N1 judge-replay inconsistency
this paper
judge replay keyed by read set and decoder tuple
equal votes for a fixed replay key
N2 belief-drift skew
𝐴5𝐵 specialisation (this
𝐴5𝐵 lifted to the (subj, pred) partition
𝐿 ≥ SR on the partition
judge table held at SR with output hash logged partition satisfies SR
N3 audit erasure
paper) this paper
K-relation reachability
𝑝𝑙 ⪯𝐾 𝑝 audit
every operator emits an audit row
C
OPERATOR ALGORITHMS AND SCHEMA
This appendix answers one reviewer question precisely: where the write-time contract of §3.2 is enforced in the reference implementation. The answer has four parts. The dual-row bitemporal schema (§C.1) gives the typed operators a place to land. The four operator algorithms (§C.2) realise the four §3.2 inference rules as pure functions. The ingestion seam (§C.3) is the single point where the algebra meets persistent storage, and it owns the loser-close, winner-insert, and audit-persist sequence. The isolation pin (§C.4) is set per worker on the PostgreSQL backend, and the judge-log row (§C.5) is written before the operator commits, which is what makes the Lemma 1 ordering hold structurally rather than by caller discipline. Every column, function name, file location, and behavior below is read from the implementation under implementation/bitemporal/.
C.1
Dual-row bitemporal schema
The table agent_memory carries eleven user-visible columns plus a physical twelfth discriminator. The eleven user-visible columns are the §3.1 narrative SSOT: fact_id, subject, predicate, object, valid_from, valid_to, system_time_start, system_time_end, provenance_id, confidence, and resolution_strategy_id (the COLUMNS tuple at schema.py:65–77). The twelfth column row_kind is the N3 defence: a CHECK-constrained TEXT discriminator over row_kind ∈ {current, audit} with a default of current, giving the twelve-column physical layout ALL_COLUMNS at schema.py:81. Current-kind rows are the §3.1 eleven-column schema; audit-kind rows carry the loser lineage emitted by every operator. Table 12 lists the five integrity constraints the class-level DDL string at schema.py:88–107 declares to pin the write-time contract at the storage layer. Table 12: Storage-layer integrity constraints from the agent_memory DDL (schema.py:88–107). Constraint
Target
Rule
confidence range row-kind domain primary key valid-period order system-period order
confidence row_kind (fact_id, system_time_start) valid_from, valid_to system_time_start, system_time_end
CHECK (confidence BETWEEN 0.0 AND 1.0) CHECK (row_kind IN (’current’, ’audit’)) two system-time versions of one fact coexist CHECK (valid_from < valid_to) CHECK (system_time_start < system_time_end)
DuckDB ships no native SQL:2011 temporal tables, so the four timestamp columns are hand-rolled rather than declared through a PERIOD FOR clause. The temporal predicate is implemented as the as_of class method (schema.py:183–220) under closed-open semantics (system_ time_start ≤ 𝑡 < system_time_end); it defaults to row_kind = current so the §3.1 retrieval narrative is preserved, and accepts kind= ’audit’ or kind=’all’ for audit inspection. The open upper bound is the sentinel 9999-12-31 (Schema.SENTINEL_END, schema.py:86). A version is closed by close (schema.py:246–279), which raises LookupError when no open current row matches the fact_id rather than failing silently. The schema admits three modes through Schema.create’s mode kwarg (schema.py:111–148): audit_row (default), dual_row, and base. The physical table is identical across all three; the mode is validated at construction and the persistence-behavior change lives at the ingestion layer (§C.3). An unknown mode raises ValueError at create time (schema.py:143–147), which keeps the schema-mode ablation axis validated before a misspelt mode reaches a silent ingest behavior change. 21
Ziming Wang
C.2
The four operator algorithms
The four operators are the classes LWW, Evidence, AwaitConfirm, and PerRule (operators.py:159–285). Each is a pure function from a pair of contradicting facts to a stamped winner and an AuditRow, and each carries a typed isolation_level class attribute that names its scheduling precondition: LWW at RC, Evidence at SI, AwaitConfirm at RC+cb, and PerRule at SR. The contradiction predicate is the function is_contradiction (operators.py:58–71): two facts contradict when subject and predicate agree, object differs, and the closed-open valid-time periods overlap. All four share the dual-row machinery _resolve_dual_row (operators.py:135–154), which computes the provenance merge 𝑝 𝑤 ⊕ 𝑝𝑙 once, stamps the winner, and emits the AuditRow. The shared steps are: (1) Reject non-contradicting inputs with ValueError through _require_contradiction (operators.py:126–132). (2) Choose the winner-loser ordering by the operator’s selector (the only step that differs across the four; see below). (3) Compute 𝑝 𝑤 ⊕ 𝑝𝑙 via merge_provenance (audit.py:40–56), the commutative semiring sum over the 𝐾 [𝑋,𝑇 ] witness polynomial. (4) Stamp the winner through _stamp_winner (operators.py:76–92): a fresh system_time_start set to now, system_time_end set to the open sentinel, the resolution_strategy_id stamp, and the merged provenance_id. (5) Materialize the AuditRow through _build_audit (operators.py:95–123), keyed on (loser_fact_id, system_time). The four operators differ only in step 2, the winner selector, summarised in Table 13. An out-of-range return from the AwaitConfirm callback or the PerRule policy oracle raises ValueError; the callback is the external oracle (human review, regulated-vertical confirmation, or upstream agent decision). Table 13: The four operator winner-selectors. Each names its isolation precondition, strategy id, selection rule with source line, and the anomaly its level admits or precludes. Operator (iso, strategy)
Selector (source)
Anomaly
LWW (RC, lww)
larger (system_time_start, fact_id) pair (operators.py:178–184); last writer wins larger (confidence, system_time_start, fact_id) tuple (operators.py:209–216); confidence-weighted external callback returns 0/1 (operators.py:236–253)
admits 𝑃4 lost-update
Evidence (SI, evi) AwaitConfirm (RC+cb, await) PerRule (SR, rule)
policy oracle returns 0/1 (operators.py:268–285); serializable on policy table
admits A5B write-skew no admitted anomaly precludes 𝑃3 phantom
The operators never mutate persistent storage. Closing the loser is the caller’s responsibility, documented in the operators.py module @breaks contract: the operator returns the AuditRow whose loser_fact_id the caller passes to Schema.close. This division is what keeps the four operators pure and the persistence policy in one place.
C.3
Transaction boundary at the ingestion seam
The single seam where the algebra meets persistent storage is the ingest function (ingestion.py:181–361). It is the write-path enforcement point the reviewer question targets. For each incoming fact it executes the eight-step sequence of Table 14, and the caller, not ingest, owns the surrounding transaction commit and rollback. The loser-close-then-winner-insert ordering at step 7 and the audit-persist at step 8 are the storage-side realisation of the Fact × Fact → (Fact, Audit) signature. The audit packer pack_audit_row (audit.py:139–170) materializes the twelve-column physical row: a fact_id of the form audit::{loser}::{system_time}, the conflict witness encoded as winner_object | loser_object in the object column, the merged provenance_id, and row_kind = audit.
C.4
Isolation pin per session
The isolation level is a typed precondition in the algebra and a real session pin in the systems backend. In the algebra, each operator carries its required level as the isolation_level class attribute (operators.py:167, 198, 233, 265), and the baselines record the level they actually run at in the partition_isolation field of the Baseline abstract class (anomaly_bench/baselines.py:112), typed over {none, RC, SI, SR}. The real isolation pin is set per worker connection on the PostgreSQL backend. Each writer process opens its own connection and begins every contradiction-resolution transaction with BEGIN ISOLATION LEVEL SERIALIZABLE (g3_systems_perf/postgres_backend.py:330). Inside that transaction the worker reads the incumbent open current row FOR UPDATE, closes it by setting system_time_end, inserts the winner, and lets serialization failures surface as isolation-level outcomes rather than retrying or hiding them. This is the empirical analogue of the SR precondition that PerRule names: the abstract level on the operator becomes a concrete SERIALIZABLE session pin on a real engine, and §4.3 measures its lock-contention signature. 22
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 14: The eight-step ingestion sequence at the write seam (ingestion.py:181–361). Each step names its action, source line, and the failure it raises rather than masks. #
Action
1
validate ablation knobs: coerce operators_on, reject unknown ingestion.py:111–153, schema_mode 231–235 read open current rows for the (subject, predicate) partition ingestion.py:156–178 (row_kind = current, system_time_end at open sentinel) via _open_rows_for_partition same-object overlapping-valid-time write is a duplicate confirmation, ingestion.py:257–263 return without insert (contradiction predicate requires object to differ) select contradicting incumbents via is_contradiction; no incumbent ingestion.py:264, 265–267, inserts a fresh open row and returns; > 1 incumbent raises (binary 268–274 operators need a single incumbent) enforce operator-on/off ablation: a resolution_strategy_id absent ingestion.py:286–296 from an active operators_on set raises rather than reroute or drop dispatch to the operator named by resolution_strategy_id: lww, evi, ingestion.py:298–324 await (needs callback), rule (needs policy) if incumbent lost, Schema.close at audit timestamp then ingestion.py:326–335, Schema.insert the stamped winner; if new fact lost, incumbent stays 336–338 open and the rejected fact survives only in the audit row (no silent insert of a lost row) persist the audit row per schema_mode: audit_row packs via ingestion.py:339–360 pack_audit_row and inserts at row_kind = audit; dual_row and base return the in-flight pair but do not persist the audit half
2
3 4
5 6 7
8
Source
Failure ValueError on bad mode –
– ValueError on > 1
OperatorNotEnabledError ValueError on unknown id –
–
The DuckDB-backed reference path under implementation/bitemporal/ carries no SET TRANSACTION call; its isolation guarantee is the typed annotation plus the single-incumbent invariant at the ingestion seam, and the PostgreSQL backend supplies the multi-process serializable evidence. This split is deliberate: the algebra states the precondition, the DuckDB path proves the abstraction compiles and resolves, and the PostgreSQL path proves the precondition is enforceable on a production engine.
C.5
Judge-log write ordering
The judge-log row is written before the operator commits. This is the ordering that makes Lemma 1 hold structurally. The OperatorDispatcher class (operators.py:307–406) carries an in-memory judge_log keyed on the pair (𝑅, 𝜃 ), where 𝑅 is the contradictingfact signature (f1.fact_id, f2.fact_id) and 𝜃 is the judge parameter pin (prompt, seed, model version, temperature, tool-output hash; operators.py:300–304). The two dispatch methods dispatch_await (operators.py:353–379) and dispatch_rule (operators.py:381–405) follow the same ordering contract: (1) Reject non-contradicting inputs through _require_contradiction. (2) Compute the judge vote by invoking the callback or policy. (3) Write the witnessed vote to judge_log[(𝑅, 𝜃 )] through _log_judge_call (operators.py:332–351), which appends synchronously and preserves multiplicity. This write completes before any state mutation. (4) Delegate to the free operator (AwaitConfirm or PerRule) with the already-computed vote. (5) Invoke the caller-supplied commit_hook (for example Schema.close on the loser) only after the log write and the resolution. The log write at step 3 strictly precedes the commit_hook at step 5 because the control flow is synchronous Python; the dispatcher supplies the ordering rather than leaving it as a precondition the caller must maintain. This realises hypothesis H1 of Lemma 1: every 𝑗𝑖 (𝑅, 𝜃 ) event is paired with a committed row at key (𝑅, 𝜃 ) whose commit precedes the operator’s commit. The free operator surfaces remain available for callers that own their own logging; the dispatcher is the reference implementation that closes the silent-lie risk where the paper claimed enforcement and the bare operator did not provide it.
C.6
Schema-lift conservatism
The audit-row refinement adds the single CHECK-constrained column row_kind ∈ {current, audit} above the eleven-column base schema; no base column changes shape. Let Qbase denote the relational-algebra fragment over the base columns: any composition of selection 𝜎, projection 𝜋, join Z, union ∪, difference \, and the bitemporal AS OF (𝑡 𝑣 , 𝑡𝑠 ) predicate whose selection predicates and projection lists do not reference row_kind. By construction Qbase does not reference the auxiliary judge_log or callback_log tables: those tables exist only in the operator-infrastructure schema and do not surface in the base-schema fragment a deployed system upgrades from. Each 𝑞 ∈ Qbase lifts to 23
Ziming Wang
a query 𝑞 ∗ on the audit-row schema by structural induction on the constructors: at each table-scan leaf the lift prepends the default filter 𝜎row_kind=current ; at each internal node the liftis the same constructor applied to the lifted operands. The base table 𝑇 and a lifted instance 𝑇 ∗ are related by 𝑇 = 𝜋1..11 𝜎row_kind=current (𝑇 ∗ ) , where 𝜋1..11 drops the discriminator. Proposition 5 (Schema-lift conservatism). For every 𝑞 ∈ Qbase and every audit-row instance 𝑇 ∗ , 𝑞 ∗ (𝑇 ∗ ) = 𝑞 𝜋1..11 𝜎row_kind=current (𝑇 ∗ ) . Equivalently, every Qbase -query evaluated on the audit-row schema returns the same answer as the same query evaluated on the base-schema table whose rows are the current-kind rows of 𝑇 ∗ . Proof. The CHECK constraint pins row_kind ∈ {current, audit}, so 𝜎row_kind=current projects 𝑇 ∗ onto its current-kind sub-relation 𝑇 ′ , and 𝜋1..11 (𝑇 ′ ) matches the base-schema row type by construction. The proof proceeds by induction on the Qbase constructors. Selection. For 𝑞 = 𝜎𝜑 (𝑞 1 ) with 𝜑 ignoring row_kind, 𝜎𝜑 commutes with 𝜎row_kind=current because their predicates address disjoint columns; the inductive hypothesis on 𝑞 1 closes the case. Projection. For 𝑞 = 𝜋𝐿 (𝑞 1 ) with 𝐿 ⊆ {1, . . . , 11}, the inductive hypothesis gives 𝑞 1∗ (𝑇 ∗ ) = 𝑞 1 𝜋1..11 𝜎row_kind=current (𝑇 ∗ ) ; applying 𝜋𝐿 to both sides and using 𝜋𝐿 ◦ 𝜋1..11 = 𝜋𝐿 on lifted rows closes the case. Binary constructors (Z, ∪, \). The default filter distributes over the operator and applies to each operand; inductive hypotheses on each operand close the case. Bitemporal AS OF (𝑡 𝑣 , 𝑡𝑠 ). The predicate selects on columns 5–8, disjoint from the discriminator, so it commutes with 𝜎row_kind=current by the same argument as selection. □ Proposition 5 pairs with Theorem 2: the audit-row refinement defends N3 and preserves the answer to every Qbase -query. A deployed system upgrading from base to audit-row schema adds the discriminator column and the audit-row slice; queries that do not mention row_kind keep their answers verbatim, and audit-rule retrieval becomes available through the as_of(kind=’audit’) path without rewriting any pre-existing read path.
C.7
Memory-pipeline decomposition
The four typed operators sit at the write boundary; a deployed agent-memory system surrounds them with a retrieval policy on the read side and a synthesis stage that turns retrieved candidates into a user-visible answer. The algebra is silent on both surrounding stages by design: it specifies the contradiction-resolution contract on the write path and on a candidate set, and leaves retrieval-policy choice and synthesis-style choice to deployment. Definition 9 (Memory-pipeline decomposition). A memory pipeline is a triple 𝑃 = (R, A, S) where R : (query, store) → candidate-set is the retrieval policy mapping a query plus the materialized store to a bounded candidate set (top-𝑘 vector similarity, BM25 ranking, structural traversal, or the trivial include-all); A is the typed contradiction-resolution algebra on the write path and on the candidate set returned by R; S : (candidate-set, query) → answer is the synthesis stage (language-model prompt-and-decode or deterministic concatenation). A does not constrain R or S; the algebra acts after retrieval has bounded the candidate set and before the synthesis stage commits an answer. Proposition 6 (Cross-system Δaccuracy axis attribution). Let 𝑃1 = (R1, A1, S1 ) and 𝑃2 = (R2, A2, S2 ) be two pipelines paired on benchmark Q under a shared judge 𝐽 . The paired accuracy delta Δaccuracy (𝑃 1, 𝑃2 ; Q, 𝐽 ) = E𝑞∼Q 𝐽 S1 (R1 (𝑞), 𝑞), ref 𝑞 − 𝐽 S2 (R2 (𝑞), 𝑞), ref 𝑞 attributes to the algebra axis A1 versus A2 only when R1 = R2 on Q and S1 = S2 on candidate sets and queries. When R1 ≠ R2 , the delta is dominated by the retrieval-policy axis on workloads where retrieval recall is the bottleneck (e.g. needle-in-haystack benchmarks); when S1 ≠ S2 , the delta is dominated by the synthesis-style axis on workloads where answer-shape conformity drives judge score. Proof outline. Δaccuracy is by construction a function of the three components of each pipeline plus the workload and judge. Holding the workload and judge fixed, the delta is a difference over three orthogonal axes; isolating the algebra-axis contribution requires the remaining two axes to agree between the paired pipelines. The retrieval-policy bottleneck on needle-in-haystack workloads is the standard recall-saturation argument: when one pipeline’s |R(𝑞)| excludes the gold passage by construction, the synthesis stage cannot recover it, and the algebra cannot distinguish itself from the read-side ceiling. The synthesis-style bottleneck on answer-shape-sensitive judges follows from the prompt-sensitivity image: a judge whose verdict depends on prompt phrasing of the answer candidate scores systematically differently on long-form synthesis versus extractive snippets. □
D
ADAPTER VERDICT LEDGER
Table 4 reports a verdict for each baseline against each schedule predicate {N1, N2, N3} in two columns: a Claim column from the AnomalyClaim design-path model and a Wire column from the AnomalyWire runtime layer. This appendix makes every cell auditable. Each system carries one witness card per predicate; the card pins the verdict to a source file, a line range, a pinned upstream commit, the minimal triggering history the harness runs, the trace the harness expects to observe, and the raw log path. For abstentions the card states the structural reason the layer cannot witness the predicate rather than reporting a verdict the construction cannot support. The ledger folds the 24
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 15: Pinned-commit manifest. One revision per clone; table cells use the seven-hex prefix. Adapter kind is the maximal kind present for the system across its predicates (transcribed, imported, or both). System
Commit
Upstream primary path
Adapter kind
mem0 v2 mem0 v3 Graphiti Letta Zep WorldDB Toki
a623caf a623caf c427615 bb52a89 faf2ace arxiv-2604.18478-v1 HEAD
mem0/memory/main.py mem0/memory/main.py graphiti_core/edges.py letta/services/block_manager.py legacy/src/store/memory_ce.go Algorithm 2 (contradicts handler) operators.py + ingestion.py
transcribed transcribed, imported transcribed, imported transcribed, imported transcribed, imported transcribed imported
read-path versus write-path configuration scope (Section D.5) and the cross-system measurement protocol (Section D.6) that bound the interpretation of these cells.
D.1
Reading a cell
The Claim column reads the structural model in experiments/anomaly_bench/baselines.py: each baseline declares three fields (judge_ kind, partition_isolation, recovers_provenance) and three frozen trigger sets (N1_NAMED_TRIGGERS, N2_NAMED_TRIGGERS, N3_NAMED_ TRIGGERS) name which baseline admits which predicate under the Section 4.1 taxonomy. The Wire column reads the adapter layer: transcribed adapters (experiments/anomaly_wire/adapters.py) encode the upstream control flow by hand with file:line citations, and imported adapters (experiments/anomaly_wire/<system>_imported.py) call the real upstream contradiction-resolution entry point under a seedpinned deterministic-judge stub. The runner verifies each clone sits on its pinned commit before any adapter executes; a drifted clone raises rather than silently producing a wrong cell. A wire cell is one of three evidence kinds. A transcribed cell (T) cites the upstream line that produces the verdict. An imported cell (I) that executes carries the runtime trace observed on the pinned commit. An imported cell that abstains records status="n/a" because the deterministic-judge stub cannot witness the predicate by construction, or because the predicate is structurally undefined under the upstream schema. Of the fifteen imported cells, nine carry executable verdicts and six abstain; Section D.4 names each abstention.
D.2
Pinned commits
The AnomalyWire manifest (experiments/anomaly_wire/manifest.py) pins each clone to one revision. Table cells show the short seven-hex prefix; the full revisions are: mem0 v2 and v3 share a623cfaf76ae7379a58be1e837f8a88a9b15a184 on mem0/memory/main.py; Graphiti is c427615044678f4bde026745d8d28a16504868c5 on graphiti_core/edges. py; Letta is bb52a8900a79cf1378e6e9cdecf244b673a13a72 on letta/services/block_manager.py; Zep CE is faf2acec4f2ec777a27d8fe0411619bc913a9660 on legacy/src/store/memory_ce.go; WorldDB pins the arXiv revision arxiv-2604.18478-v1 at Algorithm 2 because no public code drop exists; the Toki row runs the in-repo implementation at HEAD. The imported Zep cell additionally pins the Zep Cloud service boundary at zep-cloud-api-v2-2026-05-13.
D.3
Witness ledger
Table 16 traverses the eleven adapter rows of Table 4 in registry order, one row per (system, predicate). Each verdict is encoded A (admit), X (exclude), or − (abstention) in the Claim (design-path) and Wire (runtime) columns. The mechanism column states the structural reason behind the verdict (or, for an abstention, why the layer cannot witness the predicate); the source column pins the verdict to the adapter line that produces it. The status value the adapter returns is trig for an admit, excl for an exclude, def for a defended exclusion (Toki, or a runtime divergence such as mem0 v3-I N2), and n/a for an abstention. The raw log column names the per-workload CSV under results/anomaly_wire/; the runner regenerates these from the pinned clones on demand, so the verdict authority is the cited adapter source. The Claim-authority baselines.py lines follow the table. Table 16: Witness ledger. Every (system, predicate) cell of Table 4 with its Claim and Wire verdict (A admit, X exclude, − abstain), the structural mechanism or abstention reason, the adapter source line, and the raw-log CSV. System
Pred.
Cl.
Wi.
Mechanism / abstention reason
mem0 v2 (T)
N1
−
−
mem0 v2 (T) mem0 v2 (T)
N2 N3
−
−
A
A
no LLM judge votes across replays in ADD/UPDATE/DELETE path; adapters.py:110 judge absent in contradiction path no (subj, pred) confidence-weighted partition rerank adapters.py:120 DELETE branch removes loser with no audit row; no vote outcome adapters.py:130 preserves 𝑝 old reachability under ⪯𝐾 . History: alice/lives_in/LA then alice/lives_in/NYC
Source
mem0 v3 (T)
N1
A
A
mem0 v3 (T)
N2
A
A
retrieval rerank invokes LLM with no decoder-seed pin; replay returns adapters.py:194 distinct votes (source unpinned even though stub pins) rerank reads (subj, pred) partition at SI adapters.py:208
Raw log – – –
– –
continued on next page 25
Ziming Wang
Table 16 continued System
Pred.
Cl.
Wi.
Mechanism / abstention reason
Source
Raw log
mem0 v3 (T)
N3
A
A
ADD-only accumulation shadows older fact at retrieval, no audit emission
adapters.py:218
–
mem0 v3 (I)
N1
A
−
N2
A
X
mem0 v3 (I)
N3
A
A
deterministic stub returns identical votes by construction, cannot mem0_v3_imported.py:310 witness divergence; N1 delegated to transcribed companion mem0_v3_imported.py:363 runtime divergence: Memory.add hi- then lo-confidence on same (subj, pred) , but get_all snapshot returns one row ( | post | = 1); retrieval collapses competing rows under deterministic judging, status def writes Alice’smanagerisBob then Carol, walks Memory.history, mem0_v3_imported.py:418 finds no audit entry naming superseded Bob fact
n2,n3.csv
mem0 v3 (I)
Graphiti (T)
N1
A
A
N2 N3
−
−
A
A
resolve_edge_contradictions LLM call selects winning edge with adapters.py:267 no decoder-seed pin (cites edge_operations.py) edges carry no (subj, pred) confidence partition adapters.py:277 handler sets invalid_at on older edge, emits no audit edge with adapters.py:287 merged provenance (cites graphiti_core/edges.py)
–
Graphiti (T) Graphiti (T) Graphiti (I)
N1
A
−
n3.csv
Graphiti (I)
N2
−
−
Graphiti (I)
N3
A
A
duck-typed deterministic bridge (singular entry graphiti_imported.py:340 resolve_extracted_edge at edge_operations.py:622) cannot produce vote divergence timestamp-only Bob-Alice then Bob-Carol run end to end, invalidation graphiti_imported.py:374 driven by valid_at; EntityEdge has no confidence partition field, predicate undefined inspects EntityEdge.model_fields, finds no fact-level superseder graphiti_imported.py:432 (superseded_by, replaces, replaced_by_uuid); temporal-window supersession fails ⪯𝐾
Letta (T)
N1
−
−
–
N2
A
A
block updates use deterministic precedence, no LLM judge in contradiction path block-history confidence updates read (subj, pred) partition at SI without serializing the rewrite block snapshot history disjoint from message trace
adapters.py:338
Letta (T)
adapters.py:348
–
Letta (T)
N3
A
A
Letta (I)
N1
−
−
Letta (I)
N2
A
−
Letta (I)
N3
A
A
Zep (T)
N1
−
−
Zep (T)
N2
A
A
Zep (T)
N3
A
A
Zep (I)
N1
−
−
Zep (I)
N2
A
A
Zep (I)
N3
A
A
WorldDB (T)
N1
X
X
WorldDB (T)
N2
X
X
WorldDB (T)
N3
X
X
Toki (I) Toki (I) Toki (I)
N1 N2 N3
X X X
X X X
adapters.py:358
n2,n3.csv
n2,n3.csv
– –
n3.csv
n3.csv
–
checkpoint path is LLM-free letta_imported.py:276 (BlockManager.checkpoint_block_async on live BlockHistory, block_manager.py:842), no decoder to mis-replay two-checkpoint schedule; BlockHistory carries sequence_number, letta_imported.py:294 actor_id but no confidence partition field, predicate undefined checkpoints BobmanagesAlice (seq 1) then Carol (seq 2); letta_imported.py:311 BlockHistory columns ∩ superseder-field set is empty, supersession implicit in sequence order only
n3.csv
CE wrapper delegates retrieval to Graphiti HTTP service, no local LLM judge row (cites legacy/src/store/memory_ce.go) GetMemory/Search return Graphiti facts with no (subj, pred) serializable partition boundary DeleteFact forwards to Graphiti with no merged-provenance audit tuple (cites fact_handlers_ce.go)
adapters.py:409
–
adapters.py:419
–
adapters.py:429
–
Zep Cloud graph API (artifact pinned zep-cloud-api-v2-2026-05-13) exposes no local decoder-judge replay row edge schema exposes relevance/search scores but no confidence-weighted serializable partition boundary. History: two distinct-confidence (subj, pred) episodes (zep_imported.py:150) edge schema carries source episodes + validity timestamps but no fact-level superseder audit edge. History: two manager-assignment episodes
zep_imported.py:283
zep_imported_run. json
zep_imported.py:281
zep_imported_run. json
zep_imported.py:282
zep_imported_run. json
n3.csv n3.csv
engine never calls LLM on read path (preprint App. B); deterministic adapters.py:479 reconciler, excluded by construction contradicts handler emits both edges and computes the partition adapters.py:508 winner at query time with no confidence-weighted rerank; belief-drift skew excluded by construction at the engine layer content-addressed Merkle ancestry retains the overwritten fact, so the adapters.py:518 recoverable-provenance property holds; audit erasure excluded at the engine layer
–
SR on logged-judge table with judge seed and prompt pinned SR on the (subj, pred) partition audit-row schema lift: OursWire._run_with_audit ingests the pair, checks emitted audit row dominates both inputs under ⪯𝐾 via provenance_dominates, status def
n1,n2,n3.csv n1,n2,n3.csv n1,n2,n3.csv
adapters.py:560 adapters.py:560 adapters.py:560
–
–
The mem0 v3 imported N2 cell is a genuine design-path-to-runtime divergence (Claim A, Wire X): the transcribed companion admits N2 by structural inspection, while the imported run defends it because mem0 v3 retrieval collapses the competing rows under deterministic judging. The cross-layer audit surfaces the divergence rather than suppressing it. The Claim-column authority is the structural model in experiments/anomaly_bench/baselines.py: Mem0V2Simulated (judge_ kind="none", partition_isolation="none", in N3_NAMED_TRIGGERS only, baselines.py:135); Mem0V3Simulated (judge_kind= "stochastic", partition_isolation="SI", all three trigger sets, baselines.py:171); GraphitiSimulated (judge_kind="stochastic", partition_isolation="none", in N1_NAMED_TRIGGERS and N3_NAMED_TRIGGERS, baselines.py:213); LettaSimulated (partition_ isolation="SI", in N2_NAMED_TRIGGERS for N2 and N3_PENDING_TRIGGERS for the extrapolated N3, baselines.py:256); ZepSimulated 26
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 17: The six abstaining imported cells. Each records status="n/a" on structural grounds, not a missing run. R1 = deterministic-judge stub cannot witness N1 vote divergence; R2 = upstream schema has no confidence-weighted (subj, pred) partition field, so N2 is undefined. Cell
Pred.
Source
Reason
mem0 v3-I Graphiti-I Graphiti-I Letta-I Letta-I Zep-I
N1 N1 N2 N1 N2 N1
mem0_v3_imported.py:310 graphiti_imported.py:340 graphiti_imported.py:374 letta_imported.py:276 letta_imported.py:294 zep_imported.py:283
R1: stub cannot witness vote divergence R1: deterministic bridge cannot diverge R2: EntityEdge has no confidence partition field R1: checkpoint path is LLM-free R2: BlockHistory has no confidence partition field R1: Cloud graph API exposes no decoder-judge replay row
(partition_isolation="SI", in N2_NAMED_TRIGGERS for N2 and N3_PENDING_TRIGGERS for N3, baselines.py:292); WorldDBSimulated (judge_kind="deterministic", absent from all three trigger sets, baselines.py:328; the engine-layer exclusion is the cousin-scope analysis of Section D.6); and OursSimulated (judge_kind="pinned", partition_isolation="SR", dual-row audit recovery via recover_ provenance, baselines.py:592). The Toki Claim-column star in Table 4 marks the mechanism: N1 via SR on the judge table, N2 via SR on the partition, N3 via the audit-row schema lift.
D.4
The six abstaining imported cells
Six of the fifteen imported cells abstain. Two structural reasons account for all six. The first is the deterministic-judge construction: the wire harness must be reproducible, so every imported adapter consumes a seed-pinned DeterministicJudge stub that returns identical votes on identical (seed,prompt) pairs. A stub that cannot diverge cannot witness the N1 judge-replay predicate, so every imported N1 cell delegates the verdict to its transcribed companion and records status="n/a". The second is schema undefinedness: the N2 predicate requires a confidence-weighted (subj, pred) partition, and Graphiti’s EntityEdge and Letta’s BlockHistory expose no such field, so the predicate is structurally undefined and the adapter abstains after running the schedule end to end.
D.5
AnomalyWire deployment-configuration scope
The wire cells of Table 4 are pinned to the upstream commits of Table 15. This section states which configuration axis each verdict is constant on so a reviewer reads each cell against a precise scope. Definition 10 (Read-path and write-path deployment configuration). Let C be the deployment configuration space of an agent-memory system 𝑠. We split C into two disjoint axes: CR (read-path). Configuration that affects only how the retrieval policy R ranks or filters candidate facts: ranking metric (ℓ2 versus cosine), vector normalization, top-𝑘 truncation, reranker on or off. CW (write-path). Configuration that enters the operator’s contradiction-resolution decision inputs at write time: prompt injections into the extractor or adjudicator language model, extractor model identity when the operator’s vote depends on it, or a graph-store toggle when graph membership feeds the resolution rule. The split is per-system: a knob is in CR for system 𝑠 if and only if a code-path trace from the wire schedule does not reach the operator’s vote-generating call under that knob. Proposition 7 (AnomalyWire verdict read-path configuration-invariance). For each system 𝑠 pinned to upstream commit commit(𝑠) by the AnomalyWire manifest, the verdict function 𝑉𝑎 (𝑠, commit(𝑠), ·) is constant on CR : for every 𝑐𝑖 , 𝑐 𝑗 ∈ CR and every anomaly 𝑎 ∈ {N1, N2, N3}, 𝑉𝑎 (𝑠, commit, 𝑐𝑖 ) = 𝑉𝑎 (𝑠, commit, 𝑐 𝑗 ). The same statement does not hold on CW : write-path configuration enters the operator’s vote at write time and can shift the storage-layer trajectory between the schedule’s writes and the schedule’s read. Proof outline. The wire verdict for each anomaly is constructed from a fixed schedule that probes the storage-layer commitment of the upstream contradiction-handling path. The schedule’s read step does not invoke the retrieval policy R on the ranked-search path; it invokes filter-by-user reads and audit-trail walks, both of which read materialized storage rather than ranked candidates. Hence CR knobs do not enter the read step. The schedule’s write step invokes the language model for the add-or-update decision; any CW knob that enters that prompt shifts the vote, the storage trajectory, and ultimately the read-step predicate the wire checks. □ Empirical witnesses. A six-cell configuration sweep on mem0 v3 witnesses both halves of the proposition. Four read-path perturbations (distance metric, 𝐿2 normalization, two reranker toggles) return the identical baseline triple for (N1, N2, N3); one write-path perturbation (a custom adjudicator instruction) flips N2 to trigger. A five-seed extension confirms the read-path half holds within every seed and the write-path perturbation holds on four of five seeds. A second read-path witness is the top-𝑘 sweep on mem0 v3 at LoCoMo (top𝑘 = 10 versus top𝑘 = 30, 𝑛 = 3 each): the wire verdicts hold at the same baseline triple on both configurations.
27
Ziming Wang
Table 18: Cross-system utility ledger. Paired Δ accuracy of Toki versus four agent-memory systems on the shared LoCoMo slice. The three measured rows are single-conversation slices with paired bootstrap 95% CI; all three intervals cover zero. Six structural abstentions († predicate scope; ‡ compute envelope; § service availability) cover the LongMemEval-S, MultiTQ, and Letta rows. System
𝑛
Toki
Ext.
Δ (95% CI)
mem0 v3 Graphiti Zep
50 50 50
0.02 0.04 0.06
0.06 0.12 0.04
−0.04 [−0.10, +0.00] −0.08 [−0.18, +0.00] +0.02 [−0.06, +0.10]
The mem0 v3 LoCoMo cell carries discordant counts (𝑏, 𝑐 ) = (0, 2) ; the McNemar exact 𝑝 -value floors at 0.50 in this underpowered regime, so the row records no evidence on Δ. Six external pairs abstain on LongMemEval-S and MultiTQ (predicate scope or compute envelope), and Letta abstains across all three datasets (service availability during the measurement window); Appendix D.6 carries the per-row protocol and structural reason.
External measurement-error framing. Messing [48] report that naive 95% confidence-interval coverage drops below nominal as 𝑛 grows on Chatbot Arena while a Total Evaluation Error correction holds coverage at 95% (a benchmark-gaming surface of 32 Elo under the correction versus 56 Elo without). Our protocol pins judge identity, decoder tuple, prompt, and seed before the binary cited-commit witness, so the per-cell verdict carries no continuous score the decomposition would correct; the correction is the natural envelope for any continuous-score aggregate a future revision computes over the 33-cell AnomalyWire family or the 9-cell G2 family.
D.6
Cross-system measurement protocol
The cross-system rows of Table 18 report three measured LoCoMo cells against four imported systems (mem0 v3, Graphiti, Zep, Letta) plus nine structural abstentions. This section records the workload pinning, the configuration deltas, the pre-registration anchors, and the per-row statistical detail compressed in the main-text ledger. Workload pinning. A single pinned language model handles fact extraction, synthesis, and judging across every paired cell; the artefact manifest records the exact model identifier, the temperature, and the maximum output length. Paired Δaccuracy controls for model capability under the same workload. Every row uses top𝑘 = 10 as the retrieval ceiling on the matched-retrieval slice; the configuration-mismatch discussion below names where each imported system departs from this baseline. Per-row measured detail. The three measured rows expand Table 18 with the paired statistic and the per-row note (all at 𝑛 = 50, 2,000 bootstrap resamples). mem0 v3: Δaccuracy = −0.04, 95% question-level paired bootstrap CI [−0.10, +0.00], McNemar exact 𝑝 = 0.50 with 𝑏 + 𝑐 = 2, per-system accuracy Toki 0.02 versus 0.06; the configuration delta is five-axis (hosted client versus local vector index; larger top-𝑘 versus our 10; graph mode enabled versus disabled; a different extractor model identifier versus our pinned synthesiser; a custom adjudicator prompt versus the default), recorded as a five-axis snapshot in the artefact manifest. Graphiti: Δaccuracy = −0.08, CI [−0.18, +0.00], accuracy Toki 0.04 versus 0.12; the extraction-cost ledger records roughly 3.7× more external language-model calls than Toki on the same slice, a cost the algebra-axis attribution proposition (Proposition 6) does not absorb at the extraction boundary. Zep: Δaccuracy = +0.02, CI [−0.06, +0.10], accuracy Toki 0.06 versus 0.04; the imported cell runs against the Zep Cloud service boundary at per-conversation granularity, with trace elapsed-time bands of 0.75 to 1.32 s per reconciled operation reported as service-boundary timing rather than local throughput. Pre-registration anchor and traceability. The cross-system slice is pre-registered against analysis drift. The prospective record fixed the selection rule, random seed, bootstrap trial count, and runner command before any cell in the measurement window completed. The artefact manifest mirrors the same anchors for subsequent windows. Pre-registration sets statistical power at 0.42 for 𝛿 = 0.05 on 𝑛 = 50; effect sizes below 𝛿 = 0.05 sit beneath detection, and the measured |Δ| ≤ 0.08 values land inside that envelope. The Holm step-down family for G2 covers the nine-cell grid (three primary diagonal plus six specificity controls) at 𝛼 = 0.05; the cross-system family is reported separately because the binary cited-commit witnesses of the AnomalyWire layer (G1) and the continuous accuracy estimates of the cross-system layer carry different statistical objects. LongMemEval-S sibling slice. A separately pre-registered LongMemEval-S pilot fixed loader-order rows three through seven before scoring. It reports 𝑛 = 5, Toki 0.40, mem0 v3 0.60, Δ = −0.20, CI [−0.80, +0.40]; the cell is pilot evidence only because 𝑛 = 5 is below the pre-registered power threshold. Proposition 6 classifies this row as retrieval-bound rather than algebra-bound on the needle-in-haystack workload: include-all retrieval against vector-top-𝑘 retrieval is dominated by the retrieval-policy axis when retrieval recall is the bottleneck. No-memory baseline cell. A separately tabled cell pairs Toki against itself with memory disabled (same synthesis boundary and pinned judge, but the disabled side bypasses fact extraction and bitemporal ingest and sees only the most recent 32 turns), at 𝑛 = 50 on LoCoMo under the same synthesiser pin. The cell measures memory-utility rather than memory-availability, since Zhang et al. [81] show the gain is not automatic: their incremental experiments measure 54% solution-loss on previously solved problems once a frontier language-model consolidation step is introduced. WorldDB cousin scope. WorldDB [25] is paper-only at submission; no public artefact supports an imported G2 or G3 runtime cell. The cousin enters our framing analytically. The engine’s stated discipline (Appendix B of [25]) excludes any language-model call on the read path, 28
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
so the deterministic reconciler excludes N1 at the engine layer. The contradicts handler preserves both sides and computes the partition winner at query time, excluding N2 at the engine layer. Content-addressed Merkle ancestry realises the N3 recoverable-provenance property through an alternative schema lift. The G1 verdict for WorldDB-T reads exclude across all three predicates.
E
EXPERIMENT PROTOCOLS AND STATISTICS
This appendix registers one protocol card per experiment. Each card fixes the estimand, the sample construction, the random seed, the bootstrap method, the multiple-testing correction, the raw-output path, the regeneration command, and the explicit boundary between the conclusion the cell licenses and the conclusion it does not. Every number below reads from the released CSV ledgers; the regeneration commands reproduce those ledgers from the same seeds. Seeds follow the project convention of 20260512 for sampling and 20260513 for the bootstrap resampler on the runtime experiments, and 42 on the structural-grid experiments whose schedules are combinatorial rather than sampled from a model.
E.1
G2 utility (3×3 defence-by-benchmark grid)
Protocol. The estimand is a paired accuracy delta per cell. Audit-row cells measure paired_accuracy_delta_audited_current_vs_stale; partition-SR cells measure paired_accuracy_delta_serializable_vs_si_skew; judge-pin cells measure replay_disagreement_delta_pinned_vs_unpinned. The grid pairs three defences against three benchmarks (LoCoMo, LongMemEval-S, MultiTQ), forming a diagonal of three primary cells and six off-diagonal specificity controls. Primary cells run at 𝑛 = 50 trials (LongMemEval-S judge-pin at 𝑛 = 100); off-target controls run at 𝑛 = 10 for the audit-row and partition-SR rows and 𝑛 = 20 for the judge-pin rows. A single pinned judge model handles extraction, synthesis, and adjudication so the paired delta controls for model capability. This single-judge design controls for capability but invites a self-consistency-bias objection, since the adjudicator can agree with its own synthesis; the five-judge cross-judge robustness check bounds the effect for the judge-pin row, and the structural N1 evidence of §E.4 routes through no single judge. The sampling seed is 20260512; the paired bootstrap draws 2,000 resamples for the 95% interval. Significance combines a paired bootstrap CI, a McNemar exact test on the binary-agreement vector, and Holm step-down at 𝛼 = 0.05 over the full nine-cell family. The raw output is results/g2_utility/summary.csv; regenerate with make repro-g2. Allowed conclusion: each defence raises paired accuracy on its matched benchmark and abstains off-target, and the Holm-corrected family controls the nine-cell familywise error at 𝛼 = 0.05. Forbidden conclusion: a per-cell delta does not measure absolute headroom over a no-memory baseline, and the saturated Δ = +1.00 controls reflect the synthetic off-target skew construction rather than a realistic benchmark gap. Joint family-wise robustness across every paired-accuracy test. The nine-cell Holm family above corrects the mechanism-stress grid in isolation. As a stronger sensitivity check, we pool every paired-accuracy null-hypothesis-significance test in the paper into a single confirmatory family of seven and re-correct jointly: the three G2 primary diagonal cells (audit-row × LoCoMo, partition-SR × MultiTQ, judge-pin × LongMemEval-S), the three cross-system cells (mem0 v3, Graphiti, Zep, each × LoCoMo), and the memory-layer ablation on the answerable-factual pool (§4.7, 𝑛 = 1,444). The 33-cell anomaly-wire verdict matrix is a structural 0/1 census with no 𝑝-value, and the §𝐸.4 Bernoulli and oracle-calibration panels are closed-form fits reported by 𝑅 2 , so neither is a significance-testing family and both are excluded with this stated reason. Under joint Holm step-down (family-wise error) and joint Benjamini–Hochberg (false-discovery rate) at 𝛼 = 0.05 over the seven, the three positive confirmatory results survive both corrections (audit-row Holm-adjusted 𝑝 ≈ 1.1 × 10−12 ; partition-SR ≈ 1.1 × 10−14 ; the memory ablation ≈ 3.7 × 10−126 ), while judge-pin (𝑝 = 1.0) and all three cross-system cells (𝑝 ∈ {0.22, 0.50, 1.0}) do not reach significance. The non-significant cells are consistent with the paper’s own framing: judge-pin carries structural rather than benchmark-movement evidence (§𝐸.4), and the cross-system comparison draws no superiority claim. No confirmatory result depends on the choice of correction family. Table 19 expands Figure 2 with the exact per-cell statistics read from the summary ledger. The cross-judge robustness rendered in Figure 7 extends the judge-pin row to five frontier judges and four discriminating bands, isolating the N1 trigger from judge-family paraphrase fragility. The primary diagonal carries the strongest evidence: audit-row on LoCoMo rejects at Holm rank 2 with exact 𝑝 = 2.3 × 10−13 , and partition-SR on MultiTQ rejects at Holm rank 1 with exact 𝑝 = 1.8 × 10−15 . The six off-diagonal controls confirm that each defence abstains on the benchmarks it does not target: the three judge-pin cells return Δ = +0.00 with no discordant pairs and are kept under Holm, while the audit-row and partition-SR off-target cells saturate against a synthetic skew that every cell admits.
E.2
G3 systems performance (five axes)
Protocol. The estimand is per-axis write or query latency, summarised by the median, 𝑝 95 , 𝑝 99 , and the mean with a bootstrap CI. The five axes are memory size, conflict rate, writer concurrency, AS_OF selectivity, and audit retention. Each sweep point runs 30 timed runs after 3 warm-up runs on the DuckDB ours_wire backend. Conflict rate and writer concurrency record per-write samples (𝑛 samples ∈ {1500, 960} per sweep point, from 30 runs of 50 or 32 contradiction-path writes), while memory size, AS_OF selectivity, and audit retention record one timed query per run (𝑛 samples = 30). The judge seed is 20260512 and the bootstrap seed is 20260513, with 2,000 percentile resamples on the mean. There is no multiple-testing family here: G3 reports descriptive scaling and runs no hypothesis-test grid. The raw outputs are 29
Ziming Wang
judge-disagreement rate
1.00
gpt-5.4 claude-haiku-4-5
0.75
gpt-5.4-mini
0.50
claude-sonnet-4-6 0.25 deepseek-v4-flash 0.00 CONTROL
DISTRACTOR
PARAPHRASE
PARTIAL
discriminating band Figure 7: N1 admits across five frontier judges on the PARTIAL band. Disagreement rate by judge × band, 𝑛 = 75 items per band; CONTROL and DISTRACTOR stay replay-stable. PARAPHRASE outliers (DeepSeek 0.99, GPT-5.4 0.67) are judge-family paraphrase fragility, orthogonal to the N1 trigger. Table 19: Detailed G2 utility cells, read from results/g2_utility/summary.csv. The delta column reports the paired estimand and 95% bootstrap interval. McNemar 𝑝 is the exact two-sided value on the binary-agreement vector; (𝑏, 𝑐) are the discordant-pair counts. Holm step-down at 𝛼 = 0.05 covers the full nine-cell family. The off-target audit-row and partition-SR controls run at 𝑛 = 10 and saturate at Δ = +1.00 with CI [1.00, 1.00] and McNemar 𝑝 = 1/29 ≈ 0.00195, the smallest value attainable at this budget. The judge-pin cells tie at Δ = +0.00 on a non-saturating axis. Defence
Dataset
Role
Delta/CI
𝑛
(𝑏, 𝑐 )
Holm
audit-row audit-row audit-row judge-pin judge-pin judge-pin partition-SR partition-SR partition-SR
LoCoMo LongMemEval-S MultiTQ LoCoMo LongMemEval-S MultiTQ LoCoMo LongMemEval-S MultiTQ
prim. ctrl ctrl ctrl prim. ctrl ctrl ctrl prim.
+0.86 [0.76, 0.94] +1.00 [1.00, 1.00] +1.00 [1.00, 1.00] +0.00 [0.00, 0.00] +0.00 [0.00, 0.00] +0.00 [0.00, 0.00] +1.00 [1.00, 1.00] +1.00 [1.00, 1.00] +1.00 [1.00, 1.00]
50 10 10 20 100 20 10 10 50
(43, 0) (10, 0) (10, 0) (0, 0) (0, 0) (0, 0) (10, 0) (10, 0) (50, 0)
reject reject reject keep keep keep reject reject reject
results/g3_systems_perf/scaling.csv (memory size) and results/g3_systems_perf/scaling_*/scaling.csv (the four remaining axes); regenerate with make repro-g3. Allowed conclusion: the bitemporal write path scales sub-linearly in writer concurrency and AS_OF selectivity, decays linearly in conflict rate, and holds 𝑝 99 flat against audit retention. Forbidden conclusion: the 𝑝 99 statistic at 𝑛 samples = 30 is the single maximum of thirty samples rather than a stable tail estimate, so no tail-percentile ranking claim is licensed on the three single-query axes; the mean trajectory is the primary scaling signal. Table 20 reports the per-axis statistical characterisation derived from these sweep ledgers. Spearman 𝜌 (𝑥, 𝜇) ranks the input variable against the mean latency and 𝜌 (𝑥, 𝑝 99 ) against the tail. The log-log power-law fit reports mean ∼ 𝑥 𝛼 when every 𝑥 > 0; the conflict-rate fit is linear because the rate domain spans zero. The coefficient of variation CV averages the within-run dispersion 𝜎/𝜇 over the five sweep points; lower values indicate higher run-to-run reproducibility. Table 20: Per-axis statistical characterisation of the G3 envelope, derived from the five sweep ledgers under results/g3_systems_ perf/. Each row reports rank correlation, scaling-law fit, mean CV across sweep points, and the count of 𝑝 99 non-monotone sweep pairs. Axis
𝜌 (𝑥, 𝜇 )
𝜌 (𝑥, 𝑝 99 )
𝛼
𝑅2
CV
𝑝 99 rev.
memory size conflict rate writer concurrency AS_OF selectivity audit retention
0.80 1.00 1.00 1.00 −0.10
0.90 1.00 0.90 0.90 −0.50
– – 0.86 0.86 –
– – 0.992 0.990 –
0.22 0.43 0.35 0.16 0.04
1 0 1 1 1
30
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
p99 latency
storage amp. (right axis)
(b) Conflict rate ( =
)
) 600
75
latency (ms)
50 25
8 6
400
4 2
1
2
4
8
16
200
0.0
0.2
0.4
read latency (ms)
query latency (ms)
(d) Audit retention ( =
)
100 50 0 0.01
0.05
0.1
0.8
0.5
1.0
conflict rate (fraction)
writer concurrency (threads, log )
(c) As-of selectivity ( =
0.6
1
3
14
2
12
1
0
as-of selectivity (fraction, log)
)
16
10
100
1000
10000
storage amplification (×)
latency (ms)
(a) Writer concurrency ( =
throughput (right axis)
throughput (writes/s)
p50 latency
audit retention (rows, log)
Figure 8: Sub-linear scaling on four workload axes; 30 runs per point after 3 warmups, 95% paired-bootstrap CI. Three cross-axis findings. (F1) Identical sub-linear exponent on two orthogonal axes. Mean latency follows mean ∼ 𝑥 0.86 on both writer concurrency (𝑅 2 = 0.992; 4,846 𝜇s at concurrency 1 to 54,258 𝜇s at 16) and AS_OF selectivity (𝑅 2 = 0.990; 2,373 𝜇s at selectivity 0.01 to 115,975 𝜇s at full), although the two axes exercise distinct DuckDB internals (thread-pool lock acquisition versus period-overlap range scan); the mechanistic decomposition is follow-up work. (F2) Throughput decays linearly in conflict rate. The five-point linear fit gives slope −355.3 writes/sec per unit rate (𝑅 2 = 0.948); throughput drops 584.5 → 218.3 writes/sec from rate 0 to 1 (a 62.7% decline), and the linearity across the full domain shows the per-write dispatcher overhead for the audit-row write is constant. (F3) Audit retention does not load the tail. 𝑝 99 correlates negatively with storage amplification (𝜌 (amp, 𝑝 99 ) = −0.50, mean CV 0.04): a 104 × retention setting (3.00× amplification, 30,000 rows) reads the current-kind partition at 𝑝 99 = 13,093 𝜇s, indistinguishable from the 0× baseline (1.00×) at 14,477 𝜇s. The row-kind discriminator partitions the read scan so the current-kind index never touches audit rows, the structural cost guarantee the calculus pays for the N3 defence. Non-monotone 𝑝 99 disclosure. Four of the five axes show one sweep pair where 𝑝 99 decreases as 𝑥 increases (memory size 103 → 104 : 8.71 → 5.65 ms; writer concurrency 2 → 4: 49.28 → 22.58 ms; AS_OF selectivity 0.01 → 0.05: 10.73 → 8.30 ms; audit retention 10 → 100: 15.95 → 12.36 ms). All four reversal pairs sit where one operand carries a high CV (≥ 0.07) and the mean bootstrap CI already overlaps, consistent with small-sample 𝑝 99 tail variance under cold-start lock or cache effects rather than a mean-monotone violation; the mean stays rank-correlated at 𝜌 ≥ 0.80. PostgreSQL backend pilot. A separately registered PostgreSQL 17.6 backend pilot exercises the writer-concurrency axis under SR isolation at concurrencies {1, 2, 4} with 12 writes per run over 3 runs against one hot partition. It records the serialization-failure count the inprocess ours_wire backend cannot expose: 0 failures at concurrency 1, 18 at concurrency 2, and 25 at concurrency 4. The raw output is results/g3_systems_perf/postgres_backend/scaling.csv; regenerate via the repro-g3 PostgreSQL stanza. Allowed conclusion: a real SR engine aborts the conflicting writers the calculus reasons about. Forbidden conclusion: the three-run pilot does not license a latency comparison against the DuckDB backend, whose process and connection models differ.
E.3
G4 carrier ablation
Protocol. The main-text Table 5 reports the cell rates; G4 ablates two orthogonal axes the algebra exposes. The carrier axis varies the provenance semiring across multilinear N[𝑋,𝑇 ], multi-degree N[𝑋,𝑇 ] # , and the Boolean reduct B. The operator axis turns one mechanism on at a time: audit-row for N3, judge-pin for N1, and (subj, pred)-SR for N2, the 𝐴5𝐵 write-skew specialisation on the (subj, pred) projection. The matched-cell estimand is the defence rate; the carrier-axis estimand is counterfactual token recall (the fraction of audited write identities the carrier recovers). The runner sweeps each cell across 100 seeded runs with seed base 20260512; the operator-ablation companion records 50 trials per cell at noise rate 0.05. Bootstrap CIs use seed 20260513 with 2,000 resamples. There is no multiple-testing family: G4 reports per-cell rates against a fixed 0.00/1.00 structural prediction rather than a hypothesis-test grid. The raw outputs are results/g4_ ablation/operator_ablation/results.csv (operator diagonal) and results/g4_ablation/k_semiring/counterfactual.csv (carrier recall); regenerate with make repro-g4. Allowed conclusion: anomaly soundness is carrier-invariant for verdicts (every matched cell defends at 1.00, every off-target cell at 0.00), while audit-time token recall separates the carriers. Forbidden conclusion: the Boolean reduct’s 0.00 recall is not a verdict failure; it preserves existence and fails only the concrete-write-identity query that the token-retaining carriers answer. 31
Ziming Wang
The operator-ablation diagonal (Table 21) confirms that each operator peaks on the anomaly it targets: await_confirm reaches 0.94 on N1, evidence reaches 0.88 on N2, and per_rule reaches 0.98 on N3, against a last-writer-wins floor that never exceeds 0.24. Table 21: G4 operator-ablation diagonal, read from results/g4_ablation/operator_ablation/results.csv. Accuracy and 95% bootstrap CI over 50 seeded trials per cell at noise rate 0.05. The diagonal cell (the operator matched to its target anomaly) is marked ★. Operator lww evidence await_confirm per_rule
N1
N2
N3
0.08 [0.02, 0.16] 0.46 [0.32, 0.60] 0.94 [0.86, 1.00] ★ 0.62 [0.48, 0.76]
0.24 [0.14, 0.36] 0.88 [0.78, 0.96] ★ 0.40 [0.26, 0.54] 0.52 [0.38, 0.66]
0.08 [0.02, 0.16] 0.60 [0.44, 0.74] 0.64 [0.50, 0.76] 0.98 [0.94, 1.00] ★
Table 22 reports the matched 3×3 carrier-by-defence grid alongside the off-target specificity rate, the audit-polynomial size, and the counterfactual recall. Every matched cell defends at 1.00 across all three carriers; the off-target companion records 0.00. Verdict is carrierinvariant. Token recall separates the carriers: N[𝑋,𝑇 ] and N[𝑋,𝑇 ] # recover every audited write identity (𝑛 recoverable = 375 of 375 for multi-degree; 106 of 375 recoverable for multilinear at the bridged accuracy 0.683), while B preserves only existence (0 of 375, recall 0.00). Table 22: G4 carrier ablation, read from results/g4_ablation/k_semiring/counterfactual.csv (recall) and the operator-ablation match/off-target ledger. Match and off-target columns report defence rates against the structural prediction; the provenance-size column reports 𝜇 ± 𝜎 over the audit polynomial; recall is the counterfactual token-recovery accuracy. Carrier
Defence
N[𝑋 ,𝑇 ] N[𝑋 ,𝑇 ] N[𝑋 ,𝑇 ] N[𝑋 ,𝑇 ] # N[𝑋 ,𝑇 ] # N[𝑋 ,𝑇 ] # B B B
audit-row judge-pin partition-SR audit-row judge-pin partition-SR audit-row judge-pin partition-SR
Target
Match
Off
|prov|
Recall
N3 N1 N2 N3 N1 N2 N3 N1 N2
1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00
0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00
4.00 ± 1.42 1.00 ± 0.00 4.00 ± 1.42 4.00 ± 1.42 1.00 ± 0.00 4.00 ± 1.42 1.00 ± 0.00 1.00 ± 0.00 1.00 ± 0.00
1.00 1.00 1.00 1.00 1.00 1.00 0.00 0.00 0.00
The counterfactual ledger sharpens the carrier contrast. The multi-degree carrier N[𝑋,𝑇 ] # recovers all 375 recoverable write identities at recall 1.00 with zero seed variance; the multilinear carrier N[𝑋,𝑇 ] recovers 106 at bridged accuracy 0.683 (95% CI roughly [0.65, 0.71]); the Boolean reduct recovers 0 at accuracy 0.345, the existence-only floor. Anomaly soundness is carrier-parametric for verdicts, and audit queries that must name concrete write events need a token-retaining carrier, which is the operational work G3 charges separately.
E.4
G5 structural grids
The G5 grids are exhaustive structural sweeps rather than sampled estimators: each cell enumerates adversarial schedules against a typed prediction and counts admits. The estimand is the per-cell admit rate; the structural prediction is binary (0.00 when the guard dominates the isolation level, 1.00 when it does not, modulo a small schedule noise floor 𝜖 on the composition grid). The shared seed is 42; per-cell seeds offset by a stable hash of the cell key. No bootstrap and no multiple-testing family apply, because the prediction is exact and the admit rate is a census over enumerated schedules. The main-text Figure 4 anchors these grids visually. Table 23 reports the dimensions, the observed boundary against the prediction, the raw output, and the regeneration command for each grid; each command writes under results/<name>/run_*/. The per-grid conclusion boundaries: the iso-matrix, schema-axis, and N2 grids license that the typed guard surface admits exactly the schedules the lattice predicts (the (subj, pred)-SR specialisation is the unique level eliminating N2 across every partition size and contention level), but the 0.00/1.00 rates are an exact census, not a probability, and the RC/SI partial-contention rates below 1.00 follow from the schedule construction and do not measure a defence. The T5 grid licenses the lattice-supremum prediction under composition up to five operators, but the 𝜖 = 0.02 admit floor on dominating cells is a modeled schedule-noise term, not a measured guard leakage. The oracle-variance grid licenses that the boundedly-nondeterministic flip rate predicts the N1 admit rate to within 0.10 on 29 of 30 cells, but the single cell at error 0.1114 does not falsify the prediction at 50 votes. The lemma-bridge grid is empirical support for the bridge lemma, not a proof; the proof is in Appendix B.1.
E.5
Cross-system slice
Protocol. The cross-system slice tests Theorem 5’s prediction that every H1-non-compliant system sharing one boundedly-nondeterministic oracle admits N1 at the same Bernoulli rate. The estimand is the per-pair difference in N1 admit rate between two systems; the statistic is a Welch two-sample 𝑡 on the per-seed admit rates of the five H1-non-compliant variants (Toki-stripped, mem0-v3-like, Graphiti-like, 32
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
Table 23: G5 structural-grid census. Each grid enumerates schedules per cell at seed 42 and observes an exact 0.00/1.00 admit boundary (the composition grid carries a modeled 𝜖 = 0.02 noise floor on dominating cells). The observed column matches the typed prediction exactly; the rates are a census over the enumerated family and carry no sampling error. Grid
Dimensions
Observed vs. prediction
Raw output / regen command
Iso-matrix (T-01, Cor. 1–2)
9 predicates × 6 iso levels (RC/SI/SR ±cb) = 54 cells, 100 sched/cell, 𝜖 = 0.0 6 iso levels × {base, audit-row} = 12 cells, 100 sched/cell 3 iso levels × 4 partition sizes {2, 4, 8, 16} × 3 contention {0.5, 0.75, 1.0} = 36 cells, 200 sched/cell 1364 pipelines up to length 5 × 6 iso levels = 8184 cells, 50 sched/cell, 𝜖 = 0.02
32 dominating admit 0.00, 22 under admit 1.00; exact match
results/iso_matrix/run_v1/iso_matrix_grid.csv; python -m experiments.iso_matrix.runner
base 1.00 on all 6; audit-row 0.00 on all 6
results/schema_axis/run_v1/schema_grid.csv; python -m experiments.schema_axis.runner results/n2_partition/run_v1/n2_grid.csv; python -m experiments.n2_partition.runner
Schema axis (T-01b) N2 partition (Cor. 2)
T5 composition (T-05)
Oracle variance (T-06)
30 cells (5 systems × 6 seed cells, 50 votes each) vs. 2𝑝 (1 − 𝑝 )
Lemma bridge (Lemma 1)
1000 trials at schedule length 12; checks keyed-log alphabet, edge set, N1-on-P2 iff
RC 0.7496, SI 0.7462 (to 1.00 at full contention); SR 0.00 on all 12; half-contention near 0.5 (RC size 2: 104/200 = 0.52)
2219 dominating admit 0.0904 (𝜖 floor), 5965 results/t5_composition/run_length5/ under admit 1.00; length- ≤ 3 exact run run_v1: composition_grid.csv; python -m 84 pipelines, 0/193 dominating, 311/311 under experiments.t5_composition.runner –max-length 5 mean abs. error 0.0166, max 0.1114, 96.67% results/oracle_variance/run_v1/calibration. (29/30) within 0.10 csv; python -m experiments.oracle_variance.analyze (consumes results/n1_empirical/run_v1/trials.jsonl) all three pass rates 1.00; every trial results/lemma_bridge/run_v1/bridge_ key-multiplicity preserved verification.csv; python -m experiments.lemma_bridge.runner
Letta-like, Zep-like), evaluated over 5 seeds per system. The four pairwise tests pin Toki-stripped against each imported mimic. The raw output is results/cross_system_n1/run_v1/cross_system_test.csv; regenerate with python scripts/cross_system_n1_test.py –output results/cross_system_n1/run_v1/cross_system_test.csv (the script reads results/n1_empirical/run_v1/state). The four measured pairs all return |𝑡 | < 2: mem0-v3-like Δrate = 0.0286, 𝑡 = 0.19, df = 7.41; Graphiti-like Δrate = 0.00, 𝑡 = 0.00, df = 7.65 (identical mean admit rate 0.1959); Letta-like Δrate = 0.0082, 𝑡 = −0.05, df = 7.99; Zep-like Δrate = 0.0122, 𝑡 = 0.08, df = 7.39. The maximum absolute mean difference across the four pairs is 0.0286 and the maximum |𝑡 | is 0.19. Allowed conclusion: at the |𝑡 | < 2 sanity threshold the four imported mimics are statistically indistinguishable from Toki-stripped on the N1 admit rate, consistent with the shared-oracle prediction. Forbidden conclusion: with 5 seeds per system the Welch test is underpowered for tiny effect sizes, so a high 𝑝-value does not positively confirm distributional identity; the slice serves as a sanity check against the bounded-oracle prediction and stops short of a formal equivalence proof, and it carries no bootstrap CI or power figure in the released ledger.
E.6
Multi-writer concurrency: the operator-to-isolation mapping under real contention
Protocol. This card upgrades the single-process cost pilot (§4.3) to a measured concurrency result. A multi-writer experiment runs the lost-update anomaly 𝑃4 on PostgreSQL 17.10 with writer count 𝑤 ∈ {1, 2, 4, 8, 16} crossed with the three isolation levels read committed, repeatable read, and serializable, 30 runs per cell. The estimand per cell is the anomaly admit rate (the fraction of runs in which a concurrent writer overwrites another’s committed value without aborting) and the serialization-failure rate (the fraction of writers the backend aborts). The raw output is results/g3_systems_perf/isolation_concurrency.csv (15 cells); regenerate with python experiments/g3_systems_perf/isolation_concurrency.py. Result. Table 24 records the grid. At one writer no cell admits the anomaly. At every multi-writer cell read committed admits the lost update at rate 1.00, while repeatable read and serializable exclude it at rate 0.00 by aborting the losing writer. The serialization-failure rate the two stronger levels pay tracks (𝑤 − 1)/𝑤 exactly: 0.50 at two writers, 0.75 at four, 0.875 at eight, 0.9375 at sixteen. Read committed pays no abort and reaches the highest commit throughput, the throughput cost the exclusion guarantee charges. The mapping the algebra assigns each operator is therefore operationally enforced at the SQL layer, not only stated as a typing precondition. The full lattice. Three companion experiments extend the grid from 𝑃 4 to the rest of the iso-axis lattice on the same PostgreSQL 17.10 backend, 30 runs per cell. Read skew (𝐴5𝐴) runs one reader whose two correlated reads straddle a concurrent mirror update: read committed admits the torn read at rate 1.00, while snapshot isolation and serializable exclude it at 0.00. Write skew (𝐴5𝐵) runs two writers that read both equal-weight competitors and promote disjoint rows: read committed and repeatable read both admit the skew at 1.00, and serializable alone excludes it, aborting one writer at rate 0.50. The phantom (𝑃3 ) runs two writers that scan a cardinality predicate and each insert a primary row: read committed and repeatable read admit it at 1.00, serializable excludes it at 0.00. The 𝐴5𝐵 and 𝑃3 cells separate repeatable read from serializable, the boundary the Evidence and Per-Rule operators assume. Figure 9 plots the full grid, and raw output sits in results/g3_systems_perf/read_skew_a5a.csv, results/g3_systems_perf/write_skew_a5b.csv, and results/g3_systems_perf/phantom_p3.csv.
33
Ziming Wang
Table 24: Multi-writer lost-update (𝑃4 ) admit rate, serialization-failure rate, and commit throughput on PostgreSQL 17.10, 30 runs per cell. Read committed (RC) admits the anomaly at every multi-writer cell; repeatable read (RR) and serializable (SR) exclude it by aborting the losing writer at rate (𝑤−1)/𝑤. Source: results/g3_systems_perf/isolation_concurrency.csv. Writers
Level
Admit
Ser. fail
Throughput (commits/s)
1 1 1
RC RR SR
0.00 0.00 0.00
0.00 0.00 0.00
6.76 7.13 7.23
2 2 2
RC RR SR
1.00 0.00 0.00
0.00 0.50 0.50
13.92 6.99 7.02
4 4 4
RC RR SR
1.00 0.00 0.00
0.00 0.75 0.75
26.26 6.72 6.68
8 8 8
RC RR SR
1.00 0.00 0.00
0.00 0.875 0.875
42.07 5.03 5.16
16 16 16
RC RR SR
1.00 0.00 0.00
0.00 0.9375 0.9375
44.81 3.07 3.05
Read Committed
Snapshot (RR)
Serializable (SSI)
P4 lost update
admit
exclude
exclude
1.00
0.00
0.00
A5A read skew
admit
exclude
exclude
1.00
0.00
0.00
A5B write skew
admit
admit
exclude
1.00
1.00
0.00
P3 phantom
admit
admit
exclude
1.00
1.00
0.00
anomaly admitted
anomaly excluded
Figure 9: The operator-to-isolation mapping is the Berenson–Adya anomaly lattice. Admit rate of each write-time anomaly at each PostgreSQL isolation level, over 30 two-writer runs on PostgreSQL 17.10. Read committed admits all four anomalies, snapshot isolation (repeatable read) excludes lost update and read skew, and only serializable also excludes write skew and the phantom. The two-step staircase is the empirical form of Table 3, and the figure is generated from the same CSVs by scripts/plot_isolation_lattice.py. Scope. The experiment is single-node on one PostgreSQL instance, so it bounds the operator-to-isolation correspondence under real intra-node contention and makes no distributed-deployment claim.
E.7
N-ary conflict-set confluence grid
Protocol. This card anchors Proposition 2. The grid resolves a conflict set of 𝑛 pairwise-contradicting facts under the two fold operators (last-writer-wins and evidence-weighted merge) for 𝑛 ∈ {2, 3, 4, 5, 6, 7, 8}, and for each 𝑛 enumerates the permutations of the set. The two
34
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
checked properties are confluence (the winner identity and the merged provenance are identical across every permutation) and provenancecompleteness (the emitted audit row’s merged provenance dominates every member under the K-semiring natural order). The grid is exercised by tests/bitemporal/test_conflict_set.py; regenerate with python -m pytest tests/bitemporal/test_conflict_set.py. Result. Across the grid every permutation of each 𝑛-member set returns the identical winner and the identical merged provenance, and the audit row’s merged provenance dominates all 𝑛 members under ⪯𝐾 . The await-confirmation and per-rule operators resolve the set by direct selection. The judge-logged dispatcher elects one member by oracle, records the winner’s stable identity under an order-independent set key, and replays it by identity after a crash, exercised by tests/bitemporal/test_judge_log_persistence.py.
F
ARTIFACT REPRODUCIBILITY RUNBOOK
This runbook satisfies the four PVLDB reproducibility surfaces: the white-box prototype with its source, configuration, and build environment; the input data and its generation process; the experiment configuration and workload that produces raw data; and the scripts that turn raw data into the paper’s figures and tables. An independent team that follows the command catalogue below recreates similar behavior for every numeric claim in the main text and for every cell of the G1 verdict matrix in Table 4. The claim-to-evidence map of Table 6 binds each claim to the runner, seed, and pinned commit that anchor it.
F.1
Build environment
The reference implementation is a white-box prototype: source, configuration, and a containerized build environment ship together. The Python package declares requires-python=">=3.11"; the reviewer Dockerfile pins python:3.12-slim-bookworm and resolves every dependency from the committed uv.lock, so a fresh build reproduces the exact wheel set rather than a floating range. The bitemporal core uses DuckDB under the >=1.0,<2 constraint, resolved by the lockfile to the date-versioned 2026.4.22 build. The host platform is macOS 15 on Apple Silicon for the DuckDB latency envelope; the PostgreSQL pilot runs PostgreSQL 17.6 under SERIALIZABLE isolation in a containerized postgres:17 instance on the same host, and the runner records the exact server_version alongside each row so the version is auditable from the raw CSV. Two commands establish the environment. make install installs the bitemporal package in editable mode plus fal-client, pytest, and pyyaml, then runs the reference-sync script. make sync-locked performs the lock-step install through uv sync with the test and experiments extras, which is the path the reviewer Dockerfile follows. make tests runs the full pytest suite under real-dependency TDD and needs no network.
F.2
The command catalogue
Every runnable surface routes through one Makefile. Table 25 states what each target produces, whether it needs the network, and the runtime order of magnitude where known. Only the repro-g2 live-LLM path (next subsection) needs the network beyond the optional DOI resolution in make refs; the cross-system ledger reuses the same live judge.
F.3
Deterministic judge versus live LLM
The language-model channel splits cleanly. Every experiment except the G2 utility slice uses a deterministic judge stub that needs no network. The stub seeds at 20,260,512 and votes by hashing the prompt: it returns a choice or an integer from the first eight bytes of SHA-256 of seed::prompt, so the same prompt under the same seed always yields the same vote and the wire adapter’s output is byte-reproducible. This is the judge behind make repro-anomaly-wire, make repro-claim, and the AnomalyBench runner. The G2 utility slice (make repro-g2) is the single live-LLM experiment. It calls an OpenRouter-compatible chat-completions endpoint through a strict-binary judge. The judge reads its API key from the first set environment variable among the family-specific VLDB2027_<FAMILY>_API_KEY, then VLDB2027_JUDGE_API_KEY, OPENROUTER_API_KEY, and OPENAI_API_KEY; or, when invoked from a config file, from the ignored local file at artefact/credentials/openrouter.local.json (the committed openrouter.example.json shows the schema). Each call runs at temperature zero and the judge records the prompt hash and the output hash as SHA-256 digests on every JudgeResult, so a reviewer audits the live path without re-issuing it: the judge trace hash pins each scored question to the exact prompt and response that produced its binary verdict. The deterministic judge needs no such audit because it carries no network nondeterminism by construction. The G2 prerequisite gate is explicit and fails closed. The target checks for the judge config (G2_JUDGE_CONFIG, default artefact/credentials/openrouter.local.json), the three trace directories (G2_LOCOMO_DIR, G2_LONGMEMEVAL_S_DIR, G2_MULTITQ_DIR), the judge replay table (G2_JUDGE_REPLAY_TABLE), and the LoCoMo and MultiTQ partition traces, exiting with a diagnostic when any is absent rather than running against a half-populated input. The order of magnitude is tens of minutes for the default example count, dominated by the per-question round trips to the provider.
F.4
Data provenance
The input data has two origins. The bitemporal-core and wire-level experiments generate their inputs deterministically from a pinned seed; no external download is required, which is why the wire sweep reproduces under –seed 20260512 alone. The G2 utility slice consumes the 35
Ziming Wang
Table 25: Makefile target catalogue. Net? marks the network requirement; runtime is the order of magnitude. Target
Produces
Net?
Runtime
make paper make figures make refs make smoke
src/main.pdf via latexmk -xelatex the five matplotlib figure PDFs (TikZ renders through paper) verifies every references/refs.bib entry resolves to a DOI or arXiv id fitness/surface/visual gates, supplement, benchmark PRD, bitemporal core tests, Appendix B.8 composition coverage, AnomalyBench runner (CSV under results/anomaly_bench/) smoke then the five reproduction sub-targets in series (non-parallel) provenance suite (tests/bitemporal/test_provenance.py) + full AnomalyBench runner composition coverage in tests/integration/test_compose.py AnomalyWire adapter sweep across all workloads at –seed 20260512, regenerating the wire rows of Table 4 G3 sweep (100 runs after 3 warmups, bootstrap seed 20,260,513), PostgreSQL pilot at concurrencies 1,2,4, Zep service-boundary timing; longest target (one SERIALIZABLE session per writer) carrier-by-defence ablation, 100 seeded runs from seed base 20,260,512 with off-diagonal cells, anchoring Theorem 3 utility slice of §4.2 against LoCoMo/LongMemEval-S/MultiTQ, 2,000 bootstrap trials at seed 20,260,512; gates on the next-subsection prerequisites cross-system slice of §4.6 in sweep mode at 50 examples, 2,000 trials, seed 20,260,512, same live judge; three LoCoMo cells + nine abstentions ship under results/g2_utility/cross_system/ with one paired-judge trace per cell (offline-readable per §D.6) chains figures, experiments, tests, refs, paper, and the four paper-quality gates both AnomalyBench and AnomalyWire runners over all workloads then the matching test suites experiments/<name>/run.sh per registered experiment (anomaly groups drive through make anomaly / repro-anomaly-wire) remove build artifacts; distclean also clears results/ for a from-scratch reproduction
no no opt. no
seconds seconds seconds minutes
no no
tens of min–hours minutes
no no
minutes minutes
no
tens of min
no
minutes
yes
tens of min
yes
tens of min
opt. no
hours minutes
no
varies
no
seconds
make repro-full make repro-claim make repro-compose make repro-anomaly-wire make repro-g3
make repro-g4 make repro-g2 experiments.g2_utility.cross_ system_runner
make all make anomaly make experiments make clean / distclean
LoCoMo, LongMemEval-S, and MultiTQ traces, supplied through the directory variables of the prerequisite gate and replayed against the recorded partition traces and judge replay table. The AnomalyWire imported adapters pin each upstream system to an exact commit (the full revisions are in the pinned-commit manifest, Table 15), and the runner verifies the clone is on the pinned revision before running, raising rather than running against a drifted source. mem0 (v2 and v3), Graphiti, Letta, the Zep self-hosted clone, and the WorldDB arXiv revision were all verified 2026-05-10; the hosted Zep Cloud boundary (zep-cloud-api-v2-2026-05-13) was verified 2026-05-13; and Toki pins to this repository at its artifact-release tag. The human-readable counterpart lives in references/repos/INVENTORY.md and references/manifest.json.
F.5
Archival plan
The reference implementation, data, and reproducibility artifact are publicly available at the repository linked on the first page. A versionfrozen, citable archive (a Zenodo deposit minting a DOI) is planned and will be cut on publication; that DOI does not yet exist. Both the AnomalyClaim verdict CSVs under results/anomaly_bench/ and the AnomalyWire runtime CSVs under results/anomaly_wire/ ship pre-computed; every populated verdict in the matrix is reproduced exactly by the adapter sweep, and the cross-layer audit surfaces a single design-path-to-runtime divergence (the mem0 v3 imported N2 cell). The Zep imported row ships its cached Zep Cloud trace (zep_imported_run.json from a one-time live write, replayable offline); the Letta imported row regenerates against a managed Docker Postgres container or a VLDB2027_LETTA_PG_URI endpoint. The G5-anchor CSVs are shipped: the four inputs to the G5-anchor figure (the isolation-matrix grid, the length-five composition grid, the oracle-variance calibration, and the cross-system N1 table) are committed under results/, so the anchor figure rebuilds without re-running the underlying sweeps. The artifact carries a reviewer Dockerfile (artefact/Dockerfile), a seed manifest (artefact/seed.json), and artefact/REPRODUCE.md as the entry-point document for an independent team.
F.6
Per-claim map
The claim-to-evidence map of Table 6 (Appendix A) binds each main-text claim to its evidence object, reproduce token, and strongest valid conclusion; the artifact manifest carries a programmatic counterpart whose keys mirror the map rows and whose values record the claim, evidence object, runner, seed, and pinned commit. The reproduce token for each evidence group is the matching make target of Table 25; every target except repro-g2 runs offline against the deterministic judge, so an independent team recreates the structural verdicts before configuring a single live provider key for the utility slice.
36
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
G
NEGATIVE RESULTS AND SCOPE LIMITS
This appendix states the boundary of every claim as a positive scope statement. The structure separates three concerns: the measurements that carry controlled-grid rather than natural-workload evidence (§G.1–§G.3), the formal results whose hypotheses fix their reach (§G.4–§G.6), the open problems the calculus exposes (§G.7), and the wire imports and benchmark integrations deferred under the scoping caps (§G.8, §G.9). A reviewer reads this appendix to confirm the contribution survives a hostile re-read: each limit names what holds, on what surface, and on what terms a follow-on revision closes it. The main-text limitations paragraph (§6) summarises these boundaries; the detail lives here.
G.1
G2 off-target controls measure mechanism stress under saturating perturbation
The G2 grid is a mechanism-stress instrument (§4.2, Figure 2). The constructed perturbations saturate off-target controls by design: the auditrow defence moves its primary LoCoMo slice by Δ = +0.86 (paired-bootstrap CI [0.76, 0.94]), and that single cell carries natural-workload movement, while both audit-row off-target controls, both partition-SR controls, and the partition-SR primary MultiTQ cell all saturate at +1.00 under their constructed slices. The saturation is evidence that the perturbation stresses the intended mechanism to its ceiling, and the grid reports exactly that. The grid scopes below a specificity claim: a specificity grid would require off-target controls that stay flat while the on-target cell moves, and the constructed slices here do not provide that separation. The judge-pin defence records no movement on this surface because its replay-disagreement estimand requires a judge replay table absent from this grid. The load-bearing G2 evidence is therefore the audit-row +0.86 natural-workload cell, and it stays below an end-to-end utility-superiority claim.
G.2
G3 SERIALIZABLE saturation is disclosed honestly under concurrency
The G3 cost envelope is a single-process measurement against the DuckDB reference backend, where writer concurrency fits 𝜇 ∼ 𝑐 0.86 at 𝑅 2 = 0.992, a sub-linear lock-contention signature (§4.3). A transactional-backend pilot against PostgreSQL 17.6 under SERIALIZABLE isolation discloses the saturation point directly: of 36 attempted writes (twelve writes per run across three runs), 18 commit at writer concurrency two and 11 commit at concurrency four, with the remaining writes returning serialization failures the backend raises by construction. The in-memory envelope is the load-bearing systems claim; the PostgreSQL pilot establishes that the same operators implemented at the SQL layer expose the contention honestly rather than masking it. The envelope holds for single-process deployments, and the distributed-deployment question stays open (§G.5).
G.3
Cross-system utility is reported as transparency, with intervals covering zero
The cross-system ledger pairs Toki against four imported agent-memory systems on a shared LoCoMo slice under a pinned synthesiser and judge (§4.6, Table 18). All three measured confidence intervals cover zero: mem0 v3 records Δ = −0.04 with CI [−0.10, +0.00], Graphiti records −0.08 with CI [−0.18, +0.00], and Zep records +0.02 with CI [−0.06, +0.10]. The pre-registered statistical power is 0.42 for a 𝛿 = 0.05 effect at 𝑛 = 50, so the slice is powered to report distributional equivalence rather than to detect a small superiority margin. The paper draws a transparency conclusion from these rows: the contract delivers write-time correctness, and the measured downstream utility is statistically indistinguishable from the baselines at this scale. The companion N1-anchor pairing in results/cross_system_n1/run_v1/cross_system_test.csv records the same equivalence on the keyed-log estimand, with the stripped reference against the four baselines returning a maximum |𝑡 | = 0.19 (mem0 v3-like) across the four Welch tests at five seeds per arm, rejecting no superiority null. A larger powered cross-system study is a follow-on axis (§G.9).
G.4
The N1 lower bound holds for boundedly nondeterministic oracles
The N1 lower bound (Theorem 5) characterises N1 exclusion for boundedly nondeterministic judge oracles: a frontier language model at a sampling temperature whose reasoning prefix engages the sampling rng, where the admit rate matches the closed form 2𝑝 (1 − 𝑝). The bound applies within that hypothesis class. Deterministic oracles fall outside the hypothesis because a deterministic judge admits no replay disagreement to bound, so the 2𝑝 (1 − 𝑝) form is vacuous for them. Engine-layer reconcilers such as WorldDB also fall outside the hypothesis: WorldDB realises deterministic reconciliation at the engine layer, so N1 does not apply to its write path and the lower bound makes no claim about it. The bound is therefore tight on the relational schedule model with a boundedly nondeterministic oracle, and silent on the two adjacent regimes.
G.5
The single-process envelope makes no distributed-deployment claim
The systems envelope is measured and stated for single-process deployments (§4.3). The 𝑐 0.86 writer-concurrency fit and the memory-size, conflict-rate, retrieval-selectivity, and audit-retention axes all charge the local reference stack on one process. A distributed deployment introduces a provenance-aware quorum question that the present envelope does not address: whether a provenance-aware Byzantine quorum can replace SI with a stronger level implementable in Θ(log 𝑛) writes without routing every read through SR on the whole fact table remains open (§G.7). The contribution scopes to the single-process correctness contract, and the distributed scalability result is future work.
37
Ziming Wang
G.6
The N1 defence holds at intra-deployment replay granularity
The N1 defence (Corollary 2) holds at intra-deployment replay granularity for a fixed decoder tuple: within one deployment, replaying the keyed judge log over the same decoder tuple reproduces the recorded verdict. Cross-deployment model upgrades and judge-prompt drift sit outside the isolation lattice because they change the decoder tuple itself, and the lattice levels are defined over a fixed tuple. The judge-prompt sensitivity lemma bounds the cross-deployment divergence that those upgrades and drift induce, so the boundary is quantified rather than merely flagged. The isolation lattice governs write-time scheduling for a fixed oracle configuration, and the judge-prompt sensitivity lemma governs the behavior across configuration changes.
G.7
Open Problems
The calculus opens eight problems. Each names what holds today and the open question that would close it. Confidence-aware bitemporal indexing. A four-dimensional access path ranking rows by conf within the (subj, pred) partition at any (Tv, Ts ) slice would let ⊕p skip the snapshot read without admitting N2 under SR. Open: does such an index exist with sub-linear maintenance under SI commits when confidence and period revisions are non-independent? BeliefShift [51] and Memora [70] measure the downstream N2 symptom on natural workloads. Cross-modal bitemporal extensions. Image- and audio-typed facts about the same (subj, pred) require a deterministic similarity predicate for the four operators to preserve their isolation signatures. Open: which similarity predicates over embedding spaces admit such an operator closed under composition with Allen’s thirteen relations [3]? Distributed bitemporal and adaptive keys. Adversarial writers (prompt injection, tool-output hallucination) violate the SI read invariant by construction, and fixed (subj, pred) keys cover only the evaluated operator while stale-premise, relation-poisoning, and cascade-repair workloads stress broader dependency regions [15, 44]. Open: can a provenance-aware Byzantine quorum replace SI with a stronger level implementable in Θ(log 𝑛) writes without routing every read through SR on the whole fact table, and can a substrate refine isolation keys from repair cascades while preserving serializable writes per exposed key? GDPR-preserving time-travel. GDPR Article 17 erasure and Article 5 trace retention pull in opposite directions. Open: which carrier 𝐾 admits quotienting W by user-bound write tokens while keeping a typed erasure operator ⊕⊥ composable with the four existing operators? Compression-utility axis. Zou et al. [86] cast agent memory as a decision-centric rate-distortion problem with a near-minimax-regret forgetting boundary (orthogonal to ours: DeMem owns what compresses safely under a decision-relevance loss, the algebra owns which schedules avoid N1/N2/N3 under named isolation), and Zhang et al. [83] unify memory, skills, and rules on one compression spectrum (5–20× episodic, 50–500× procedural, 1,000×+ declarative), reporting a cross-community citation rate below 1% across 1,136 references in 22 primary papers and a “missing diagonal” where no shipped system supports adaptive cross-level compression. Open: does a DeMem forgetting boundary composed with the four operators preserve SR on the surviving (subj, pred) partition (or does a confidence-weighted carrier 𝐾 [𝑋,𝑇 ] become load-bearing), and does the dual-row signature Fact × Fact → (Fact, Audit) lift to a tier-indexed Fact × Fact → (Tier, Audit) that types the missing diagonal so an audit row witnesses every episodic-to-skill-or-rule promotion and extends Theorem 2’s N3 defence to compression-induced erasure across tiers? Argumentation-driven retrieval. Sadowski and Chudziak [61] surface parallel goal-conditioned perspectives at read time using Dung argumentation semantics over an attack graph of conflicting items, complementary on the resolve-versus-surface dimension. Open: does a fifth operator ⊕s typed at the schedule layer deferring to Dung’s preferred-extension semantics compose with ⊕t , ⊕p , ⊕? , ⊕c under SR, lifting the runtime mechanism into the type theory? Neuro-symbolic conflict detection. Xie and Du [77] translate clinical-guideline rules into SAT clauses to detect local and global conflicts at retrieval time (their pipeline owns detection, the calculus owns typed resolution). Open: can the audit row of Theorem 2 act as the lineage proof for a downstream SAT-encoded explanation of a chosen local-conflict resolution, making the typed witness consumable by a logic-level reasoner? Threat-model integration with deployment governance. The algebra formalizes write-time correctness for well-formed writes from registered principals; adversarial injection through the normal memory-update path is the orthogonal threat surface. Sleeper Memory Poisoning [57] scales the gap: on six frontier models in the external memory-manager regime our implementation occupies, no evaluated defence drives injection to zero and goal-adjacent adversarial usage reaches 60–89% of subsequent retrievals. A complete deployment composes three layers: proof-derived authorisation above the agent action gate (Verifiable Agentic Infrastructure [33]); our audit-row schema below, making every resolution event durable; and MemLineage’s [52] cryptographic lineage threaded through the schema’s W column to bind the two (it blocks sensitive-action dispatches with derived-untrusted ancestry). Open: does the 𝐾-relation carrier map into MemLineage’s maxof-strong-edges trust lattice so the audit row’s 𝑝 w ⊕ 𝑝 l annotation simultaneously satisfies Theorem 2’s ⪯𝐾 comparison and MemLineage’s untrusted-path persistence, and does a fifth ⊕d operator typed at SI with a detection-oracle callback slot into the lattice join without weakening the four operators’ isolation signatures? 38
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
G.8
Deferred Wire Imports and Benchmark Integrations
A 2026-04 to 2026-05 frontier-landscape survey surfaced five candidate extensions to the AnomalyWire layer of §4: three open-source agent-memory projects under active development and two new external benchmarks. We assessed each under the per-extension working-day caps adopted for scoping discipline (three days per wire import, two to three days per benchmark integration). All five exceeded the cap. The cap-and-convert outcomes appear below so a reader can audit which extensions we considered, why they did not land, and on what terms a follow-on revision can complete them. Table 26 records six of the seven, each with the structural blocker that exceeds the cap and the predicate it would map to; the Graphiti-Neo4j scope-out, which carries its own measurement detail, follows the table. Table 26: Deferred wire imports and benchmark integrations. Each exceeded the per-extension cap (three working days per wire, two to three per benchmark) for the named blocker. “Maps to” names the predicate the extension would test. Extension
Type
Blocker (estimated effort)
Maps to
AgentMemory [28]
wire (TS)
N1/N2/N3
Supermemory [63]
wire (TS)
TencentDB-AgentMemory [68]
wire (TS)
HaluMem [16]
benchmark
STALE [15]
benchmark
GroupMemBench [78]
benchmark
first-class contradicts/supersedes/extends/derives/related relation kinds plus by-convention audit; Node subprocess + REST, so wiring needs a cross-language sidecar and an HTTP shim for the deterministic-judge stub to intercept the write-time call site (5–7 days > 3-day cap) MIT-licensed, claims top LongMemEval/LoCoMo/ConvoMem; every operation is an outbound round-trip to a paid managed cloud endpoint with no in-process intercept, so a live account (non-hermetic, billed) or a hermetic REST mock is needed (> 3-day cap) MIT-licensed four-tier pipeline (raw / extracted records / scene blocks / persona); raw-layer-append-only is a by-convention recorder, not a typed audit per operator (the extraction-tier dedup leaves no witness), and a TS adapter + Node sidecar would not differentiate from Graphiti’s “raw preserved, resolution opaque” verdict 700 sessions, 15,000 memory points, 3,500 questions (Extract/Update/QA); Update maps one-to-one to N3 via gold (𝑚 old , 𝑚 new ) to n3_audit_erasure, but CC-BY-NC-ND 4.0 no-derivatives is legally ambiguous against PVLDB availability (needs unbounded written permission) and free-form plaintext needs a non-deterministic LLM preprocessing pass 400 scenarios, 1,200 queries (State Resolution, Premise Resistance, Implicit Policy Adaptation) under CC-BY-4.0; State Resolution and Premise Resistance map to N1, Implicit Policy Adaptation is an N2 correlate needing a projection; the 55.2% best-frontier figure comes from 1,200 prompts at 150 K context to a closed API the bench cannot call four-domain enterprise corpus (∼ 30,000 msgs/domain, 6–10 channels, six question types); sessions of several thousand turns exceed the 200K-token extractor budget, and the 128-turn chunked path (∼ 235 sequential calls/tile) wedged the relay across the pilot. Two completed cells (bm25 0.20, simulated frontier 0.0, knowledge-update axis, 𝑛 = 30) ship in results/benchmark_f/groupmembench.csv as transparency evidence only
N1/N2/N3
N3
N3 (Update)
N1 (corroboration)
N3 (knowledge update)
Graphiti-Neo4j scope-out under V6 matched retrieval. The V6 matched-retrieval cells against Graphiti on LoCoMo and LongMemEval carry structured status=n/a abstention rows with abstention_kind=service_boundary: Graphiti needs a running Neo4j graph database, the reviewer-reproducible host does not deploy Neo4j as a service-boundary dependency, and the closest standalone deployment exceeds the per-wire cap once credentials, schema migration, and reproducible seeding are scoped. The transcribed Graphiti wire in §4.1 preserves the cited-commit N1/N2/N3 verdicts under the AnomalyWire dispatch path (which runs without live Neo4j); the deferred V6 cells concern only the matched-retrieval utility surface and rerun via the existing cross_system_runner entry points once a live cluster is reinstated.
G.9
Experimental Extensions for a Future Revision
The 2026-05 adversarial-review cascade flagged six compute-bound experimental extensions that strengthen the empirical chapter when run at scale. The manuscript’s positioning holds the typed operator algebra, the soundness theorems, and the AnomalyClaim and AnomalyWire artefacts as the contribution; each extension below is a strengthening pass rather than a load-bearing addition. Table 27 names each item, why it is deferred, and the smallest follow-on protocol that closes it.
H
EXTENDED RELATED WORK AND POSITIONING
The body (Section 5) positions Toki against the isolation-theory and agent-memory-benchmark neighbors closest to its claims. This appendix extends that positioning across five further literatures. Each subsection states what the line contributes and where the typed write-time operator algebra of Section 3.2 sits relative to it. The recurring boundary is consistent. Prior lines fix the storage substrate, the read-path operator, the provenance carrier, or the belief-update rule. Toki supplies the missing piece: a type for the contradiction-resolution operator together with the isolation level its correctness assumes.
H.1
Agent-memory architectures
Agent-memory architectures organize how an agent writes, retrieves, and consolidates long-horizon state. MemGPT casts the language model as an operating system that pages memory between a bounded context window and an external store [53]. Generative Agents store episodic 39
Ziming Wang
Table 27: Compute-bound experimental extensions for a future revision. Each is a strengthening pass on the scoped empirical slice, not a load-bearing addition. Extension
Why deferred
Smallest closing protocol
Hosted mem0 v2 published-config rerun
the mem0 v3 cross-system row (Table 18) runs with five configuration deltas from the published operating point (Appendix A.7); the paper leads with the algebra and verdict matrix, not a single cross-system delta
Judge-pin discriminating-workload run
the G2 primary judge-pin diagonal reports Δaccuracy = 0.00 on LoCoMo with four of six off-target controls also moving positive; judge-pin is positioned as the N1 checker-detected predicate, the Δaccuracy a secondary channel the envelope reports mean ∼ 𝑐 0.86 at 𝑅 2 = 0.99 across 30 samples/rung, where the 𝑝 99 estimator is the sample maximum (so the body keeps the mean envelope, drops 𝑝 99 ) the G4 grid runs three carriers (multilinear N[𝑋 ,𝑇 ] , multi-degree N[𝑋 ,𝑇 ] # , Boolean reduct) with verdict-layer invariance; the 𝐾 [𝑋 ,𝑇 ] carrier is a forward-compatibility hook, and a fourth probabilistic cell would commit to confidence-weighting as load-bearing G3 runs against the in-memory backend; the §G.2 pilot establishes the SERIALIZABLE saturation point (18 of 36 commits at concurrency two, 11 of 36 at four) G1 runs three benchmarks (LongMemEval-S, LoCoMo, MultiTQ) over 33 wire cells; the breadth claim rests on the 33-cell matrix not benchmark count, and no reviewer flagged BEAM
a second cell under the published config (hosted v2 client, larger top-𝑘 , graph mode on, published extractor, ≥ 3 LoCoMo conversations), lifting harness-vs-harness to system-vs-system under bounded compute a run on an ImpossibleBench-style constructed workload, producing a positive delta or confirming inertia, independent of the algebra’s load-bearing claim
G3 scaling to larger 𝑛 per rung
Confidence-semiring carrier cell
PostgreSQL-backend confirmation for G3 BEAM synthetic memory benchmark
scale to 10× the sample size per rung across the two main-text axes, stabilising 𝑝 99 from sample maximum to a quantile estimate a future paper introducing a confidence-weighted resolution operator lands the fourth carrier cell and revises the classification
a full confirmation run extending the pilot across the remaining G3 axes via a single SQL-layer adapter on the existing G3 runner, testing platform-independence of 𝑐 0.86 land the BEAM integration as a fourth benchmark axis testing composability under perturbation
observations and synthesize them through periodic reflection [54]. HippoRAG indexes long-term memory through a knowledge-graph retrieval structure inspired by hippocampal indexing [32]. Recent systems push this substrate toward databases: MemoriesDB organizes agent memory as a temporal-semantic-relational store [72], and Engram backs coding-agent memory with a bitemporal graph [18]. A recent survey catalogues the mechanisms and evaluation gaps of this space [22]. These architectures decide where a fact is stored and how it is recalled; Toki types the operator that decides which of two contradicting facts survives a write and states the isolation level (Section 3.2) under which that decision is sound.
H.2
Semantic-operator data systems
A parallel line at the data-systems venues types the language model as a relational operator and optimizes pipelines of such operators. LOTUS defines semantic operators over tables and optimizes them with accuracy guarantees [56]; Abacus adds a cost-based optimizer for semantic-operator systems [60]; DocETL rewrites agentic document-processing pipelines [64]. The broader argument that hand-crafted systems give way to learned and language-model components frames the trend [34], and the agent-first redesign of data systems extends it to the agent setting [41]. These systems type the language model on the read and query path, where the operator transforms or selects data the caller already trusts; Toki types it on the write path, where the operator adjudicates a contradiction and commits one survivor, making soundness a question of which interleavings of competing writes the operator admits.
H.3
Provenance and semiring lineage
The 𝐾-relation provenance carrier of Section 3 rests on the semiring provenance tradition. Buneman, Khanna, and Tan characterize whyand where-provenance [13], and Cheney, Chiticariu, and Tan survey the why, how, and where dimensions [19]. Geerts, Poggi, and Tannen delimit where provenance for queries with difference reaches its limit [26], a boundary the audit-erasure recovery of Theorem 2 respects by working in a semiring without multiplicative inverses. The algebraic backbone extends to weighted shortest-distance computation [50] and to provenance for lightweight description logics [11]. This tradition explains how a query result traces to its inputs; Toki applies the same carrier to the audit row a contradiction-resolution operator emits so a superseded fact stays recoverable under the natural order.
H.4
Bitemporal and temporal data models
Temporal and bitemporal data models supply the storage substrate the operator algebra writes onto. Lorentzos and Johnson extend relational algebra to manipulate temporal data [42], and production bitemporal stores realize the model: Datomic records an information model with time, provenance, and accumulation [21], and XTDB exposes bitemporal SQL [69]. RoMem [39] learns per-relation volatility and phase-rotates obsolete facts out of retrieval reach without deleting them, a representation-time analogue of the audit-row preservation our schema axis types. These systems make valid time and transaction time first-class; Toki assumes such a substrate and adds the layer above it, where the four contradiction strategies ⊕t , ⊕p , ⊕? , and ⊕c become typed operators whose write-time anomalies the isolation guards exclude.
40
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
H.5
Belief revision and contradiction handling
Belief revision formalizes how an agent should change what it believes when a new fact contradicts an old one. Recent work studies iterated revision with belief algebras [47] and revision over fuzzy belief bases [10], and a graph-native cognitive memory gives formal belief-revision semantics for versioned agent memory [55]. Roynard [59] argues each memory layer needs distinct persistence semantics (indefinite supersession, evidence-gated revision) and stops at the layer decomposition. This line answers which belief should hold after a contradiction; Toki answers which schedule of applying that revision is admissible under concurrent writers, and which write-time anomalies (N1, N2, N3) a given isolation level admits. The revision rule and the isolation level are independent axes, connected by the alphabet bridge of Lemma 1.
H.6
Concurrency control and context-memory conflict
The write-time concurrency framing of Toki has two close neighbors. Adaptive concurrency control for unforeseen agentic transactions tunes isolation for agent workloads [84], and altruistic locking is the classical strategy for long-lived transactions [62], the regime an agent’s multi-step write resembles. On the empirical side, recent work characterizes context-memory conflict as predictable regimes [71] and reconciles such conflicts dynamically [85]. These efforts tune or describe the conflict. Toki types it: the replay-inconsistency, belief-drift-skew, and audit-erasure predicates are the write-time anomalies a concurrency-control scheme must exclude, and Theorem 5 lower-bounds the replay anomaly any system without keyed-judge-log discipline admits.
REFERENCES [1] Seyed Moein Abtahi, Rasa Rahnema, Hetkumar Patel, Neel Patel, Majid Fekri, and Tara Khani. 2026. Memanto: Typed Semantic Memory with Information-Theoretic Retrieval for Long-Horizon Agents. arXiv preprint arXiv:2604.22085 (2026). https://arxiv.org/abs/2604.22085 [2] Atul Adya, Barbara Liskov, and Patrick E. O’Neil. 2000. Generalized Isolation Level Definitions. In Proceedings of the 16th International Conference on Data Engineering (ICDE). 67–78. https://doi.org/10.1109/ICDE.2000.839388 [3] James F. Allen. 1983. Maintaining Knowledge about Temporal Intervals. Commun. ACM 26, 11 (1983), 832–843. https://doi.org/10.1145/182.358434 [4] Bahareh Sadat Arab, Su Feng Lee, Boris Glavic, Xing Niu, Seokki Lee, and Thomas Heinis. 2017. Using Reenactment to Retroactively Capture Provenance for Transactions. In Proceedings of the 2017 IEEE 33rd International Conference on Data Engineering (ICDE 2017). IEEE, 1077–1088. https://doi.org/10.1109/ICDE.2017.149 [5] Pratyay Banerjee, Masud Moshtaghi, Shivashankar Subramanian, Amita Misra, and Ankit Chadha. 2026. APEX-MEM: Agentic Semi-Structured Memory with Temporal Reasoning for Long-Term Conversational AI. arXiv preprint arXiv:2604.14362 (2026). https://arxiv.org/abs/2604.14362 [6] Manuel Barros, Alcino Cunha, Jose Pereira, and Eunsuk Kang. 2026. Reasoning about Transactional Isolation Levels with Isolde. arXiv preprint arXiv:2604.00159 (2026). https://arxiv.org/abs/2604.00159 [7] Hal Berenson, Philip A. Bernstein, Jim Gray, Jim Melton, Elizabeth J. O’Neil, and Patrick E. O’Neil. 1995. A Critique of ANSI SQL Isolation Levels. In Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data. ACM, 1–10. https://doi.org/10.1145/223784.223785 [8] Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. 1987. Concurrency Control and Recovery in Database Systems. Addison-Wesley. https://www.microsoft.com/enus/research/wp-content/uploads/2016/05/ccontrol.zip [9] Nishant Bhargava and Rodrigo Sobral Barrento. 2026. MemAudit: An Exact Package-Oracle Evaluation Protocol for Budgeted Long-Term LLM Memory Writing. arXiv:2605.02199 [cs.AI] https://arxiv.org/abs/2605.02199 [10] Richard Booth and Eva Richter. 2012. On Revising Fuzzy Belief Bases. arXiv preprint arXiv:1212.2444 (2012). https://arxiv.org/abs/1212.2444 [11] Camille Bourgaux, Ana Ozaki, and Rafael Peñaloza. 2023. Semiring Provenance for Lightweight Description Logics. arXiv preprint arXiv:2310.16472 (2023). https: //arxiv.org/abs/2310.16472 [12] Sophie Brinke, Anuj Dawar, Erich Grädel, and Benedikt Pago. 2026. Preservation Theorems in Semiring Semantics. arXiv:2605.10829 [cs.LO] https://arxiv.org/abs/2605. 10829 [13] Peter Buneman, Sanjeev Khanna, and Wang-Chiew Tan. 2001. Why and Where: A Characterization of Data Provenance. In Database Theory - ICDT 2001, 8th International Conference (Lecture Notes in Computer Science), Vol. 1973. Springer, 316–330. https://doi.org/10.1007/3-540-44503-X_20 [14] Michael J. Cahill, Uwe Röhm, and Alan D. Fekete. 2008. Serializable Isolation for Snapshot Databases. In Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data. ACM, 729–738. https://doi.org/10.1145/1376616.1376690 [15] Hanxiang Chao, Yihan Bai, Rui Sheng, Tianle Li, and Yushi Sun. 2026. STALE: Can LLM Agents Know When Their Memories Are No Longer Valid? arXiv preprint arXiv:2605.06527 (2026). https://arxiv.org/abs/2605.06527 [16] Ding Chen, Simin Niu, Kehang Li, Peng Liu, Xiangping Zheng, Bo Tang, Xinchi Li, Feiyu Xiong, and Zhiyu Li. 2025. HaluMem: Evaluating Hallucinations in Memory Systems of Agents. arXiv preprint arXiv:2511.03506 (2025). https://doi.org/10.48550/arXiv.2511.03506 [17] Ziyang Chen, Jinzhi Liao, and Xiang Zhao. 2023. Multi-granularity Temporal Question Answering over Knowledge Graphs. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). Association for Computational Linguistics, 11378–11392. https://doi.org/10.18653/v1/2023.acllong.637 [18] Chris Cheney and Engram contributors. 2026. Engram: Bitemporal, Graph-Backed Memory System for AI Coding Agents. GitHub repository, AGPL-3.0 licence, latest release [email protected] (2025-12-30), HEAD commit 1553e53 (2026-01-05T20:10:48Z), 5 stars and 1 fork at survey. https://github.com/rawcontext/engram [19] James Cheney, Laura Chiticariu, and Wang-Chiew Tan. 2009. Provenance in Databases: Why, How, and Where. Foundations and Trends in Databases 1, 4 (2009), 379–474. https://doi.org/10.1561/1900000006 [20] Prateek Chhikara, Dev Khant, Saket Aryan, Taranjeet Singh, and Deshraj Yadav. 2025. Mem0: Building Production-Ready AI Agents with Scalable Long-Term Memory. arXiv preprint arXiv:2504.19413 (2025). https://arxiv.org/abs/2504.19413 [21] Cognitect. 2026. Datomic: An Information Model with Time, Provenance, and Accumulation. Online documentation. https://docs.datomic.com/datomic-overview.html [22] Pengfei Du. 2026. Memory for Autonomous LLM Agents: Mechanisms, Evaluation, and Emerging Frontiers. arXiv preprint arXiv:2603.07670 (2026). https://arxiv.org/abs/ 2603.07670 [23] Alan Fekete, Dimitrios Liarokapis, Elizabeth O’Neil, Patrick O’Neil, and Dennis Shasha. 2005. Making Snapshot Isolation Serializable. ACM Transactions on Database Systems 30, 2 (2005), 492–528. https://doi.org/10.1145/1071610.1071615 [24] J. Nathan Foster, Todd J. Green, and Val Tannen. 2008. Annotated XML: Queries and Provenance. In Proceedings of the 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS ’08). ACM, 271–280. https://doi.org/10.1145/1376916.1376953 [25] Harish Santhanalakshmi Ganesan. 2026. WorldDB: A Vector Graph-of-Worlds Memory Engine with Ontology-Aware Write-Time Reconciliation. arXiv:2604.18478 [cs.AI]. https://arxiv.org/abs/2604.18478 [26] Floris Geerts, Antonella Poggi, and Val Tannen. 2013. On the Limitations of Provenance for Queries with Difference. In Proceedings of the Theory and Practice of Provenance Workshop (TaPP ’13). USENIX Association. https://doi.org/10.1145/2448496.2448516 [27] Shabnam Ghasemirad, Si Liu, Christoph Sprenger, and David Basin. 2025. VerIso: Verifiable Isolation Guarantees for Database Transactions. Proc. VLDB Endow. 18, 5 (2025), 1362–1375. https://doi.org/10.14778/3718057.3718065 41
Ziming Wang
[28] Rohit Ghumare and AgentMemory contributors. 2026. AgentMemory: Persistent Memory for AI Coding Agents. GitHub repository, Apache-2.0 licence, npm package @agentmemory/agentmemory, latest release v0.9.17 (2026-05-16), HEAD commit c93c715 (2026-05-17T11:15:59Z). https://github.com/rohitg00/agentmemory [29] Erich Grädel and Val Tannen. 2024. Provenance Analysis and Semiring Semantics for First-Order Logic. arXiv preprint arXiv:2412.07986 (2024). https://arxiv.org/abs/ 2412.07986 [30] Todd J. Green, Grigoris Karvounarakis, and Val Tannen. 2007. Provenance Semirings. In Proceedings of the 26th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS). 31–40. https://doi.org/10.1145/1265530.1265535 [31] Todd J. Green and Val Tannen. 2017. The Semiring Framework for Database Provenance. In Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS). 93–99. https://doi.org/10.1145/3034786.3056125 [32] Bernal Jiménez Gutiérrez, Yiheng Shu, Yu Gu, Michihiro Yasunaga, and Yu Su. 2024. HippoRAG: Neurobiologically Inspired Long-Term Memory for Large Language Models. In Advances in Neural Information Processing Systems 37 (NeurIPS 2024). https://arxiv.org/abs/2405.14831 [33] Jun He and Deying Yu. 2026. Verifiable Agentic Infrastructure: Proof-Derived Authorization for Sovereign AI Systems. arXiv:2605.15228 [cs.AI] https://arxiv.org/abs/ 2605.15228 [34] Stratos Idreos. 2025. Alphabets, Grammars, Calculators, and the End of Hand-Crafted Systems. Proceedings of the VLDB Endowment (PVLDB) 18, 12 (2025), 5537. https: //doi.org/10.14778/3750601.3760522 [35] Christian S. Jensen, Curtis E. Dyreson, Michael Böhlen, James Clifford, Ramez Elmasri, Shashi K. Gadia, Fabio Grandi, Pat Hayes, Sushil Jajodia, et al. 1998. The Consensus Glossary of Temporal Database Concepts—February 1998 Version. In Temporal Databases: Research and Practice, Opher Etzion, Sushil Jajodia, and Suryanarayana Sripada (Eds.). Lecture Notes in Computer Science, Vol. 1399. Springer, 367–405. https://doi.org/10.1007/BFb0053710 [36] Sajjad Khan. 2026. S-Bus: Automatic Read-Set Reconstruction for Multi-Agent LLM State Coordination. arXiv:2605.17076 [cs.DC] https://arxiv.org/abs/2605.17076 [37] Krishna Kulkarni and Jan-Eike Michels. 2012. Temporal Features in SQL:2011. ACM SIGMOD Record 41, 3 (2012), 34–43. https://doi.org/10.1145/2380776.2380786 [38] Letta Team. 2026. Context Constitution: Letta Code’s Memory Filesystem. Letta engineering blog. https://letta.com/blog/context-constitution [39] Weixian Waylon Li, Jiaxin Zhang, Xianan Jim Yang, Tiejun Ma, and Yiwen Guo. 2026. Time is Not a Label: Continuous Phase Rotation for Temporal Knowledge Graphs and Agentic Memory. arXiv preprint arXiv:2604.11544 (2026). https://arxiv.org/abs/2604.11544 [40] Zhiyu Li, Chenyang Xi, Chunyu Li, Ding Chen, Boyu Chen, Shichao Song, Simin Niu, Hanyu Wang, Jiawei Yang, Chen Tang, Qingchen Yu, Jihao Zhao, Yezhaohui Wang, Peng Liu, Zehao Lin, Pengyuan Wang, Jiahao Huo, Tianyi Chen, Kai Chen, Kehang Li, Zhen Tao, Huayi Lai, Hao Wu, Bo Tang, Zhengren Wang, Zhaoxin Fan, Ningyu Zhang, Linfeng Zhang, Junchi Yan, Mingchuan Yang, Tong Xu, Wei Xu, Huajun Chen, Haofen Wang, Hongkang Yang, Wentao Zhang, Zhi-Qin John Xu, Siheng Chen, and Feiyu Xiong. 2025. MemOS: A Memory OS for AI System. arXiv preprint arXiv:2507.03724 (2025). https://doi.org/10.48550/arXiv.2507.03724 [41] Shu Liu, Soujanya Ponnapalli, Shreya Shankar, Sepanta Zeighami, Alan Zhu, Shubham Agarwal, Ruiqi Chen, Samion Suwito, Shuo Yuan, Ion Stoica, Matei Zaharia, Alvin Cheung, Natacha Crooks, Joseph E. Gonzalez, and Aditya G. Parameswaran. 2026. Supporting Our AI Overlords: Redesigning Data Systems to be Agent-First. Proc. CIDR 2026, January 18–21, Chaminade. https://www.cidrdb.org/cidr2026/papers/p32-liu.pdf [42] Nikos A. Lorentzos and Roger G. Johnson. 1988. Extending Relational Algebra to Manipulate Temporal Data. In Proceedings of the 14th International Conference on Very Large Data Bases (VLDB). Morgan Kaufmann, 289–296. https://vldb.org/conf/1988/P289.PDF [43] Yihao Lu, Wanru Cheng, Zeyu Zhang, and Hao Tang. 2026. MMA: Multimodal Memory Agent. arXiv:2602.16493 [cs.AI] https://arxiv.org/abs/2602.16493 [44] Yang Luo, Zifeng Kang, Tiantian Ji, Xinran Liu, Yong Liu, Shuyu Li, and Lingyun Peng. 2026. ShadowMerge: A Novel Poisoning Attack on Graph-Based Agent Memory via Relation-Channel Conflicts. arXiv preprint arXiv:2605.09033 (2026). https://arxiv.org/abs/2605.09033 [45] Adyasha Maharana, Dong-Ho Lee, Sergey Tulyakov, Mohit Bansal, Francesco Barbieri, and Yuwei Fang. 2024. Evaluating Very Long-Term Conversational Memory of LLM Agents. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 13851–13870. https://doi.org/10.18653/v1/2024.acllong.747 [46] Mem0 Team. 2026. Mem0 README: New Memory Algorithm (April 2026). GitHub repository README. https://github.com/mem0ai/mem0/blob/main/README.md [47] Hua Meng, Zhiguo Long, Michael Sioutis, and Zhengchun Zhou. 2025. On Definite Iterated Belief Revision with Belief Algebras. arXiv preprint arXiv:2505.06505 (2025). https://arxiv.org/abs/2505.06505 [48] Solomon Messing. 2026. Hidden Measurement Error in LLM Pipelines Distorts Annotation, Evaluation, and Benchmarking. arXiv:2604.11581 [cs.CL] https://arxiv.org/ abs/2604.11581 [49] Bardia Mohammadi, Nearchos Potamitis, Lars Klein, Akhil Arora, and Laurent Bindschaedler. 2026. Atomix: Timely, Transactional Tool Use for Reliable Agentic Workflows. arXiv:2602.14849 [cs.DC] https://arxiv.org/abs/2602.14849 [50] Mehryar Mohri. 2002. Semiring Frameworks and Algorithms for Shortest-Distance Problems. Journal of Automata, Languages and Combinatorics 7, 3 (2002), 321–350. http://www.cs.nyu.edu/~mohri/pub/jalc.pdf [51] Praveen Kumar Myakala, Manan Agrawal, and Rahul Manche. 2026. BeliefShift: Benchmarking Temporal Belief Consistency and Opinion Drift in LLM Agents. arXiv preprint arXiv:2603.23848 (2026). https://arxiv.org/abs/2603.23848 [52] Ciyan Ouyang and Rui Hou. 2026. MemLineage: Lineage-Guided Enforcement for LLM Agent Memory. arXiv preprint arXiv:2605.14421 (2026). https://arxiv.org/abs/ 2605.14421 [53] Charles Packer, Sarah Wooders, Kevin Lin, Vivian Fang, Shishir G. Patil, Ion Stoica, and Joseph E. Gonzalez. 2023. MemGPT: Towards LLMs as Operating Systems. arXiv preprint arXiv:2310.08560 (2023). https://arxiv.org/abs/2310.08560 [54] Joon Sung Park, Joseph C. O’Brien, Carrie J. Cai, Meredith Ringel Morris, Percy Liang, and Michael S. Bernstein. 2023. Generative Agents: Interactive Simulacra of Human Behavior. In Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology (UIST). 1–22. https://doi.org/10.1145/3586183.3606763 [55] Young Bin Park. 2026. Graph-Native Cognitive Memory for AI Agents: Formal Belief Revision Semantics for Versioned Memory Architectures. arXiv preprint arXiv:2603.17244 (2026). https://arxiv.org/abs/2603.17244 [56] Liana Patel, Siddharth Jha, Melissa Pan, Harshit Gupta, Parth Asawa, Carlos Guestrin, and Matei Zaharia. 2025. Semantic Operators and Their Optimization: Enabling LLM-Based Data Processing with Accuracy Guarantees in LOTUS. Proceedings of the VLDB Endowment (PVLDB) 18, 11 (2025), 4171–4184. https://doi.org/10.14778/3749646.3749685 [57] Sidharth Pulipaka, Stanislau Hlebik, Leonidas Raghav, Sahar Abdelnabi, Vyas Raina, Ivaxi Sheth, and Mario Fritz. 2026. Hidden in Memory: Sleeper Memory Poisoning in LLM Agents. arXiv:2605.15338 [cs.CR] https://arxiv.org/abs/2605.15338 [58] Preston Rasmussen, Pavlo Paliychuk, Travis Beauvais, Jack Ryan, and Daniel Chalef. 2025. Zep: A Temporal Knowledge Graph Architecture for Agent Memory. arXiv preprint arXiv:2501.13956 (2025). https://arxiv.org/abs/2501.13956 [59] Michaël Roynard. 2026. The Missing Knowledge Layer in Cognitive Architectures for AI Agents. arXiv preprint arXiv:2604.11364 (2026). https://arxiv.org/abs/2604.11364 [60] Matthew Russo, Chunwei Liu, Sivaprasad Sudhir, Gerardo Vitagliano, Michael Cafarella, Tim Kraska, and Samuel Madden. 2026. Abacus: A Cost-Based Optimizer for Semantic Operator Systems. Proceedings of the VLDB Endowment (PVLDB) 19, 5 (2026), 1060–1073. https://www.vldb.org/pvldb/vol19/p1060-russo.pdf [61] Albert Sadowski and Jarosław A. Chudziak. 2026. Rashomon Memory: Towards Argumentation-Driven Retrieval for Multi-Perspective Agent Memory. https://doi.org/ 10.48550/arXiv.2604.03588 arXiv:2604.03588 [62] Kenneth Salem, Hector Garcia-Molina, and Jeannie Sands. 1989. Altruistic Locking: A Strategy for Coping with Long Lived Transactions. In Proceedings of the 2nd International Workshop on High Performance Transaction Systems. https://doi.org/10.1145/64162.64173 [63] Dhravya Shah and Supermemory contributors. 2026. Supermemory: State-of-the-art Memory and Context Engine for AI. GitHub repository supermemoryai/supermemory, MIT licence, HEAD commit 36ecf47 (2026-05-17T07:55:12Z), 22,596 stars, zero GitHub releases, Python SDK supermemory-openai-sdk on PyPI at alpha v1.0.3. https: //github.com/supermemoryai/supermemory [64] Shreya Shankar, Tristan Chambers, Tarak Shah, Aditya G. Parameswaran, and Eugene Wu. 2025. DocETL: Agentic Query Rewriting and Evaluation for Complex Document Processing. Proceedings of the VLDB Endowment (PVLDB) 18, 12 (2025), 3920–3932. https://www.vldb.org/pvldb/vol18/p3920-shankar.pdf [65] Richard Snodgrass and Ilsoo Ahn. 1986. Temporal Databases. IEEE Computer 19, 9 (1986), 35–42. https://doi.org/10.1109/MC.1986.1663327 [66] Richard T. Snodgrass. 2000. Developing Time-Oriented Database Applications in SQL. Morgan Kaufmann, San Francisco, CA. https://www2.cs.arizona.edu/~rts/tdbbook. pdf 42
TOKI: A Bitemporal Operator Algebra for Contradiction Resolution in LLM-Agent Persistent Memory
[67] Miao Su, Yucan Guo, Zhongni Hou, Long Bai, Zixuan Li, Yufei Zhang, Guojun Yin, Wei Lin, Xiaolong Jin, Jiafeng Guo, and Xueqi Cheng. 2026. Beyond Dialogue Time: Temporal Semantic Memory for Personalized LLM Agents. arXiv preprint arXiv:2601.07468 (2026). https://arxiv.org/abs/2601.07468 [68] Tencent. 2026. TencentDB Agent Memory: Fully Local Long-Term Memory for AI Agents via a 4-Tier Progressive Pipeline. GitHub repository Tencent/TencentDB-Agent-Memory, MIT licence (Tencent header wrapper), HEAD commit 5736acc (2026-05-16T12:17:22Z), latest release v0.3.4 (2026-05-13), 2,674 stars, npm package @tencentdb-agent-memory/memory-tencentdb, Node >=22.16 required. https://github.com/Tencent/TencentDB-Agent-Memory [69] The XTDB Authors. 2026. XTDB 2.x: Bitemporal SQL for the Real World. Online documentation. https://docs.xtdb.com/intro/what-is-xtdb.html [70] Md Nayem Uddin, Kumar Shubham, Eduardo Blanco, Chitta Baral, and Gengyu Wang. 2026. From Recall to Forgetting: Benchmarking Long-Term Memory for Personalized Agents. arXiv preprint arXiv:2604.20006 (2026). https://arxiv.org/abs/2604.20006 [71] Pruthvinath Jeripity Venkata. 2026. Three Regimes of Context-Parametric Conflict: A Predictive Framework and Empirical Validation. arXiv:2605.11574 [cs.CL] https: //arxiv.org/abs/2605.11574 [72] Joel Ward. 2025. MemoriesDB: A Temporal-Semantic-Relational Database for Long-Term Agent Memory. arXiv preprint arXiv:2511.06179 (2025). https://arxiv.org/abs/ 2511.06179 [73] Lei Wei, Xiao Peng, Xu Dong, Niantao Xie, and Bin Wang. 2026. FadeMem: Biologically-Inspired Forgetting for Efficient Agent Memory. arXiv preprint arXiv:2601.18642 (2026). https://arxiv.org/abs/2601.18642 [74] Albert Widiaatmaja, Belkis Djeffal, Ashish Dandekar, and Pierre Senellart. 2025. Demonstration of ProvSQL Update Provenance through Temporal Databases. In Provenance Week@SIGMOD. https://doi.org/10.1145/3736229.3736253 [75] Di Wu, Zixiang Ji, Asmi Kawatkar, Bryan Kwan, Jia-Chen Gu, Nanyun Peng, and Kai-Wei Chang. 2026. LongMemEval-V2: Evaluating Long-Term Agent Memory Toward Experienced Colleagues. arXiv preprint arXiv:2605.12493 (2026). https://arxiv.org/abs/2605.12493 [76] Di Wu, Hongwei Wang, Wenhao Yu, Yuwei Zhang, Kai-Wei Chang, and Dong Yu. 2025. LongMemEval: Benchmarking Chat Assistants on Long-Term Interactive Memory. In Proceedings of the 13th International Conference on Learning Representations (ICLR). https://openreview.net/forum?id=pZiyCaVuti [77] Shiyao Xie and Jian Du. 2026. Neuro-Symbolic Resolution of Recommendation Conflicts in Multimorbidity Clinical Guidelines. In Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence, Bridge Program on Logic and AI. https://doi.org/10.48550/arXiv.2604.17340 [78] Jingbo Yang, Kwei-Herng Lai, Xiaowen Wang, Shiyu Chang, Yaar Harari, and Evgeniy Gabrilovich. 2026. GroupMemBench: Benchmarking LLM Agent Memory in Multi-Party Conversations. arXiv:2605.14498 [cs.CL] https://arxiv.org/abs/2605.14498 [79] Jiawei Yu, Yixiang Fang, Xilin Liu, and Yuchi Ma. 2026. H-Mem: A Novel Memory Mechanism for Evolving and Retrieving Agent Memory via a Hybrid Structure. arXiv:2605.15701 [cs.AI] https://arxiv.org/abs/2605.15701 [80] Zep AI. 2026. Graphiti: Build Real-Time Knowledge Graphs for AI Agents. GitHub repository. https://github.com/getzep/graphiti [81] Dylan Zhang, Yanshan Lin, Zhengkun Wu, Yihang Sun, Bingxuan Li, Dianqi Li, and Hao Peng. 2026. Useful Memories Become Faulty When Continuously Updated by LLMs. arXiv preprint arXiv:2605.12978 (2026). https://arxiv.org/abs/2605.12978 [82] Kehao Zhang, Shangtong Gui, Sheng Yang, Wei Chen, and Yang Feng. 2026. Learning to Remember: End-to-End Training of Memory Agents for Long-Context Reasoning. arXiv:2602.18493 [cs.CL] https://arxiv.org/abs/2602.18493 [83] Xing Zhang, Guanghui Wang, Yanwei Cui, Wei Qiu, Ziyuan Li, Bing Zhu, and Peiyang He. 2026. Experience Compression Spectrum: Unifying Memory, Skills, and Rules in LLM Agents. arXiv:2604.15877 [cs.AI] https://arxiv.org/abs/2604.15877 [84] Weixing Zhou, Zhiyou Wang, Zeshun Peng, Hetian Chen, Yanfeng Zhang, and Ge Yu. 2026. ATCC: Adaptive Concurrency Control for Unforeseen Agentic Transactions. arXiv preprint arXiv:2603.13906 (2026). https://arxiv.org/abs/2603.13906 [85] Yigeng Zhou, Wu Li, Yifan Lu, Yequan Wang, Xuebo Liu, Wenya Wang, Jun Yu, Min Zhang, and Jing Li. 2026. Mitigating Context-Memory Conflicts in LLMs through Dynamic Cognitive Reconciliation Decoding. arXiv:2605.12185 [cs.CL] https://arxiv.org/abs/2605.12185 [86] Mingxi Zou, Zhihan Guo, Langzhang Liang, Zhuo Wang, Qifan Wang, Qingsong Wen, Irwin King, Lizhen Qu, and Zenglin Xu. 2026. Remember the Decision, Not the Description: A Rate-Distortion Framework for Agent Memory. arXiv preprint arXiv:2605.10870 (2026). https://arxiv.org/abs/2605.10870
43