Mathematical foundations

The local transition, durable receipts, immutable readers and boundaries of the proof.

Local alpha · 23 September 2026. This is the public, project-neutral explanation of RURAL's mathematical prototype whitepaper. It describes implemented local behavior separately from proposed network behavior.

One durable transition#

RURAL has one authenticated local service owner. A branch has a head and an immutable key/value root. A command names its branch, expected head, typed mutation and stable request identity. The owner validates the command against current authority, prepares a new state without exposing it, appends its exact intent to a versioned journal, synchronizes the journal, then publishes the prepared root and receipt.

Let S be the visible state, c a command, J[n] its journal frame and R[b,id] the receipt for request id on branch b. Under the local synchronization and recovery assumptions, the safety contract is:

Ack(c) => Durable(J[n]) AND Visible(S') AND R[b,id] = receipt(c)

The reverse is not guaranteed: a reply can be lost after the journal is synchronized. The caller then retries the same request ID, expected head and arguments. An identical committed request returns its receipt; a different command under that identity conflicts. A partial or corrupt journal frame must be handled by recovery, not silently treated as a clean end of history.

Readers, branches and documents#

Readers retain immutable roots while the owner prepares later writes. A child branch initially shares its parent's root; later changes copy only affected map paths. A branch is a database experiment, not a Git worktree or an automatically independent replica. Merge comparison and resolution are explicit.

Ordinary records support create, read, update and delete with optional schema validation. Edges connect live documents and maintain forward and reverse indexes in the same authoritative transition. Analytics observations carry stable source/event identities, metric versions, units, windows and source coverage. An exact zero with missing sources is not a complete zero.

Atlas lenses are deterministic presentations of a selected snapshot. The Oracle and MCP return bounded, scoped evidence for an AI. Neither a visual record nor an AI output can become a credential or bypass current authority.

What is proved, and what is proposed#

The local argument is conditional on the tested journal and recovery contract; it is not a machine-checked proof of the Zig implementation or a hardware power-loss certification. Bounded TLA+ models explore portable-cell identity, transfer and replication safety, but no distributed cell protocol is running in this alpha.

The intended distinction is a combined contract for branchable project worlds, typed authority, replay receipts, coverage-aware analytics and compact AI evidence. This is a workflow hypothesis. There are no measured speed, capacity, cost or token-saving claims against SurrealDB, PostgreSQL or MongoDB. Read the current project status and local import exercise for what has actually been exercised.