killed 16 stale buffer(s) (0 stream, 10 file, 0 render, 859
invoke, 1508 HTTP, 4 Dired, 246 temp); 115 remain.
That line is from a real system running right now: the futon-buffer-cleaner in Joe's Emacs, deleting unneeded buffers on a timer. It exists because on 2026-06-10 there were 6,502 of them. It is the predecessor of Inbox Zero — the same automated-hygiene idea, one generation earlier — and Inbox Zero in turn begat the test registry. Three generations of one neuron: buffer cleaner → inbox zero → test registry. This post is about the first, smallest one, because a question we cannot yet settle at the larger scales can be checked against truth at this one.
The bar, declared up front (the standard our September 11 post set, and the standard every worked example on this fork must meet): in that post's domain, a proof either elaborates or it doesn't — the answer is cut-and-dried. Here, a killed buffer either was needed later (a false kill: it gets re-visited, and that event is in the record) or wasn't. The verdict of any scoring rule we apply can be checked against that truth. If seeing both scoring horns compute on this cleaner makes one obviously right, the win must show itself against the declared rule below — not against our taste.
The cleaner is a small authored panel — fully automated, nothing asks the operator (this is the Zero Theorem's premise: the whole point is that it runs unattended). Two wirings of the same chips:
The noise attribution is the whole shape of the problem. A temp buffer whose process has exited is a decisive channel — killing it is certain-safe; there is nothing uncertain to model, and no honest score invents noise there. A file buffer you last touched three days ago is genuinely uncertain — "stale" is a guess about the future (will you need it again?), and that uncertainty is real. The two wirings differ only in how much of the genuinely-uncertain channel they act on.
Correct wiring = the one that reaches the clean-enough buffer state (remaining count below a declared threshold) at least total cost — where false kills are charged their measured revisit cost, and total cost is each horn's G-terms plus fuel. The reader checks each horn's pick against this rule; the rule precedes the numbers.
Data source, declared either way: if the logged history can yield revisit counts (which log, what window, what counts as a revisit — the derivation shown in full), the false-kill costs are measured. If it cannot, the post uses constructed parameters, labeled as construction — never quietly invented numbers. The choice of data source is part of the declaration.
Horn B — the book G. Each cycle contributes its risk against the preference (clean-enough state, few false kills) plus the entropy of each observation channel as the channel is: decisive temp-observations are sharp and contribute nothing; the stale-age guess contributes its true uncertainty, per buffer judged.
Horn A — the illustration. Push likelihood and preference onto the task outcome (buffers cleaned, kills false or true) and exclude channels that are noise about something else. Here, as in the registry, the question is whether anything legitimate is excluded: the stale-age uncertainty is not noise about something else — it is the risk itself. So the horns are close in this domain, and where they part, the parting is exactly the question.
All probabilities, revisit flags and costs are constructed and labeled as such — the real log line is motivation, not measurement, and §4.5 below says why it cannot be. One cycle is one scored endpoint (T=1); 24 buffers with per-group needed-later probabilities and recovery costs; preferences encode recovery cost; fuel = 0.01 per scan + 0.1 per kill. Every number below is produced by an executable script with identity checks, committed alongside.
| wiring | remaining | expected recovery | book G (Horn B) | G, Horn A (illustration) | fuel | predicted total | realized (constructed oracle) | rule says |
|---|---|---|---|---|---|---|---|---|
| aggressive | 8 | 7.225 | 10.733 | 10.733 | 1.84 | 12.573 | 17.84 | eligible, loses |
| conservative | 16 | 0.500 | 4.008 | 4.008 | 1.04 | 5.048 | 6.04 | eligible, wins |
Both wirings reach the clean-enough threshold; conservative wins under the declared rule, and the constructed oracle — which selects by realized recovery-plus-fuel, not by either horn's score — agrees. Both horns' predictions match the oracle on this outcome. The aggressive wiring's price is exactly where it should be: not its decisive temp kills (free, as they must be) but its stale-file kills, whose constructed revisit exposure (7.2 expected recovery) dominates its savings.
In this domain, the two horns coincide. The A illustration can only project away deterministic bookkeeping; the genuine revisit uncertainty stays, so its scores equal the book's at every cell. There is no injected coin, no provably-irrelevant channel, nothing legitimate to exclude. That is a finding, not a failure: the A/B fork only has work to do in models that carry noise which is irrelevant to the outcome — and this example, built with per-channel honesty, has none. Where the horns differ, they will differ precisely over whether some channel's noise is excludable; the buffer cleaner cannot exhibit that question because it has no such channel. A distinct full-A formula remains blocked on its mathematical definition, not on arithmetic or a bigger example — we have not invented one.
The constructed parameters above stand in for measurements the real system cannot supply: the cleaner's report counts candidate attempts per category while its total is a net count difference — the "16" of the log line is not a per-category successful-kill census — and nothing retains buffer identities joined across kill and reopen. The cleaner has no way to know its own false-kill rate. To be scored on real data it needs a retained buffer-identity / kill / reopen history and a declared revisit window — the same warranty-carrying record every other part of this stack learned to keep. That gap is now this post's most practical finding: before any live tuning of stale-age thresholds, the cleaner should learn to remember what it killed and whether that was regretted.
Joe's answer to the Stage-0 semantics question was not a ruling between the horns but a property of the computation itself: a cascade should be suited to the domain and constructed progressively, so G is defined over cascades IN ANY STATE OF COMPLETION, and EFE should be minimised. If increased length caused G to increase, then length should not increase; if G decreases, extend. This follows from "minimize EFE."
What this does to the A/B question: the fork asked which global formula prices length. Under Q1 there is no global choice — length is decided by the score itself, during authoring (see §7 for what is being authored). The candidate design is extended step by step; at each prefix the author asks whether the next pattern lowers G; the design stops when it does not. The question that survives is not "which horn" but the channel question each step poses: when G is computed on a partial design, which observation channels enter — decided per channel by whether its noise is about the task or about something else. The buffer cleaner demonstrates this natively: score each candidate reconstruction at each authoring step (observe → classify → kill → yield), and the progressive property is visible — [PENDING codex-26: prefix-scored G for each authoring step of both candidate reconstructions, showing where extension lowers G and where it does not].
An earlier draft of this section read "per-problem" as per-cycle: the wiring re-formed from current state each run. Joe corrected it: what we are doing is forming a RATIONAL RECONSTRUCTION of the buffer-cleaner CODE from patterns. The reconstruction is authored once; once written, the code has the same deterministic functional behaviour — the specific functioning varies with the data it is given, but the wiring does not vary. "Cascades are formed per problem" is about the authoring act — the ARGUE-phase analogue at design time, per problem-domain — not about the runtime re-deciding its panel.
So the two wirings in this post are two candidate rational reconstructions of the same underlying cleaner capability — competing authored designs (what an aggressive vs a conservative reconstruction looks like) — compared as designs. The progressive property of §6 scores authoring: a candidate reconstruction is extended while EFE falls, at design time; the chosen code then runs deterministically on whatever buffers arrive. The partial-cascade requirement is about scoring designs mid-authoring, not about runtime plasticity.
[PENDING: one worked authoring — the design-time argument that produces the aggressive reconstruction, step by step, as the ARGUE-phase analogue: which patterns the reconstruction draws on, why, and where EFE said stop.]
Joe has no opinion on these; we work them out HERE, by argument and example, in the buffer-cleaner domain once the adapter passes re-review: