← Rivering · beecork.com/rivering
Technical companion · not the place to start
Five propositions with proofs, six claims that are not propositions, and the four places where writing this down changed what the other two documents say. Then the falsifiers, actually attempted — against 270 real tables.
The companion documents argue. Argument is the right register for them — they are written to be read by people who don't write code, and a proof would not help that reader.
But an argument and a proof are different things, and a document that mixes them invites a reasonable objection: which of these am I being asked to accept on evidence, and which on authority? This page separates them.
You cannot prove a taxonomy. “There are two kinds — the river and the noun” is not the sort of claim that has a proof; it is an empirical claim, and §06 states it as one with its denominator attached. What can be proved is a smaller and more interesting set: five propositions that the other documents currently present as persuasion.
Writing this changed four things. Formalising a claim is a test of it, and four did not survive contact in the form they were written. Two were sharpened, one was widened, and one was downgraded from a theorem to a robustness argument. They are collected in §07, and the corrections have been made in both companion documents.
Enough definition to make the propositions say something, and no more.
An event e is a tuple (s, to, tr, n, p) — a subject, the time it occurred, the time it was recorded, a name drawn from a fixed set, and a payload.
A history H is a finite sequence of events. H′ ⊇ H means H′ extends H: it contains every event of H and possibly more.
A derivation is a function f : H → V from histories to values. A table whose rows are produced only by evaluating some f is derived.
A guarantee G is a predicate over a table that the system requires to hold. A lock is a row whose existence is what makes G hold.
A rebuild R of a derived table T is the operation delete(T); insert(f(H)).
Let f : H → V be a derivation. Then H is recoverable from f(H) if and only if f is injective — and any f that discards order, multiplicity or timing is not injective.
That f is a function gives the forward direction: a history determines exactly one value. Recovery in the other direction is precisely the existence of f−1, which exists iff f is injective.
For the second clause it suffices to exhibit two histories with one image. Let f be “is currently enrolled”. Take H₁ = ⟨joined⟩ and H₂ = ⟨joined, left, joined⟩. Then H₁ ≠ H₂ and f(H₁) = f(H₂) = true. So f is not injective, and no inverse exists. ∎
Corollary 1.1. A system retaining only f(H) and discarding H cannot answer when or how many times. Those facts are in the fibre of f, not in its image.
The converse case is real and the documents never mention it. If f is injective — the value retains everything the history contained — then f−1 exists and V is merely an encoding of H. A table holding such a value is a history in different clothes, whatever it is called. Derivation presupposes loss. A lossless copy of a river is a second river, and inherits a river's rules — not a derived table's.
If two tables assert the same fact and are written independently, and the system retains no record of those writes, then no reconciliation procedure exists.
A reconciliation procedure is a function r(a, b) returning which of the two assertions is correct. Suppose one exists.
Consider run R₁ in which the write to A succeeded and the write to B failed, leaving the pair (a, b). Consider run R₂ in which the write to B succeeded and the write to A failed, leaving the same pair (a, b) — possible precisely because the two writes are independent and unrecorded.
Correctness demands r(a,b) = A in R₁ and r(a,b) = B in R₂. But r is a function of (a,b) alone, and (a,b) is identical. Contradiction. ∎
Corollary 2.1. If instead B = g(A) and B is written only by evaluating g, then b ≠ g(a) implies B is stale, and r is the constant function returning A. Reconcilability requires a designated original and a one-way derivation. This is the shop with two answers, and the whiteboard rule is its remedy.
The impossibility in Proposition 2 is relative to what the system retains, and that qualifier is load-bearing. If the two writes are themselves recorded as events, then (a,b) is no longer the whole state, the two runs are distinguishable, and a reconciliation procedure can be defined over the log.
So there is a second cure for two originals, and it is one the documents never offer: keep a river of the writes. Which is exactly what an audit log is for — and it explains why a system with a complete audit trail can survive a shape that would otherwise be unrecoverable.
Every derived value is either final or replaceable, never both and never neither.
Let v = f(H, t) be a derived value evaluated at time t, concerning an interval I. Say I is closed at t when no extension of H can add an event falling in I.
Either I is closed at t or it is not; there is no third case.
If closed, then for every H′ ⊇ H and every t′ ≥ t we have f(H′, t′) = f(H, t). The value is final — a summary.
If not closed, there exists H′ ⊇ H with f(H′, t′) ≠ f(H, t). The value is replaceable — state.
The two are mutually exclusive, since a value cannot be both unchangeable and changeable; and jointly exhaustive, by the dichotomy. ∎
“Not closed” includes intervals lying entirely in the future. A forecast — projected revenue for next month — is state by this proposition: replaceable, and replaced as data arrives. Both companion documents describe state as being “about now”, which excludes it. The theorem licenses more than the prose claims, and the prose has been widened.
If a guarantee G is enforced solely by rows of a table T, and T is rebuilt while operations guarded by G may run, then G can be violated.
A rebuild is delete(T); insert(f(H)). Between the two statements T is empty, so no row of T enforces anything and G does not hold.
If an operation guarded by G executes in that interval, it is admitted when it should have been refused. ∎
The proposition holds only under its condition: that guarded operations may run during the rebuild. Serialise the rebuild against every operation G guards — an exclusive lock held across the whole of R — and the empty interval is unobservable. The violation does not arise. A selective rebuild that spares the lock rows also avoids it.
So “a lock never sits on a rebuildable table” is not a correctness theorem. It is a robustness claim, and a good one: both safe variants work, and both fail silently the first time somebody empties the table the ordinary way — with no error, no test failure, and double-booking returning unannounced. That is a real and sufficient reason for the rule. It is simply a different kind of reason, and the documents should say which they are making. They now do.
Checking before acting cannot prevent a duplicate under concurrency; claiming can.
Let two processes each execute: read T for key k; if absent, insert. Consider the interleaving read₁, read₂, insert₁, insert₂. Both reads return absent, both inserts proceed, and the guarded effect occurs twice.
The interval between a read and the subsequent write is non-zero in any implementation, so no amount of re-reading removes the interleaving. The check cannot be made safe.
Now let k carry a uniqueness constraint enforced by the store. Both processes attempt the insert; the store serialises them; exactly one commits and the other is refused. Asking and claiming have become one indivisible operation, and the refusal carries the information the check was trying to obtain. ∎
Condition: requires the store to enforce the constraint atomically. This is the classic time-of-check-to-time-of-use race, and the fix is the classic one.
Everything else the documents assert falls here. Each is labelled by what kind of claim it is, and each carries the observation that would refute it. A claim with no falsifier is not a claim; it is a preference, and is marked as one.
Falsified by: a third kind — a table that is genuinely settled, not merely unrivered, and is neither something that happened nor something that is. Denominator: 270 tables in one relational system, plus seven outside domains. Not a proof, and not claimed as one.
What does not falsify it: a new archetype. Archetypes — branch and heartbeat of the river; state, summary and lock of the noun — are open by design, and grew once, when the branch was added on 10 September. A new shape adds a name; it refutes nothing. What would refute the claim is an archetype that belongs to neither kind.
Falsified by: a river whose rows-per-subject at the 99th percentile runs into the thousands and whose users find the timeline perfectly usable. The proxy is a number, so the claim is at least checkable — but the threshold is a judgement, not a result.
False in general, and deliberately so. A person's surname has no generating event; no river was ever missing. The rule is a prompt to look before concluding, not a statement about the world — which is why the ladder now asks you to name the line rather than judge whether one could exist.
Holds only when the loss is undecided. Overwriting a phone number destroys history and is correct; dimensional modelling names the same practice deliberately. The defect is losing history nobody decided to lose. Corrected in both documents on 8 September.
Cannot be false — only unhelpful. This defines subject; it does not assert anything about the world. Its value is that it is not steerable by choosing a word, which is a property of definitions, not of theorems. Worth stating plainly, because a definition presented as a discovery is how methods acquire false authority.
Not a claim at all. It asserts that a decision must be made, not what the answer is. Its justification is Proposition 3 plus the observation that three archetypes' rules — summary, heartbeat and branch — depend on the answer.
Run on 8 September against the database these documents came from: 270 tables, the full ladder, by machine, with every fall-through read by hand. A falsifier nobody attempts is decoration.
Are there tables that fit nowhere in the list?
At the time of this run the list still had six flat kinds; it became two kinds and their archetypes on 10 September. The result translates without loss, because every archetype carries exactly the rules its old kind carried.
Eight of 270 fell through. Read by hand: six were classifier misses — join tables, a settings row, a click log — each of which settles cleanly once a person looks at it: a river or a noun, with its archetype. One was genuine debris (an import clean-up table with a date in its name, 109 rows, no primary key), correctly unrivered: nobody has decided about it, which is what that word is for.
One was a real candidate, below. The list was not falsified — and no table came close to being a third kind.
Methodological note, because it weakens the second run: the classifier's signals were widened after seeing which tables fell through, and a re-run then left only the debris table. That re-run is a check on the fix, not an independent test. The first run is the test.
tenant_order_counter(tenant_id, last_number, updated_at) — a high-water mark that hands out order numbers. Delete the row and the next order reuses a number already issued: that is a second action, which is question three, which makes it a lock. But a lock is supposed to carry no cargo, and here last_number is what is being claimed.
The reading that costs least: a lock whose claim is a value rather than a row — which sharpens the lock archetype's rule from “no cargo” to no cargo beyond the claim itself. It is a noun, and a lock; nothing about it asks for a new kind, or even a new archetype. Recorded, not adopted. One example is not a pattern, and inventing a category from a single row is the failure this whole list exists to prevent.
Is Proposition 4's danger real in this system, or only conceivable?
Real, twice, in the most consequential table there is. contact_actions — the contact diary, 1.3 million rows, a river — carries two unique indexes that are locks:
contact_actions_pathway_pending — unique on journey_step_id where the row is PENDING and came from a pathway. One pending action per step.
contact_actions_idempotency_key_key — unique on (tenant_id, idempotency_key). The “webhook already handled” lock, verbatim from the companion document's own example.
Both sit inside a river that gets pruned. This is precisely the shape the rule forbids, and it was found by looking rather than by arguing. The rule is not hypothetical here.
Is there a river whose rows-per-subject is enormous and whose timeline is fine anyway?
The worst figures in the database are all enormous: contact_actions at a 99th percentile of 595,089 rows per subject, notifications at 123,632, action_logs at 101,032.
Every one of them is measured against tenant_id — and tenant is a mention, not a subject. Against the actual subject, contact_id, the diary runs at 84. The rule is not falsified; the instrument was pointed at the wrong column.
The unit measurement is meaningless until the subject is known, and both instruments were reporting it for every foreign key. Published in a report, “595,089 rows per subject” would read as a crisis and be noise.
The classifier had the same defect, and there it did real damage: reading the worst figure across every pointer, it called a 1.3-million-row contact diary a heartbeat, and inflated the heartbeat count from 7 to 46 — a third of the system's logs reported as noise. Caught before anything was written up, which is the only reason it appears here as a finding rather than as a published number.
Fixed, and derived rather than listed: a pointer that appears on most tables in the schema is a scope, not a subject. Here tenant_id sits on more than half of 270 tables and no real subject comes close. Both tools now resolve the subject first and label the rest as mentions. A noun, having no subject, has no unit either, and is filtered out entirely.
Does the subject test ever produce an answer a person would reject?
No — and it did real work in Test 3. What tells you the tenant figure is noise is the subject test: remove the tenant from “Levan paid £240 for the coaching package” and the line still says something, so tenant is a mention; remove Levan and nothing was paid, so the contact is the subject.
A definition cannot be false (§06). It can be useless. On 270 tables it was not. ∎
The point of the exercise, and the reason it was worth the afternoon. Four claims did not survive in the form they were written.
One — derivation presupposes loss. The arrow from events to state is only one-way because the derivation throws something away. A lossless copy of a history is a second river and inherits a river's rules. (Corollary 1.2.)
Two — two originals have a second cure. The impossibility result is relative to what the system retains. Record the writes themselves and reconciliation becomes possible again. This is what an audit log buys, and neither document said so. (Corollary 2.2.)
Three — state includes the future. Both documents describe state as “about now”. The dichotomy is between closed and not closed, and a forecast is not closed. The prose was narrower than the argument. (Proposition 3.)
Four — the lock rule is robustness, not correctness. A serialised rebuild does not violate the guarantee. The rule survives, and it should, because the failure it prevents is silent and returns unannounced — but it is an argument about how systems decay, not about what is possible. Stating it as a theorem was an overclaim. (Proposition 4.)
All four corrections are now in Rivers and Their Direction and Rivering, Step by Step.
Stated conservatively, because a claimed lineage is easy to overstate.
Proposition 1 is the standard motivation for event sourcing, rarely written as an injectivity argument. Proposition 5 is the time-of-check-to-time-of-use race and its usual remedy; nothing here is new. Proposition 3 has no name known to us, though the state/summary line is visible in practice wherever systems distinguish a live aggregate from a closed-period one.
Proposition 2 resembles the reconciliation problem in distributed systems, and Corollary 2.2 — that logging the writes restores decidability — is the same intuition that motivates causal metadata there. The resemblance is offered as orientation, not as a citation; we have not checked whether the correspondence is exact.
Proposition 4 we have not found stated anywhere, which is weak evidence of anything. It may well exist under other words.
One fact, two stores. The propositions are stated over a single system. When the same fact lives in Postgres and in Redis, “the original” is no longer a table but a store, and Proposition 2 needs restating over a pair of systems with no shared transaction. This is the sharpest untested edge, and it exists inside the system these documents came from.
The marks are not formalised. external and sealed each change exactly one rule, which suggests they are modifiers over a kind rather than kinds — but “changes exactly one rule” is an observation about two examples, not a definition. A third mark would either confirm the pattern or expose it.
Whether two is minimal. Completeness is addressed in §06. Minimality is not proved: could the river and the noun collapse into one? The argument that they cannot is nearly strong enough to be tempting — every noun but one is derived from a river, so perhaps everything is the river. It fails at one place: something must refuse. A river narrates what already happened, and refusing has to occur at the moment of writing (Proposition 5). Whatever holds the rule that refuses is doing a noun's job — the lock — whatever the table is called. The reference sets this out as “Two things a river cannot do alone”. That is an argument, not a proof.
The archetypes are not minimal either, and are not meant to be. The old flat list is where minimality was once argued: the heartbeat came closest to collapsing into the river, because it is a river. The two-kinds revision settles that by agreeing — it is an archetype of the river, not a rival to it.
On the register of this page. Proofs are not a claim to more authority than the companion documents have; they are a claim to less. A proposition with a proof can be checked and refuted by anyone. An argument can only be agreed with or not. Moving four claims out of the second category and into the first is the whole of what this page does — and moving one of them back, in §07, is the part that made it worth writing.
If any proof here is wrong, that is the most useful thing that could happen to it.