RFD 0069 — The shared-live-KB write model: concurrent authoring, coexistence, and resolution

Scope. How many autonomous agents (plus humans and services) author concurrently against one shared, live Argon knowledge base, and how their contributions coexist, conflict, resolve, and coordinate. This RFD fixes the design — the layering, the write unit, the coordination boundary, and the resolution model — that the agent-integration surface (RFD 0066) forced into the open. It records why; it is not the spec. The load-bearing soundness claim is handed to a Lean mechanization (below), which gates implementation.

• State: discussion (owner-ratified shape; surface syntax and the gating mechanization are open)
• Relates to: RFD 0066 (agent integration — the surface that forced this), RFD 0052 / 0053 / 0057 (deployment topologies / the standalone concurrent engine / the served platform — the single-logical-writer substrate this builds on), RFD 0010 (strong negation / negative facts), RFD 0028 (defeasibility — the resolver), RFD 0045 (world assumptions — CWA default, #[world(open)]), RFD 0067 / 0068 (the four-valued lift), RFD 0014 (serving surface), RFD 0018 / 0021 (the incremental reasoner).
• Supersedes (in part): the promote()-as-last-writer-wins fork-merge shipped on the /v1 + embedded fork path (retired by D8).

Question

The runtime is a single-logical-writer bitemporal store (RFD 0052 D4 / 0053). The agent surface (RFD 0066) is, as shipped, an embedded, single-client server — a deliberate placeholder. The near-term requirement is a shared live KB: many concurrent writers against one durable store, whose authored contributions must be able to disagree durably (Argon’s whole reason to exist is Truth4::Both, standpoints, and a defeated conclusion that stays queryable). What is the write model — the write unit, the merge, the resolution, the coordination boundary — that delivers this without destroying the disagreement the substrate is built to hold?

Context

• The substrate already commits to coexistence machinery: FDE / Truth4 (Is/Not/Can/Both, Lean-mechanized, RFD 0067/0068), first-class standpoints (a <: lattice with an FDE information-join across per-source extents), Governatori defeasibility (#[defeats], +Δ/+∂/−Δ/−∂), CWA-by-default with per-concept #[world(open)] (RFD 0045), and a bitemporal append-only log with copy-on-write forks.
• The current fork promote() is a last-writer-wins signed-net-delta append (embedded + serve-private /v1). It silently destroys exactly the coexistence the substrate exists to preserve.
• This design is backed by a three-wave research campaign (a breadth map of 25 territories → a build-gating dive → a research-forward wave; ~500 verified sources). The campaign produced two structural results and a costed set of forks; the owner has ratified the shape recorded here. The campaign is a design input, not the spec — the external prior art it verified is cited inline.

Two structural results this design rests on

Result 1 — coexistence and resolution are two operators, not one (corroborated across six independent fields). A single merge operator cannot simultaneously be (i) a monotone information-order least-upper-bound — Both accumulates, order-independent, coordination-free — and (ii) a defeasible resolver — non-monotone, collapsing Both back to a definite value. The same wall was independently derived in six unrelated literatures: lattice theory (defeat moves a key down the info-order; an LUB cannot); differential-dataflow types (retraction needs an Abelian group, a join is only a monoid); judgment aggregation (majority is provably incompatible with a consensus postulate — Haret–Wallner–Woltran 2018); the CALM theorem (a non-monotone operation has no coordination-free implementation — Hellerstein–Alvaro 2020, an iff); conflict-of-laws doctrine (uniform symmetric cross-reference cannot terminate — the renvoi problem, In re Ross 1930 — law breaks symmetry with forum-priority, a defeats move, never a join); and abstract argumentation (the credulous∖skeptical meet is not set-intersection — Dung). The monotone information-join fragment has many homes; the defeasible resolver has none — no group-free algebra, no coordination theorem, no engine models it natively.

Result 2 — Both has no cheap home at any layer. Durable Both is not derivable in the knowledge-order least fixpoint (Fitting; it must be injected as an EDB annotation from the cross-standpoint join); it is forbidden by the provenance semiring (x·x̄ = 0); it is minimized away by record-linkage triage optima (Fellegi–Sunter); and it is collapsed by any scalar uncertainty surface. Carrying Both durably through the store → maintainer → aggregator → human surface is therefore the through-line build-not-find of the whole design.

Decision

D1 — Coexistence is reasoning-native, not storage-native. Disagreement lives in the reasoning layer (standpoints + Truth4 + provenance), not in the storage key. The write log stays a uniform monotone append; coexistence is a fold (the FDE information-join surfaces Both at projection/read time). This keeps the cheap commutative-monoid algebra and never hits the retraction-needs-a-group wall (Result 1). Storage-native coexistence (a third source axis in storage — demonstrated at scale by TARDiS/BT-tree/PRIMA) is real but drags per-type merge constructors, a two-valued store, and the group wall; it is rejected for v1. The reasoning-native bet is principled, not merely convenient: durable disagreement provably requires heterogeneous priors (Aumann), survives even a shared prior once higher-order common knowledge fails — the autonomous-agent case (Lederman), and is exactly what standpoint logic formalizes (Gómez-Álvarez–Rudolph).

D2 — Two operators, two layers. A monotone accumulate-Both merge (an information-order LUB; coordination-free, CRDT-clean, order-independent) is separate from a defeasible resolver that collapses Both to a definite value at read time, keeping the defeated conclusion queryable. Result 1 forbids one operator from being both. The merge is the write/fold path; the resolver is a read-time policy.

D3 — The write unit is the per-source (standpoint-scoped) extent — the Single-Writer carrier. Each source/agent owns a standpoint-scoped extent and is its sole writer. Sole-writer-per-extent is simultaneously contention-free (mechanical Single-Writer Principle) and monotone-append (semantic) — the two arguments coincide on one partition. Cross-source disagreement never rebases; it lands in different extents and meets as Both at the fold (D1).

D4 — The KB is a verb, not a noun. The shared object is the append-only write log plus per-standpoint projections; the cross-standpoint fold (the expensive coexistence computation) is materialized on demand, only where a cross-standpoint read is actually requested. The undecidable/coNP-hard certain-answer walls of eager global federation (Halevy) are thereby confined to the queries that demand them.

D5 — The tertiary cross-standpoint-designation layer (the resolver’s policy carrier). Argon gains a third, currently-unnamed rule layer, modeled on legal pluralism / conflict-of-laws: primary (facts) / secondary (rules) / tertiary = which standpoint’s view governs, relative to a forum. The tertiary layer is D2’s resolver expressed in the surface: forum-relative priority over standpoints, discharged by the existing defeasibility + priority machinery (RFD 0028) and Makinson–van der Torre input-output logic. This maps 1:1 onto standpoints + FDE + defeasibility + priority — the tightest external match to Argon’s whole committed shape, and it independently corroborates Result 1 (law resolves conflict by forum-priority, never by a symmetric join).

D6 — The coordination boundary is the monotone/non-monotone line (CALM). The monotone fragment {append a fact, OWA-assert, FDE information-join} is provably coordination-free — no serializer, no rebase. The non-monotone residue {retraction-semantics, #[defeats], CWA-negation-as-failure, uniqueness-of-a-value, exclusive-ownership} provably requires coordination. Uniqueness and exclusive-ownership are indivisible (escrow cannot remove them) and route through a per-scope linearizable frontier compare-and-swap; the rest is relocatable (escrow / sealing). Argon needs no self-built consensus — the single-logical-writer log means the only contested cell is the frontier watermark, served by one outsourced linearizable CAS.

D7 — Cross-writer trust needs an external decorrelated verifier, not internal vote-counting. With correlated writers (N clones of one base model are maximally-correlated voters), agreement is not evidence of correctness: majority correctness asymptotes to P(shared prior is right) < 1, not to truth (Dietrich–List), and more clones can lower competence (Kaniovski). The KB therefore never treats “N standpoints agree” as a correctness signal internally; trust is conferred by an external decorrelated verifier (a designated curator forum, or an out-of-family check) — the same decorrelation principle this track already applies in its cross-provider review gate.

D8 — Retire promote()-as-LWW. The flat-main last-writer-wins fork merge is withdrawn. It is neither a majority nor an arbitration operator (it is a recency-dictatorship), it voids every incremental-view-maintenance soundness theorem, and it is the anti-pattern four independent never-merge traditions reject. Its replacement is D1–D2: a standpoint-scoped monotone append-Both merge plus the read-time resolver.

Rationale

• Reasoning-native keeps the cheap algebra and the substrate’s crown jewels. The append-only log is already monotone; the FDE join is already the coexistence operator; standpoints are already the per-source partition. D1–D5 wire what exists rather than building a storage-side merge engine against the grain (Datomic — which the serve layer resembles — is natively anti-Both).
• The two-layer split is forced, not chosen. Result 1 is a structural wall independently corroborated across six fields; each rules out one operator being both accumulator and resolver. The corroboration is not itself the proof: the composition’s soundness for Argon is what the phase-0 Lean mechanization discharges — this RFD does not stand in for it.
• The coordination cost is minimal and known. D6 confines coordination to the small indivisible residue; everything else fans out coordination-free.
• Honesty over a faked signal. D7 refuses the seductive “agreements are answers” shortcut that correlation breaks.

Alternatives considered

• Storage-native coexistence (a source/belief axis in storage; TARDiS-shaped). Rejected for v1: per-type merge constructors + a two-valued store + the retraction group wall. Real and fast, but against the grain of a Truth4 reasoning layer. (D1.)
• One merge operator (a single CRDT-or-resolver). Rejected: Result 1 — the coexistence/resolution split (D2).
• Flat-main last-writer-wins promote (the shipped path). Rejected: D8’s indictment.
• Internal vote-counting for cross-writer trust. Rejected: correlated-writer non-independence (D7).
• Eager global federation (fold all standpoints into one read model up front). Rejected: certain-answer undecidability/coNP-hardness (Halevy); D4 makes the fold lazy.

Consequences

• Prerequisite, landed: the .oxbin standpoint-lattice + tier-table sections must be real (every decision is standpoint-based). Closed by the #1283 fix.
• The through-line build-not-find: a Truth4-native engine at scale that carries Both through the fixpoint (4QL / Laurent-2021 are the sub-scale starting points); the federation information-join ⊕ across source partitions; group-free four-valued incremental view maintenance (DBSP needs a group, Truth4 is a group-free bilattice → a semiring/semimodule IVM, unbuilt); a coexistence-preserving bitemporal merge; the tertiary designation layer (new surface); a source/standpoint-indexed Both human surface; and monotonicity verification over the bilattice.
• A new surface layer (D5, tertiary designation) — new syntax + semantics, gated on the book + Lean.
• Mechanization gates the build (framework-first). The load-bearing new soundness claim — that the two-layer composition (monotone append-Both merge + read-time defeasible resolver over standpoint-partitioned extents) is sound and that the reasoning-native fold behaves as specified under #[defeats] / CWA-negation / retraction — is mechanized in Lean before the implementation commits, with a differential oracle gating the engine. Result 1 already establishes the fold is not an ACI join once defeat enters (hence two layers); the mechanization discharges the composition.

Open questions

• The tertiary-designation surface syntax (forum-relative priority over standpoints): how it is declared, and its interaction with the existing #[defeats] / priority plane (RFD 0028).
• The correctness floor on the serve write path. Cross-process write serialization for the indivisible residue (uniqueness #271, delta-guard write-skew #224) and durable collision-free scope identity (#270/#285) — the per-scope frontier CAS D6 names — are enforced only in-process today. This must land before more than one writer shares a durable store.
• The Both human/agent surface. Presenting source/standpoint-indexed disagreement (and a bounded triage of preserved plurality — the “bandwidth” problem) without a routing oracle that is worst exactly on the hard-contested items (Mozannar–Sontag).
• Four-valued IVM at scale (group-free) and the exact resolver policy language.
• The external-verifier mechanism (D7): whether the decorrelated verifier is a curator standpoint, an out-of-family check, or a human forum — and how its verdict is recorded.

Build order (phased; framework-first)

0. Mechanize the two-layer composition soundness in Lean (scratch, never-merged until it holds); stand up the differential oracle. Gates 2+.
1. The correctness floor — cross-process write serialization for the indivisible residue + durable scope identity (the D6 CAS). The substrate must be sound under real concurrency before writers share it.
2. Standpoint-scoped write + monotone append-Both merge (D1/D3), replacing promote()-LWW (D8).
3. The read-time defeasible resolver + the tertiary designation layer (D2/D5).
4. The Truth4-native engine at scale + group-free four-valued IVM (the through-line).
5. The Both agent/human surface + the external decorrelated verifier (D7).

Each phase is gated by a differential oracle against the mechanized model, not by the framework alone.