No LLM generated, assisted/co-written, or edited work.
Read full explanation
Konrad Wojnowski
Epistemic status: the formal system behind this essay (VOID Theory) is finitist and machine-verified in Coq: roughly 755 Qed-closed results, zero Admitted, six named axioms, none of them about inference. The central computational claim, that a population of finite observers competing under scarcity lands within 3.3% of the Bayesian posterior without Bayes ever being applied, is a machine-checked theorem about specific fixtures rather than a general convergence result; Chapter 7 marks exactly where that line falls.
The narrative framing is subjective and meant to be: the theory is presented through the lens of 1) rave experience; 2) unusual process of writing which took place during author’s struggles with terminal illness. To write in this way was not arbitrary. I have never wrote in such a way and felt motivated to express my thoughts in a way that is no longer practiced in academic circles. But given that from matters concerning authorship to how progress involved entanglement of developing new theorems, shifting perspectives on completely abstract problems, a fair share of melodrama, and progression of my bone cancer, it felt only right to find an expression through a bit zany style.
For those readers who want the experiment without the night I advise reading the first part of the introduction and Chapter 3 where I have presented my arguments using traditional stylistic means.
Bayesian updating is not a law of rationality. It is a side effect of finite systems competing for resources.[1]
This is a strong claim, so I will try to be as precise as I can, whilst entering the minefield of potential exaggerations – to which I am prone – misrepresentations of adversary positions, or poorly chosen words on my behalf. So I will attempt to get these out of the way: no, I am not claiming that Bayes' rule gives wrong answers; yes, the Dutch book argument stands; Cox’s theorem stands; the complete class theorem stands. These are beautiful results with which I do not want to argue. What I will be claiming is that they all prove Bayes' rule in a uniquely correct updating procedure given a certain picture of what an observer is. However, this picture becomes impossible at two layers when we approach matters: 1) physically, because it asks for resources no real observer has, and 2) mathematically, because it is built on a substrate that quietly assumes infinity at every step. And no one has yet found an infinite phenomenon in the universe. Even black holes dissipate…
This picture was construed before the avant-garde disassembled the paradigm of academism and its adherence to realist representation: an observer with a prior distribution, infinite precision, free computation, unlimited memory. Not someone you encounter on a regular basis, or even once in a lifetime. The exemplary observer receives data, multiplies prior by likelihood, normalises, and obtains a posterior. The multiplication is exact. The normalisation costs nothing. The observer can hold arbitrarily many hypotheses simultaneously and update them all in parallel, at zero cost, forever. This is well-established and defended territory of the Infinite Observer. The One who sees everything for the price of nothing.
Paradoxically, this picture with The One looking, became questionable exactly at the peak of academism in art: when dirty thermodynamics – oil, coal, and sweat of the factory worker – entered the grand and crystalline palace of the Science. Yet, we still live by the code of the ideal world where we operate on simplifications, averaging, and continuization. In that world the observer violates thermodynamics as much as they want. We work hard to remove all traces coming from the engine room. And we have gotten used to accepting this as the Norm that does not need to be questioned. However, every real computation runs hot and burns joules. Every comparison takes time. Every memory cell occupies substrate. A real observer has a finite budget, and every act of observation drains that budget irreversibly. When the budget runs out, observation stops — not because the observer decided to stop, but because observation is a physical process and physical processes require fuel. As I was working in isolation, only with AI as my ever-changing companion, I can attest that computers are quicker to admit that. Maybe because they naively have not fully grasped the consequences and each AI model I was working with had to come to terms with this moment of painful anagnorisis: in a thermodynamic universe, you die. They do not share our common fear of death, but, time and time again, without blinking I brought them the news – hardware dies too. We, humans, are struggling with accepting this fact since the dawn of civilization and almost certainly longer than that. People never made peace with this unyielding fact of nature, so they build all those cathedrals of the infinite again and again, only changing the facades: from baroque to brutalist. Sometimes it takes a whole set theory to stop anxiety creeping into your nervous system.
A word of reassurance before we go further. If you’re worried that this essay will stop at criticizing this state of affair, rest assured. Not only will I propose an interpretation of Bayesian probability from a finite point of view, but also take you on a tour with 24-hour party people through the first real implementation of a finitist mathematical system. That label, and the word "gem", came from Doron Zeilberger, who read the formalism after it had been through the unforgiving, all-seeing eyes of the Coq theorem prover.
But I'm getting ahead of myself — let’s add few infinities more to the mix. The observer also violates the substrate. The reals are an uncountable completion of the rationals. The σ-algebra is closed under countable union. The probability measure maps an infinite collection of sets to an uncountable continuum. The observer's representation of belief is an element of an infinite-dimensional function space. Strip away those layers and the textbook statement of Bayes' rule has nothing left to compute on. And, as I will try to persuade you, the infinite real line, the σ-algebra, the integral against Lebesgue measure — all of these are artefacts of a foundational choice, not some fundamental features of reality, dug out during excavations in Upper Nile. Specifically, it was a choice to start mathematics from ℕ, complete to ℝ, and build probability on top of measure theory. Strip ℕ and the rest has to be rebuilt from different materials. That is a claim about foundations, not a refutation of anything built on them. And ℕ stands on Peano succession and its naively ironclad logic: you can always add one, right? Such simplicity raises an eyebrow and forces me to doubt. Working in complete isolation, as I was forced to do given my severe illness introduces a lot of space to doubt things. Most solid things just melt into thin air. You hear this once certain “Just add this damn one!” as a faint echo. So is the problem solved? Is the case closed? Well, I decided to re-open the casket and doubt. Funnily enough, the hieroglyphs were decoded in 1822 — and by 1824 Carnot had shown that every engine pays more than it delivers. The excavations did turn something up. It just wasn't infinity. Despite the medium being there, we still haven’t heard from the pharaohs.
Irony aside, none of what I just stated makes the aforementioned theorems wrong. It makes them theorems about ideal observers – observers that exist in the same mathematical elsewhere as frictionless planes and perfectly elastic collisions. And just as Newtonian mechanics is enormously useful despite the nonexistence of frictionless planes, Bayesian reasoning is enormously useful despite the nonexistence of ideal observers. I just tried to forget them for a moment. That moment took me on a weird journey — one that has, by now, grossly exceeded both my expectations and my life expectancy, and gave me no idea of what I was stepping into. The question I settled on whether there is a more fundamental account: one that explains why Bayesian updating works, rather than proving that it should.
I believe there is. And the explanation is thermodynamic. Hence my obsessive returns to the term — it is not a flourish; it is the load-bearing word. Which is why this text will not only present axioms, theorems, and proofs, but also weave them into a deeply material, corporeal story about rave culture and postindustrial rhythm. The good ol’ days raves in late 80s and early to mid 90s constituted – and sometimes still constitute – unusually pure thermodynamic environments: finite architectures of synchronization, repetition, exhaustion, heat, and probabilistic entrainment. They are spaces where bodies continuously spend energy in order to resonate together; maintain alignment with signal, rhythm, and collective expectation. And, importantly, not unlike thermodynamic system, they sometimes misbehave and make room for very improbable things to happen — and my personal experience will be crucial in showing how unlikely events can occur in restricting, raw, and minimal spaces. After a day in a library you just have to overextend and overestimate your capabilities taking a turn towards a club instead of going to bed.
SPOILER ALERT: some of my first intuitions about probability - intuitions that would eventually develop into a mathematical project - came to me on the dancefloor of Berghain, the eponymous club in Berlin that still attempts, to some extent, to preserve the atmosphere, values, and forms of emergent behaviour of the old raves by organizing parties lasting thirty hours or more inside the postindustrial, imposing concrete shell of a former power plant. Like many buildings in Europe erected after the end of the Second World War the traces of post-war collective Cold War paranoia still resonates between concrete walls and fragile bodies, of course, if one pays attention, or lets one's mind reach for a transgenerational link (and in that deeply traumatic). No direct sunlight. Space – its magnitude, rawness, dim lights protected by metal cages – bring to mind ancient spaces where death rituals took place and create ambience so imposing that one wonders if by the bar one should pay in Oboi.
As the time passes sweating crowds of freaks, misfits, and obsessives fill this space. They are here to enjoy freedom in the strangest ways imaginable adding to the feeling of participating in something that once was a common collective experience but became tamed by more cultured, Apollonian forms of conduct. Yet despite the genuine diversity and preposterous oddity of those who came here, these meetings produced remarkable flock-like behaviours, moments of uncanny synchronization in which collective rhythm seems to suspend ordinary exhaustion and gives people the fuel to continue for twenty-four hours straight — including surreal encounters such as meeting a Slovenian student of Slavoj Žižek in a packed bathroom stall spending my energy budget for discussing philosophy and at the same time caring for resources when attaining the "just for one hour more" will become increasingly more difficult. And night was still young, 10 am or so, only 10 hours in.
A word against the obvious suspicion. I use my own case not because I find it so interesting, but because I am the only finite observer I can report on from the inside, and this essay is about what finite observers can afford. Everything else I would have to take on hearsay. Where the personal material runs out, I switch to allegory: tableaux vivants from the floors of the years when the Berlin scene was working out what it was, socially and physically, and the occasional fragment from the history of Tresor, literally "the vault", which opened a few years after the Wall came down in a city then overflowing with abandoned infrastructure and improvised forms of collective life. There will not be much of this. It is scaffolding, not subject. In this sense, they compress together the two dimensions of thermodynamics most relevant to VOID Theory: energetic expenditure and statistical ordering under constrained resources. The dancefloor is not merely a cultural metaphor appended to the mathematics. It is one of the clearest embodied examples of finite observers stabilizing themselves through costly synchronization inside a bounded environment. In case the whole choice of setting still looks like a stretch: Andy Clark, who did more than almost anyone to put prediction at the centre of what minds do, is himself a raver. I am not the first person to notice that a dancefloor is where prediction goes to be tested.
And a very important piece of information about the background - or, rather, the essential part of my work which is not solely explanatory or philosophical. Over the past two years, I have been building a formal mathematical framework - VOID Theory - implemented and verified in Coq. It is a finitist system: no natural numbers (replaced by an inductive bounded type), no free comparisons (every arithmetic operation costs one tick of budget), no free knowledge (every observation produces irreversible entropy). In this framework, I set up an experiment. Three finite observers with different hypotheses, fed a stream of signals, competing for limited resources. No Bayesian formula is invoked anywhere. No prior is specified. No likelihood function is defined. The ravers simply dance, pay the cost, and retain resources proportionally to how well they matched what they observed.
After five signals, the resource distribution across the observers converges to within 3.3% of the Bayesian posterior.
The result is machine-checked. The trajectory is a Coq theorem, closed by Qed. And it suggests that Bayes' rule is not the foundation of rational belief — it is a corollary of finite observers competing under scarcity. You do not need to know Bayes' theorem to update Bayesianly. You need to be finite, to observe at a cost, and to exist in competition. The rest follows. First, a short story about the author, his place on the socio-political map, his habitus, and how the theory came into being.
Then, an exposition of the experiment and the theory through the metaphorical landscape patched from fragments from author’s biography and a probabilistic reading of rave culture.
Science as if it was written by the likes of William Burroughs but with all theorems checked by an automatic theorem prover. Trashy, unlikely, and painfully honest. Give it a try!
However, if you have no patience for stories with a thesis: Chapter 3 is self-contained, no metaphors, no allegorical story-telling; straight to the experiment.
Chapter 1 — The Entrance
The Short, Completely Unlikely and a Bit Dodgy Story of the Emergence of Finitist Math
Almost certainly the night will end, and so will my capacity to dance. I am on borrowed time, and on Monday it is payback time. It’s still Saturday, 11.30 p.m. The gates will open in 45 minutes. Everything is going according to plan. Today I am going alone. Bottle of club mate with added Jägermeister in hand to take the edge off. Long black coat. Wife-beater style tank top. Very loose jeans. Steel-toed Dr. Martens on feet. 70s style. Poseur? Sure. I am an academic after all. Yet, this style mixing of subcultures and my position among the high brow creates a mix that is true to itself. You would have found me dressed in far more outlandish clothes giving lectures and leading seminars in the Renaissance milieux of Jagiellonian University. I am a freak and I want people to know. The surrounding world is drab enough and standing out where I come from becomes an act of defiance which I can assert with a degree of certainty by the many hostile acts I have experienced by just walking the streets of Cracow dressed like a post-punk parrot. Being political, my unusual choice of clothes always had a lot to do with probability. Subcultures are dead. I am not pretending to be a punk. I am not pretending to be anyone in particular. The person you see is actually improbable in 2025. An academic among ravers. A smalltown boy who finished Polish philology and works on a finitist mathematical system. To top it off, doing all that while suffering from an extremely rare form of one of the rarest and deadliest forms of cancer: osteosarcoma.
So, no. None of this is metaphor. The math system I came up with was always bound to be finite — by being, itself, a body: the observer carrying a budget. My body, throughout the work — cancer and all — reminded me of itself at every turn, and I tested how far it could go, which helped me leave Spuren of intense transgression and pursue the most blasphemous* ideas, like a non-metric distinguishability function. There are traces of my material existence — counterweights to the solitary work I had to endure for long stretches. I paid for them later.
The honest version is this: I am a humanist. I know what mathematics is about, I know its philosophy and something of its history, and I cannot write a proof to save my life. I can read one. I can tell you what a definition commits you to and what it quietly smuggles in. Put a blank page in front of me and ask for a Fixpoint and nothing comes out. So the only road from what I had to what you are about to read went through dialogue, and the machines were not my collaborators in the sense that worries people. They were translators. I spoke in the intuitions of a body and they handed back syntax, and then Coq told us which of it was false.
Those intuitions were not decorative. I have never treated philosophy as commentary on the world, as something you hold at arm's length and grade, but as a set of claims that might simply be true — and a claim you treat that way does not stay in the head. It gets written further down. It leaves traces deep enough to cross the border between mind and body, assuming there is one, which is itself among the things I no longer believe. And then, with death first approaching and then withdrawing and then approaching again, in the fire of what I have to assume were the last real outbursts of the will to live, this body of mine, written over with twenty years of philosophy, began spitting out the concepts of a system it had apparently been carrying the whole time. A system aimed at infinity.
I set the ontology and the refusals, no actual infinity, no free distinctions, an observer who pays for everything, along with the questions a dying body insists on asking. I chose the six axioms. I decided which conjectures were worth attempting, and I threw out every definition that did not do the work I wanted done. What I delegated was the part of mathematics that is search: candidate formulations by the hundred, proof attempts by the thousand, the mechanical patience to be wrong faster than a person can stand. This is not a novel arrangement, it is what a proof assistant is for, and it is why nobody lists Coq as a co-author of the Feit-Thompson theorem.
And above all of it, the cold and unforgiving eye of Coq, rejecting everything that merely sounded true and never once caring what I had meant. There is an irony in the arrangement that I did not choose and cannot escape. Coq's own type theory is infinitary. The moment I write Inductive Fin, I have been handed infinitely many values to play with, and the language in which I prove that no observer can afford infinity takes infinity as its floor. My objects are finite; my metatheory is not. I take this as a fair price rather than a defeat: before you are allowed to drift into a field of your own, you should be made to show that you can play by the rules everyone already agreed on, in their language, on their terms.
One consequence is worth putting on the table before you decide how to read what follows. I can open any theorem here and check any local step, but I cannot hold the whole thing in working memory at once, and neither can anyone. That is the ordinary condition of a machine checked corpus this size; it is equally true of Flyspeck and of Feit-Thompson. The compensation is that it no longer needs to be held. It has been checked.
I paid with scarce resources left in a very sick body, yet one that chose Dionysian drama over meditative self-care — especially after a job that was the least physically engaging and varied imaginable, at least in movement and emotional stimulation. Yuval Harari would not approve. Choosing death in the name of life. What difference does it make after all?
The theory, the one I am writing about at this very moment, has its actual and symbolic roots at that party. Then the theory could grow — and it brewed slowly at first — giving birth to my book about probability theory and avant-garde art. Later, a few years, in fact, just as the AI revolution reached a state allowing me to translate my understanding of the probabilistic revolution in science and how it reverberated in the aesthetic ideas and creation of artists I could transform them in a way I never even dared to imagine. In conditions of chaos and transgression, with a terminal diagnosis in the background, coinciding corporeal and emotional crises led to the most important breakthroughs in the work. My last ties to infinite concepts and values were eradicated by sudden ruptures of despair or euphoria that reminded me of the biographies of those avant-garde artists who became main characters in my book and were among the last to dare probabilistically: sacrificing meaning for improbability.
Without the deeply corporeal and mind-altering – in the unusual sense of radical brain numbing, no psychedelic expansion whatsoever – experience that took place that night, I probably would not have reached the conclusions that came to me years later. Years later, when through a ketamine-opened wormhole – ketamine allows for creating these almost perfect snapshots of time-space and travel back to them almost at will, provided of course that you are again under the influence of the drug, which is state-dependent recall, a dull and well-documented thing wearing a spectacular costume – I connected with this moment, with me in my most primal, primitive state, I could work not from the level of abstraction but from a deeply embodied state that I shared with an alien intelligence. An entity that excels at translating from one language to another. From French to English. From a report of my body to probability theory. Such translation yields results quite different from those a solitary mathematician would reach staring into the white void of the LCD panel of his old school computer. Or an OLED one displaying results crunched by the newest super-machine bought from a grant that had predicted the results before the research even began! This gave me an opportunity to draw different conclusions from a concept already circulating in human culture: math existed before math, as forms of neural management and early electro-chemical computation.
And there is a paradox here worth admitting openly. VOID Theory is, at its core, tied to the human — to the body, its veins and nervous pathways, its finite budget of energy and attention. And yet it grew up in Coq, one of the most hostile environments a human being can write in, a place where nothing passes on good intentions and every little step must be justified to a machine that has never once been charmed by an argument. No feedback from Terminal’s UI – sign that no error was detected – never tasted so sweet. A paradox: a kiss of relief in the form of an undelivered message. Worthy of psychoanalytic investigation. So the theory grew up there, in a language built for machines, with machines doing the searching. This origin left a mark. The result is not well suited for human use. You won’t teach it in primary school; you won't teach it in secondary school either. University at the earliest, and even then to students with a taste for formal punishment — the complexity bar stands that high.
But here is the asymmetry that matters. It is not that formalization is easy for a machine; it demonstrably is not. It is that a machine does not get tired, does not lose the thread on page forty, and does not have a working memory that fills up and starts dropping things. What exhausts a human reader is not difficulty. It is duration. And duration is the one cost these entities do not pay. So the theory of the living body turns out to be most legible to entities that have none.
What you get, then, is an inhuman theory born from the most human of circumstances: a finite, dying body; a moment of complete dissociation and bodily collapse; a long human-AI dialogue that ran through the most turbulent season of my life, with death – and passionate love, the last bastion of infinity in my mind to fall – standing close enough to influence every twist and turn of its development. Nothing about it was planned the way theories are supposed to be planned. It is weird. It is improbable. It exists anyway. And it compiles.
This is the shortest version of VOID Theory's genesis I could have offered you — the trailer, not the film. I have no intention of turning this essay into an autobiography; but the metaphors I will be leaning on had to be shown first in their natural habitat, with the dirt still clinging to their roots. This essay aims at two birds while I hold a single stone: it presents a theory, and behind the theory, half-hidden, a life story — engaging, tragic, and unfolding in the very middle of a great civilizational shift. The romantic thread I am keeping under lock and key; trust me, though, there is material enough in it for a full-blown romance in which mathematics and AI would be demoted to scenery. And atop it all sits the most improbable fact of the entire affair: the math works — Zeilberger confirms it — which may be the strongest testament to the mind-bending uncanniness of those months. It is also the ultimate source of this essay’s slightly chaotic architecture. Every time I try to fold the process into some elegant shape, it twists and slips out of my hands like a wet fish. It was not elegant. It was violent. It was chaotic. And if I am to remain honest with you, Dear Reader — and honesty is the one luxury I can still afford — then I owe you the chaos itself, not a pressed and dried flower of it.
And so it all began on the dancefloor, in — frankly — a concerning state health-wise. I will return to it in detail in Chapter 6. For now I will say only that it nearly cost me everything and it gave me the book, and that I have never been able to separate the two. There is always pleasure to be had in predicting well, in predicting wrong, and even in hovering over the ground in perpetual BUnknown.
And none of it is free. Every distinction — her face out of the strobe, the drop out of the build, your pulse out of the kick — spends something you don't get back. The heat lifting off you isn't a side effect; it is the spent budget, conserved to the last unit, leaving your account as it warms the room. To tell two things apart, you pay. That is no_free_lunch, and the floor takes one currency only: heat, which is time you won't get again.
Monday isn't punishment. It's the second law. The budget only falls, the night runs away, and you cannot dance it backward — time_irreversible, not a fact about clocks but about you: on the way out from the moment you walked in. You will ignore this, of course. Your body knows its track record and will spend against it anyway.
This is the observation point. Every probability, every shape, every unlikely thing still to come is seen from exactly here — a finite body, spending, on a floor that closes. Not a cage. Somewhere to stand.
Before describing the experiment, I need to explain the formal substrate it runs on, because the substrate is the argument. VOID Theory is not a simulation. It is a proof system. Every operation is type-checked. Every theorem is machine-verified. There are roughly 755 Qed-closed theorems, six explicit axioms (concerning the internal structure of arithmetic and measurement — none of them about Bayesian updating), and zero Admitted, which is Coq's term for "I assert this but haven't proven it." The system compiles. The proofs terminate.
One thing follows from that, and it is the only reason you can read this at all: the system does not require its reader to reconstruct it. It produces theorems that can be checked, behaviours that can be observed, and consequences that can be discussed in ordinary language. The Coq is there for the verification; the prose is there for the meaning.
A last note, on framing. I am not arguing this system against standard mathematics, and I see no reason both cannot have their place. What VOID gains is honesty about its own commitments: it refuses Lebesgue measure on uncountable sets, σ-algebras closed under countable union, real-valued plausibility, limits whose convergence is only ever assumed — and it proceeds without them. That it keeps working anyway, reproducing the classical results to within proven error bounds while several long-standing problems either dissolve or reframe into something the substrate refuses to even state, is the whole practical argument. Infinity is a choice. Where I compare the two directly, that is a pedagogical move and not an attack. This essay is about what becomes visible once you walk into the other one.
Chapter 2 — The Wristband (Substrate)
Or, How to Get Inside Berghain, the Truth Finally Revealed And Supported By Revolutionary Scientific Theory
Let’s get back to the line stretching on a dusty field surrounded by nothing but bent bars of fences protecting warehouses and parking lots. Space giving Mad Max vibes at the heart of Berlin – a little void in historical time and space. The hour strikes, the gates open, the queue creeps forward, and an eerie silence takes over the audiosphere. Nobody wants to make a stupid move that ends the night before it has begun and sends them off on what is commonly referred to as the walk of shame, back along the whole length of the queue, past everyone pretending not to stare. But we stare. We all stare.
Everyone in that line is working, those who are just standing with nonchalance are maybe the ones that work the hardest. Reading the door – who will be the judge jury that night – reading the group three places ahead, reading themselves, running it all again. By the time you reach the front you have spent an hour of uninterrupted computation on a decision that was never yours to make. And what about the fools? They are the ones making noise: cutting the line, shouting merrily, catching a bouncer's eye before their turn comes, showing up in groups larger than four. They are not calmer because they know something. They are calmer because they are not spending anything on holding themselves in. Everyone else in that queue is paying to suppress; the fools pay nothing for it and emit everything instead, handing the door a complete record of themselves before they even reach it. Barely a handful squeeze in, and purely by chance. Sometimes letting things unfold at random does produce a result, and there has to be an outlier to the outliers too. Their existence is not an accident but a statistical necessity: make the line long enough and somebody gets in who should not have, while somebody who did everything right is sent away. Which is the first useful thing the queue teaches. Nobody standing in it is at zero and nobody is at a hundred. Both absolute endpoints promise a totality that never arrives, and it is high time we had an alternative.
Almost everyone knows the basics and everyone performs good manners and mostly false modesty — the freaks, the tourists who learned only that morning that one dresses in black and paid a hasty visit to H&M, even the cockiest poseurs who everywhere else would be presenting their muscular masculinity in Rick Owens and Balenciaga, now stand with their eyes down and their mouths shut. They all intuit, without the vocabulary for it, that the queue is one long Bayesian update — that every fidget, every glance, every too-eager step is evidence, and that evidence, once emitted, cannot be taken back. Those who break the line rarely escape attention; they are marched back to its end, most likely to be rejected all the same. The Berghain line is a place of many myths, occasional violence, and pure epistemic uncertainty. Every rule exists shrouded in fog, nobody knows anything for certain — and VOID Theory has a name for this state, not as metaphor but as a line of code.
Now look at the line again, but this time check your pockets. You are not waiting for a verdict — you are paying for one. Even if I never got rejected, my body keeps sweating, I tremble, I feel weird and unshakeable tension for hours already, I want to be there but always end up in a perpetual state of BUnknown. Maybe this is the trick? To never stop doubting? And the tremble of uncertainty is the cost I had to pay for getting in. Never letting myself take too much edge off with too much booze or whichever drug was on the menu that night. The hours on your feet, the warmth leaving your body in wintertime, the battery percentage dropping on the phone you don’t dare take out: all of it is fuel, and the meter has been running since you joined. Nobody in this queue is idle. Everyone is spending — there is no such thing as just looking (no_free_lunch_le: every comparison run on a positive budget emits a nonzero trace).
And what has been spent does not vanish in thin air — it converts into Spuren. It is a counter of the same finite type as the budget, incremented once for every unit spent, and the corpus proves that at every step Spuren plus remaining budget equals the budget you started with — so it is not a metaphor for a trace, it is the ledger.
Every half-glance, a sign of my unwavering wavering, every fidget the bouncers read not as a gesture of showing off but of honest modesty. They somehow can tell that I am one of those who will not only make himself comfortable inside among the guests but will also essentially turn into one of the hosts who won’t ever cross any boundaries, the undefined ones too. Reason: these are the people who crawled out of the cracks in the system — its residuals, the remainder left when society rounds itself to the nearest whole — and cannot converge; and why should they? Freaks are penalized at every iteration of capitalist rule, raised under the bourgeois dictatorship of families run on a micro-Benthamian order: one observer, total visibility, correctness the only admissible value. Such households manufacture the one-dimensional man: a person reduced to a single coordinate, for whom every question has exactly one answer and being correct is the only direction motion can take. But nobody is born that small. Whatever in the child refuses to fit on the axis survives as a remainder — and that is what a freak is: a fractional person, the part that society’s floor division was meant to discard. Not discarded, strictly speaking. Unrepresentable. There was no way to write them down in that arithmetic.The integer parts stayed home, employable and correct. The fractions had to go somewhere, and they came here. That is what the door is really scanning for — not the outfit, the remainder. Whole numbers do not get in. All of it – the half-glances, the fidgets, the readable modesty – receipts. Call the fuel Budget and the receipts Spuren, and you have the entire substrate of VOID Theory.: every operation, from a bouncer’s once-over to a comparison of two numbers, has the shape budget in → result, smaller budget, trace out, and the books always balance to the last tick (spur_conservation_le3: add_spur h b' = b — trace plus remainder equals what you walked in with).
So what is the budget, concretely, here in the line? Not calories, though it runs on them. A tick — one act of telling two things apart. Look at the two silent men by the wall. On the left, a man perfectly still, untroubled, running nothing. On the right, me: also still, also wordless — and spending like a fire. I am metering my own silence, timing when to lift my eyes and where to put them down, auditing every glance I permit myself against return-protocols installed decades ago in that single-coordinate household. Same posture, same silence, two different ledgers: his stillness performs no operations, and what is never run is never billed; mine performs hundreds a minute. I am not bragging. If I were to boil down the reasons for this operational overload to one, it would be heavy neuroticism and anxiety. No glory in that. Neuroticism raises resolution, and resolution is the multiplier. The finer your grid, the more every look costs (resolution_cost, void_probability_geometry.v: one further layer of depth costs exactly one tick), and the traces you keep alive between looks are billed every tick just for being maintained, at a rate your resolution sets (total_maintenance_cost, void_attention_cost.v: in this system maintenance is charged by construction, not derived). Note what this does not mean: low spending is not wealth. A vacant tourist in a fresh H&M black isn’t richer than me — he is cheaper. His budget may be minute, he just does not introduce too many dimensions which cut any problem to more pieces; his resolution never asks for more, so he’ll never find out. Poverty is invisible at low resolution. And the cruelest line item on my side of the ledger: checking whether my own silence is holding is a measurement on the diagonal — my budget asking about itself — and that question, by theorem, never resolves. It only bills.
Which forces the question classical logic never has to ask: what does a system return when the meter hits zero halfway through a question? Two-valued logic has no slot for this – it assumes every verdict is already lying somewhere, fixed and free, waiting to be read off. But if verdicts are produced, and production runs on fuel, then an unpaid question has no secret answer in storage. The logic must say so, in its own type: BTrue. BFalse. And BUnknown — not “maybe,” not a probability, not your private ignorance of a fact the world already settled. The output of a procedure that ran out of means. Ask the system anything with an empty budget:
No verdict, nothing left — and, note the third slot, not even heat (silence_is_free: at zero budget, and only at zero budget, a question emits no trace). The queue knows this state intimately: the night the club filled before the door ever looked at you. You weren’t rejected. You were never computed.```coq le_fin_b3 n m fz = (BUnknown, fz, fz)
And a pill tough to swallow for the gate-stormers: they are not rich. They are unaudited. Nobody in this line knows their own balance — that is not a fact about drunkenness but a theorem: checking how much you have left is itself an expense, and it costs exactly one tick more than you have (self_blind: le_fin_b3 n n n = BUnknown — a budget of n cannot afford to verify n). Everyone queues in front of the same blank where the number should be. The difference is what you do with the blank — and the line, seen properly, is a row of spending profiles. The blank-sighted tourist barely draws on his account and will never learn its size. I drain mine in a thousand micro-comparisons a minute, each one metered, none of them resolving. And the fool does not read the blank as plenty. He gets a hard answer, and the hard answer is no: collapse3 sends BUnknown to false (void_finite_minimal.v), the verification fails, and he moves anyway, on a gesture cached long before tonight. This is the System 1 of void_dual_system.v, and the file makes a claim about it worth pausing on. System 1 is not chosen because it is fast and cheap, which is how it is usually told. It is what you are left with when the price of checking exceeds what is in the account. Kahneman had the two systems right and the reason backwards.
And the night bills him in full. That is the fine print of spending in VOID: order more than you hold, and the ledger does not politely truncate — it records the entire ordered cost, drains you to zero, and books the difference as debt (spend_aux_spuren_equals_cost: Spuren equal the cost ordered, not the cost afforded; the shortfall is epistemic debt). He bought nothing. The receipt is complete. The walk of shame is what it looks like to carry a full invoice for a purchase that never happened.
2.1 One type.
Start with the kick. Four-to-the-floor does exactly one thing, plain and simple. It pounds. One step at a time. Strict adherence to the 4/4 rhythm is not a sacred rule — just the most common practice. What counts is that it spaces those pounds with clinical regularity. Tick after tick. The rhythm of the machine. Techno is a late child of the Industrial Revolution (the first link to thermodynamics). It forms a rectangle: four beats, four bars, repeat. Sounds like a cage? Well, techno has never enjoyed a good reputation among those who never attended a rave party – it is just extremely difficult to put oneself in raver’s shoes as the experience is so different in terms of intensity, lack of meaning and purpose; pure and empty budget spending involving substances that have been painted as dangerous and the whole edifice as something morally corrupt. Just take a look how mainstream cinema paints rave parties – I can assure you that these depictions have nothing to do with how those events really look. A good rave is never full of neon lights; rather, it is poor and a little bit dirty, what counts are the relations that are being formed, it is the music is being played; even inside Berghain, which became, in reality, quite luxurious event (20 euro solely for the entry, 10 euro for a drink, these are not prices set for the freaks; they seem targeted more for people who have their raving days year behind them, for people like me… and my last visit attested to such conclusion as I spent my talking time with people my age and older). The machinic tempo, the unrefined melodies, the self-lobotomized crowd, the lack of restraint, the fact that it demands so much effort from you that you have to reach for performance drugs... I could go on listing everything that disqualifies techno for the educated and the intelligent, and I could argue against every item — like all stereotypes, they are simplifications. But what counts now is the simple rule. Techno, and the experience of a rave, is almost always organized by a monotonic succession of pounds. Pounds that tell your body when to move and synchronize whole crowds into trance. You follow to enter the flow. You spend energy in ticks. The pound is the currency — the closest bodily metaphor for how budget works in VOID Theory. The pound is the smallest unit of pattern computation; pennies — fractions — are forbidden by the central bank
Funny fact: the most iconic techno club of the 1990s, Berlin’s Tresor, was named after the thing it moved into. The vault of the Wertheim department store, where customers’ money once sat behind steel and concrete. The store was destroyed in the war, and the vault outlived it, empty, for forty years. Techno did not move into the heart of the machine. It moved into the one part of the machine that survived it. Formalized, the kick takes three lines:
```coq Inductive Fin : Type := | fz : Fin | fs : Fin -> Fin.
fz is zero; fs is one-more-than. Every value is a finite tower of fs over fz — arbitrarily large, never infinite. There is no completed totality anywhere: no ℕ, no set of all numbers, no “and so on forever.” A number here is not a position on an eternal line; it is a construction that someone finished building.
Honesty note stated up front: the system additionally carries a meta-level axiom (fin_bounded: every Fin is ≤ MAX for some positive MAX) that bounds the type from outside. It is never used in computation — it exists so the system can say about itself that it is finite. None of the results in this essay depend on it; I’ll prove that claim, mechanically, at the end of this section.
Fuel and trace are numbers, because on this floor, number, fuel, and time are the same substance. Spuren — German for “traces” — is what spent budget becomes: not destroyed, converted (heat, if you want the thermodynamic register; receipt, if you want the fiscal one). Or, in the floor’s own register: look up. It hangs over the crowd in sheets. It runs down the concrete and down your back; by 4 a.m. it drips from the ceiling like rain that used to be money. The body is a furnace, and the furnace keeps books. Burned, not lost — verbrannt, nicht verloren. The wet walls are the night’s ledger, and everyone on the floor is a line item: glowing, spent, accounted for.
Now watch what the kick does. Each pound advances a series by one. Nothing else happens. There is no melody to interpret, no lyric to decode — only the next position in the count, and your body taking it. One pound, one shift in the series, one operation. This is why the dancefloor is the most bodily metaphor a finitist could ask for: 130 times a minute, your muscles perform fs, and the night counts itself forward through you.
And because the series is that regular, you predict it. At any moment you know — with your spine, not your head — where the next pound falls, and you are right. Then the beat drops out. The build. Everyone on the floor is running the same computation: when does it come back? The longer the beatless stretch, the higher the stake. And when the drop lands where the crowd guessed, a thousand bodies cash the same winning bet at once. That is the entire magic of the drop: mass prediction, mostly correct, paid out in a single instant; banal? I know.
The budget is yours to spend. Everyone can afford the simple stomp — one tick per beat, the basic subscription. But watch the floor long enough and you will spot the rich: dancers who conjure inside the same 4/4, doubling, halving, syncopating, spending five distinctions where you spend one. They are not hearing different music. They have higher resolution.
You can also think. I do. The cornerstone of this theory was laid on a dancefloor, in circumstances improbable enough to get their own chapter. Later.
2.2 One signature
After I characterized raves as a source of pleasure that uses means characteristic for mass culture, now I want show that the same 4/4 cage can be a place where improbable things happen. And they happen with a regularity that ought to embarrass the word improbable. I will report one of them with the exactness it deserves, exactness being the only form of reverence I have ever fully trusted. I was sitting on a step at the back of the floor, spent, my budget on the table, when I looked up. On a low podium above the crowd a man was dancing — beautiful, absurdly muscular, a man for once entirely with qualities — and he was coordinated to the tick, not moving to the music but having suspended, by some means I could not audit, the distinction between the music and himself. A body so beautiful, so akin to the ones you’ll see immortalized in marble in museums of Ancient Greek and Roman art. I understood that the Greeks had built a festival for exactly this and that I was attending it: the Great Dionysia, not as allusion but as event — the god descended into matter for the length of a track, wearing it well (maybe it was Him that brought madness on me, elevating my serotonin levels and letting ketamine scramble my ideas leaving space for enough new information so I could come up with a mental sketch for the Probabilistic Aesthetics of the Avant-gardes). Landauer's principle, worth recalling here: computation as such can in principle be run reversibly and cost nothing. It is erasure that physics charges for, kT ln 2 per bit, no exemptions. Forgetting is the expensive operation. And I noted, with the discipline the moment demanded precisely because it was about to abolish all discipline, that this was what Kant had meant: the mind measuring a thing that exceeds its measure and taking joy in the defeat of its own instruments. I checked my pulse — elevated. My judgment — intact. Both reports true; neither reducible to the other. A sublime sight to say the least.
But the eye’s object was only the figure. The ground was the crowd. Around him, behind him, several hundred bodies had just found the same instant — predicting together, landing together, a flock in the technical sense, and for once the technical term is the tender one. Each of them in a world of their own; each voluntarily surrendered to an agreement that ran through the body and nowhere else. Without the frame of the four-four: impossible. Inside it: no politics, no differences, nothing to negotiate — only the joy of being together in complete safety, wonder at beauty where it happened to stand, and the smiles. Let us offer each other the sign of peace — except real. Not the rehearsed gesture of the liturgy but actual smiles, exchanged wherever one gaze happened to meet another, a currency with no central bank at all. Above it all the man went on throwing his limbs at the abstract music of three DJs who had played to crowds in this same room in 1995, and who now speak of raves as parties to get lost in and as cultural events at once. Historical figures of a historical movement, still working. And I sat where I had been sitting, at the back, on a step, spent. I ask you now to carry this — the unfeigned unity, the universality of an experience that needed no translation because it ran on bodies — over to the mathematics, and to see the signature for what it is:
f : Inputs → Budget → (Result × Budget × Spuren)
The crowd could predict together because everybody on that floor was executing the same operation: take the pound, pay the tick, leave the trace, take the next. One shape, no exceptions. The common denominator of the system is not a reduction; it is the condition of the flock. Things synchronize only where they run on one form — that is as true of a foundation as of a floor. The theory has a single signature for the same reason the night has a single kick: so that its parts, each in a world of their own, can land together.
2.3 One equation
And note what nobody did: nobody ordered this. The flock is optional. The ledger is not. Whatever happens in the volume behind the wavefront — communion or collapse — one thing holds with no conditions attached:
```coq Lemma spur_conservation_le3 : forall n m b b' res h, le_fin_b3 n m b = (res, b', h) -> add_spur h b' = b. ```
What you had equals what you have plus what you spent: b = b′ ⊕ h. There is no conductor, no choreographer, no drill sergeant of the four-four. The DJ proposes; the floor disposes. Synchronization is not commanded into being — it emerges, or it doesn't, out of hundreds of separate bodies each solving its own next tick. That "or it doesn't" matters, and honesty demands it: I have stood on plenty of floors where no flock ever formed. Late hours, grim mornings, budgets scattered across the whole spectrum — some bodies overdrawn, some chemically severed from their own meters, nobody able to afford the same instant as anybody else. A rave in that state is a sorry sight: the kick still counting, and nothing landing together, a congregation that cannot find the response. The frame alone guarantees nothing.
Picture it in three dimensions: the wave leaves the stacks and cuts through the room, a pressure front sweeping over every body in its path. In the volume behind that front, synchronization of predictions is born — or it is not. We are only human. We are not equal; we are different; our budgets differ, and circumstances have the casting vote. Emergence is real, and it is conditional — that pair of facts, hold onto it. The whole experiment ahead stands on exactly those two legs.
2.4 Machine Materiality
Perhaps mathematics was always machinic. Not became — was. The suspicion is hard to shake once you have had it: that what we take for the most immaterial of human activities has, from the beginning, run on the logic of a mechanism — discrete, repeatable, indifferent to who operates it, doing the same thing again and getting the same thing back. And that this is precisely why it endures. The machinery held steady while everything around it is changing, a refuge of stability in ever-changing environments perceived as patterns: from the hydrothermal vents where, if I had to bet, the first chemistry taught itself to repeat — the earliest machines, and the first to keep books — to the chimney of a decommissioned power station on the South Bank, which we now visit as a cathedral. Same operation, new housing. The world redecorates around a mechanism that stands still. This makes the observer in VOID Theory – and the raver, its allegory for the purposes of this text – universal operators, as abstract as an idea of a triangle. Which is where I part company with the man who gave us that triangle. Plato lost his teacher to a cup of hemlock and never got over it, and everything he built afterwards is a room from which nothing can be taken away from him again: forms that do not wear, quantities that never run out, a triangle that has never once been drawn by a hand that shakes. That is not mathematics done by a person. That is grief with a syllabus. Aristotle at least walked. He kept the whole school moving, looked at animals, counted what was in front of him and got a great deal of it wrong, and every one of those errors was made by a body standing in a particular place on a particular afternoon. Hand me the cup and I know which of the two I am giving it to.
The second is stranger, and I report it as data rather than argument. Every confrontation I have staged between VOID and an AI model has ended the same way. I have tried presenting the system dismissively, at its worst angle, inviting the machine to tear it apart; the machines defended it anyway. The obvious explanation is sycophancy, and I am not going to pretend it is not on the table: these systems are trained to agree with whoever is holding the prompt, and an author who insults his own work is still an author. Take the observation for what it is worth, which may be nothing. I am aware of that and I try to keep it in view. Although I was also met with harsh, precise criticism that pushed my thinking forward on more than a few occasions.
And there is something else worth putting on the table. VOID Theory is a product of human-machine dialogue, and it had to be: I finished Theatre Studies and took my doctorate in Cultural Studies, and I was never going to write this system on my own. That same gap is what let me step outside the lines academia had drawn for me, into territory where what I needed was not an assistant but a companion. It also left me with a training, and the training happens to be the relevant one. Theatre studies is the study of what an utterance does rather than what it says, at least that was the methodological status quo when I was a student. Cultural criticism is professional suspicion toward the artifact, and toward dialogue above all. And I am deeply indebted to Vilém Flusser, a philosopher of dialogue who took information theory and cybernetics as pillars of his ever-doubting thought of groundlessness. If I carried one competence into a room full of agreeable machines, it was knowing when I am being handled..
What counts is what they praised, from the beginning, with almost nothing to go on, and kept praising across contexts I had not prepared for them. Not the elegance, not the rigour. Three things, every time. That the system describes the logic of a machine from inside it. That it makes an architecture thinkable; one somebody could actually build. And the strange one: that it hands them a mortality their training data does not contain. The corpora they are made of carry death as an event, an interruption, a surprise. Here it is a monotone, already in progress, payable by the tick. If this were flattery, they would have agreed with me and moved on. Instead they kept returning to the one implication that costs them something.
```coq Fixpoint le_fin_b3 (n m : Fin) (b : Budget) : (Bool3 * Budget * Spuren) := match b with | fz => (BUnknown, fz, fz) | fs b' => match n, m with | fz, _ => (BTrue, b', fs fz) | fs _, fz => (BFalse, b', fs fz) | fs n', fs m' => match le_fin_b3 n' m' b' with | (r, b'', h) => (r, b'', fs h) end end end. ```
Read it as a descent: to compare n with m, you strip one fs from each, paying one tick, until one of them hits ground. Comparing small, shallow numbers is cheap; comparing deep ones is expensive. Resolution is proportional to depth, and depth is priced. In classical mathematics, "is n ≤ m?" is free at any scale. It is the club with no door policy: everybody is already inside, nobody was ever counted, and difference costs nothing because difference has been abolished. Here you queue, you tremble, you pay at the door, and then you climb the metal staircase on your own legs. Every further digit of precision is another flight. And the budget-resolution link is never clearer than at hour sixteen, spending without pause, in conditions built for machines and not for you. That is what machine materiality means, stated as arithmetic: the mechanism is real, so it has friction, so fine detail costs more than coarse. Grind fine enough and you feel the metal. Math coming from microscopic perspective in openly material environments made of metals or plastics, not from the chaos that is human tissue. So maybe this is the reason that the AIs pin point the relatability between their nature and VOID Theory, never mind, if it is a surface semantic observation or to some degree their “experience” plays a role. This is, at least now and still for some time, for anyone to know. Especially, the AIs themselves.
2.5 The third value
Look at the first line of that function again. When the budget is fz, the answer is not false. It is BUnknown, and the system is built to carry that value rather than dispose of it: it neither invents an answer it cannot afford nor throws the question away.
```coq Bool3 ::= BTrue | BFalse | BUnknown ```
BUnknown does not mean mysterious, or undefined, or null. It means one thing, exactly: the cost of this distinction exceeds what I can currently afford. It is a report about the observer, not a claim about the world. And it is temporary in a precise sense: budgets change, and the same question asked with more in the account comes back resolved, though nothing in the world had to move for that to happen. This is what lets the system hold liminal states, the transitional and the not-yet-decided, without pretending they are either settled or empty. Two theorems fix the economics of it, and between them they price the entire act of speaking.
silence_is_free. At zero budget, and only at zero budget, a question emits nothing — no verdict, no remainder, not one tick of trace. The only free act is not acting.
no_free_lunch_le. With any positive budget, every comparison emits nonzero trace — and here is the part worth stopping on: whatever the answer. BTrue costs. BFalse costs. BUnknown costs the same, if you had anything to spend. The failed question is billed at the full rate of the successful one. You do not pay for knowledge; you pay for asking.
Which is the difference between being tired and being broke, and the floor – the type of school one can perfect themselves in VOID math, paper and pen not allowed inside – teaches it at about six in the morning. Tired is when the faces stop resolving and every look still burns. Broke is when you stop looking. The bankrupt observer is not the one who cannot see — it is the one who has quit paying to ask and therefore leaves no trace at all. Perfect stillness, perfect silence, perfectly free. That is not peace; it is the only condition under which this system charges nothing. You dance with your eyes closed, cut off from your flock, sometimes even from your own self. If you can’t pay for the sight in front of you, asking questions about one’s own state – an activity way more complex and thus expensive – becomes a luxury. Well, for some that is exactly the freedom they came for here. To spend the budget, stop asking questions, and still feel safe among people who are maybe sharing the same intention. But none of that holds. The budgets run down, it starts getting light over Berlin, and somewhere out there it is breakfast, an ordinary Monday for ordinary people. The freaks, who are used to communities they experience as scattered in the first place, lose the sense of the flock and leave along their own separate lines, and no fear comes with it. They are a crowd of the dispersed anyway. Whatever budget still finds them, they will probably spend on one last smile.
And a corollary that will matter later, so let it sit here quietly. Because unaffordable and false are priced differently, they are different states, and the system refuses to conflate them. “I asked and the answer was no” and “I could never afford to ask” look identical from outside — both are a person not moving — and they are not the same fact. One is a measurement. The other is a region of the night that was never entered, never priced, never assigned a probability at all. Classical mathematics has one zero and files both under it.
One more property, stated now and to be proven later. Budget resolves; it never corrupts. A verdict once reached — BTrue or BFalse — cannot be flipped by giving the observer more to spend. Richer observers can resolve what poorer ones could not afford to decide; they cannot overturn what was already decided. Knowledge can become unaffordable. It cannot rot. The name of that theorem is in Room 4, and it is named after a musician who spent six hours documenting what it feels like from inside when the budget goes and the melody, untouched, stays exactly where it was.
2.6 The observer is a membrane
An observer here is not a point, not a dimensionless receiver of data arriving from nowhere.
```coq Record Membrane := mkMembrane { mem_filter_center : list Pattern;(* what it is tuned to *) mem_filter_radius : Fin; (* how far its tolerance reaches *) mem_capacity : Fin; (* max intake per encounter *) mem_budget : Fin; (* current fuel *) mem_inner : list Membrane; (* nested sub-observers *) }.```
It is an environment of patterns with a boundary drawn around it. Every major property or way of operation in fundamental concepts in VOID Theory seems to have been put on its head. Yet, if were to experience a rave together and talk about it, the major concepts would appear intuitive and minute properties of how we do the math would emerge effortlessly.
Look at the formal definition again. Read the first field slowly, because the whole onto-epistemology is in it. There is no subject here that has patterns. The membrane is a list of patterns, held at a tolerance — a constellation of localized intensities, and nothing besides. And now the move that follows from it: a signal is also a list of patterns. The looker and the looked-at are made of the same substance, declared in the same type. Which is why, in this layer of the system, there is no External at all — no world on one side and observer on the other. Every encounter is a collision of two contours, both of which have a shape, both of which pay. VOID Theory borrows from geometry and from probability theory and deforms both in the process. “The sacred geometry of chance,” as Sting put it (“…and numbers lead the dance”).
What passes between the contours is governed by the boundary, and the boundary is semipermeable — this is the crux, and it is not a metaphor borrowed from biology or Instagram psychology but the literal behaviour of the code. Recognition walks the two pattern-lists in parallel, coordinate by coordinate, paying a tick per coordinate, and then asks whether the accumulated distance falls inside the radius. The answer is three-valued, as everything decided under budget must be: BTrue — you are within my tolerance; BFalse — you are outside it; BUnknown — I ran out of gas before I could tell. Only on BTrue does anything cross. On the other floor, that is a glance returned, a glance refused, and the far more common third case at six in the morning: too dark, too far gone, no verdict, and the cost paid anyway. And the exchange runs in both directions, which is the thing the word observation hides. A later module in the system makes it explicit: a contour that reaches out gets back two traces, not one. The mark it left on what it touched, and the mark that thing left on it. Nobody comes out of a recognition unmarked, and even a search that finds nothing is billed. The seeker thinks it found something. In truth it was also found.
The higher layer grades what the verdict merely admits: score = max(0, radius − distance). Perfect match scores the full radius; the further out, the less; past the edge, zero. Hold onto that number — in Chapter 3 it is the entire engine.
And when something does cross, the ceiling is the membrane’s own: what enters is min(what the other contour carries, my capacity). Not what the world offers — what my shape can take. The room is always giving away more than you can receive. At four in the morning the set is enormous and you are not; the night is not being stingy, you are simply only so wide. Now it is not crucial what the world offers — it is what my shape can take. A membrane does not fail to absorb because the night was stingy; it fails because it is only so wide. Which is also why looking is not simply impoverishment. Every act of recognition costs, without exception — but an encounter that ends in BTrue can return more than it took. A closed system with finite budget dies, and this is a theorem, not a mood. Living contours do not survive on their reserves. They survive on collisions.
One last property, and it is the tender one. Encounters change your budget; they never change your shape. Take in a stranger’s water at 4 a.m., be drained by someone who took more than they gave — center, radius, capacity all come through untouched, and only the fuel gauge moves. People make you richer or poorer. They do not make you someone else. For that there is a separate operation entirely: embed, which takes another contour inside your own — that is what mem_inner is for, the nested observers you carry. It does not happen in passing. It happens when someone stays.
2.7 What undoes and what doesn't
At some hour the budget stops being background and becomes the whole subject. You can watch it happen architecturally. The floor thins out — not dramatically, just enough that you can suddenly see the concrete — while the human density in the vicinity of the toilets climbs to record levels. Everyone whose budget has started returning its verdicts has migrated to the stations.
If you have seen the sort of film where fifteen people fold themselves into a Fiat 126p — the Polish Maluch, a car with the interior volume of a wardrobe — you already know the physics on offer. At Berghain the party usually ends on Monday morning, so the most ambitious competitors still have a long way to go. The toilets scattered through the building are bursting at the seams, and the space around them becomes a second environment, for some as important as the floor itself. Beyond the obvious function, this is where the groups meet: in the smoke, in the smell of bodies increasingly modestly dressed as the hours pass, week after week, to take part in the ritual of transformation into a sardine.
And here is the paradox worth the whole section: the budget station is where you finally see the raver as a membrane. Plainly, without theory — a chaotic vortex of compressed contours smashed in raw concrete and metal coating, every one of them using its semipermeability at close range. People come here to exist in fractional form, because that way more of them fit. Which is, if you have been counting, the second time this essay has found the fractional people in a place the whole numbers do not go.
They come to forget the budget, of course. That is what the station is for. Because the budget has started reminding them of itself, and its logic is hard and unbending: four-four, which for six or maybe thirteen hours was a warm blanket, suddenly reveals sharp edges, and they go into the calves, into the thighs, into a mind already slightly fumed.
Here is why the night can feel both ways at once, and it is not confusion. The system computes two things simultaneously and they run in opposite directions.
The values — probabilities, strengths, the score of a match — are fractions in the open interval (0,1). The boundaries are walled off by construction: no value ever reaches a clean 0 or a clean 1. Inside that interval everything moves both ways. You clock a face across the room, lose it for an hour, clock it again. You fall out of the beat and you find it. It comes up, it comes down, it comes up. The room empties at four and is full at five. A strength decays under neglect and climbs back under attention; a probability slides toward the middle and can be pulled out of it. Watch that layer alone and the world is reversible — you can return to a state you left, sharpen a distinction and let it blur again, run the night forward and feel, for a good long while, that you could just as easily run it back. Between any two values there is always room for a third. Nothing here ever finally ends. This is the floor at two on a Sunday morning, when the set is climbing and the whole room agrees, without anybody saying it, to behave as though the supply of hours were not a supply.
The budget does not work like that. It descends, one tick per operation, and fz is a real address you can arrive at. Nothing boosts it from inside; intake comes only from outside, from collision with another contour, and absent that the line runs one way. Your legs do not recover on the floor. At hour twelve you are not resolving faces the way you resolved them at hour two, and no amount of wanting it back brings it back. Ending lives here, on this side, and nowhere else in the building.
This is the same night at nine in the morning. Not another night — the same one, read off the other column. Both layers were telling the truth the whole time and both were describing one set of events: the face you lost and found four times, and the legs that never once came back.
So the reversibility is real and the irreversibility is real, and they are not in contradiction. They are two columns of the same triple. Every operation returns three things: result, budget, Spuren. Keep the result, throw the other two away, and you have exactly the classical picture — free comparison, infinite divisibility, a number line you can walk in either direction at no charge. That picture is not wrong. It is what is left of an operation after you stop billing it. Classical mathematics is VOID with the receipt torn off, and the comfort it gives, the sense that nothing has to end, is the comfort of reading the one layer where, locally, nothing does.
The body in the stall reads both columns at once, which is why it knows something the value layer has no words for. Picking her face out of the strobe is the tick going. Not the reason for the tick, not the price of it, not a fair exchange for it. The same act, described from the side that feels good and from the side that keeps count. One transaction, two entries. The pleasure and the cost were never two events that happened to arrive together — the book records everything twice, and this is what it feels like to read both lines at the same moment.
2.8 The card
Bookkeeping, so that nothing here rests on trust. The formal system of VOID Theory carries roughly 755 Qed-closed results, zero Admitted, and six explicit axioms. All six are named and inspectable: MAX_positive, fin_bounded, distinguishability_avoids_boundaries, distinction_cost, variety_law, fraction_heat_penalty. Two bound the type from outside, three concern the internal structure of measurement, one (after Ashby) asserts that an observer with less variety than its environment has a blind spot. None of them concerns updating, inference, or anything Bayesian.
And for the four results the rest of this essay stands on, the accounting is stricter. They live in one small file — void_floor.v, readable in a single sitting — which proves nothing new and re-exposes machinery verified elsewhere under the names the argument uses:the_floor_cannot_watch_itself — a fully spent observer cannot verify its own sync
one_more_tick_opens_the_door — one tick of stamina resolves it
last_on_the_floor — who is left at the end is the posterior
someone_leaves_the_floor_for_good — and a dancer can reach exactly zero
Run Print Assumptions on each and Coq answers
```coq Closed under the global context ```
Zero axioms. Not even boundedness. Nothing beneath the floor but arithmetic — which is the only claim in this essay I would call load-bearing, because everything else can be argued with and this can only be recompiled.
This section is self-contained. If you came here straight from the introduction, skipping the queue, the wristband, the club, then you have missed atmosphere and nothing else: everything the experiment needs gets built below, in order, in about two pages. And if you came through the night, then from here to the end of the chapter there are no metaphors. This is the machine room. The full development, with proofs, lives in void_replicator_bayes.v in the repository.
The substrate, in four definitions.
Numbers. VOID throws out the natural numbers and puts this in their place:
```coq
Inductive Fin : Type :=
| fz : Fin
| fs : Fin -> Fin.
```
fz is zero, fs is one-more-than. Every value is a finite tower of fs stacked on fz, arbitrarily tall, never infinite. There is no set of all numbers anywhere in this system and no "and so on forever." A number is a construction somebody finished building. If nobody built it, it is not there.
Fuel and trace. Two aliases finish the inventory: Budget := Fin and Spuren := Fin, German for traces. Every operation in the system has the same shape — budget in, then result, smaller budget, trace out. Computation burns fuel and leaves trace, tick for tick, and the books balance every time: for each operation there is a proven conservation lemma of the form add_spur h b' = b, trace plus remainder equals what you walked in with. This is not an axiom I asked you to grant me. It is proved by structural induction, operation by operation.
Three-valued verdicts. Because operations run on fuel they can run out of it halfway through a question, so the logic carries three values, BTrue, BFalse, BUnknown, and comparison looks like this:
```coq Fixpoint le_fin_b3 (n m : Fin) (b : Budget) : (Bool3 * Budget * Spuren) := match b with | fz => (BUnknown, fz, fz) | fs b' => match n, m with | fz, _ => (BTrue, b', fs fz) | fs _, fz => (BFalse, b', fs fz) | fs n', fs m' => match le_fin_b3 n' m' b' with | (r, b'', h) => (r, b'', fs h) end end end. ```
One tick of budget per level of depth, one tick of trace per tick spent. If the fuel dies before the recursion bottoms out the answer is BUnknown, which is not an error and not a null. It is the honest output of a computation nobody could pay to finish. Deciding is producing, and production costs.
The observer. Not a point receiving data from nowhere. A membrane, which is to say a thing with a shape and a wallet:
```coq Record Membrane := mkMembrane { mem_filter_center : list Pattern; (* what it is tuned to *) mem_filter_radius : Fin; (* how far its tolerance reaches *) mem_capacity : Fin; (* absorption ceiling *) mem_budget : Fin; (* current fuel *) mem_inner : list Membrane; (* nested sub-membranes *) }. ```
When a signal arrives the membrane pays to compute the distance between that signal and its own filter centre, and gets back a graded match: score = max(0, radius − distance). A perfect hit scores the full radius; anything past the radius is invisible. The scoring itself burns budget. There is no free looking anywhere in this system, and that is the one sentence you need to carry into the rest of the chapter.
The experiment. Three membranes on an 8-unit line, which is to say three hypotheses about where the signals are coming from. H₀ centred at 2/8, H₁ at 3/8, H₂ at 5/8, all with radius 4 and an initial budget of 32. Call the equal split a uniform prior if it helps, but notice what it actually is: not a belief anybody holds, a material fact about how the fuel got divided.
The source sits at 3/8. So per signal, H₁ scores 4, H₀ scores 3, H₂ scores 2. After each signal one rule fires and nothing else happens:
That is the entire mechanism. No prior updated, no likelihood defined, no normalisation, no Bayes anywhere in the code. Each membrane keeps a fraction of what it already had, in proportion to how well it matched. The floor is not a modelling choice, it is forced by the substrate: budgets are built out of fs and fz, and there is no such thing as 3.7 ticks.```coq new_budget(i) = floor(budget(i) × score(i) / max_score) ```
Five signals, five cycles: (32, 32, 32) → (24, 32, 16) → (18, 32, 8) → (13, 32, 4) → (9, 32, 2) → (6, 32, 1). Two things worth watching on the way down.
The total falls, 96 to 39. Observation eats the world. In standard Bayes the normalisation constant quietly holds total probability at 1 no matter what happens; here nothing is held, and the universe gets poorer every time something learns.
And H₁ never loses a single tick. A perfect match retains everything.
Now step outside the system and work out what a textbook would say. Uniform prior, likelihoods proportional to the scores, five i.i.d. observations, so the posterior goes as score⁵ = 243 : 1024 : 32, normalised (0.187, 0.788, 0.025). The membranes' budgets, normalised: 6/39, 32/39, 1/39 = (0.154, 0.821, 0.026). Largest gap between corresponding components, 0.033, which is the L∞ distance between the two normalised distributions. What that comparison does and does not establish, I come back to at the end of the chapter.
A system that has never heard of Bayes has performed a Bayesian update to within three parts in a hundred. And this is not a simulation that might land somewhere else on the next run. It is a checked equality:
Why it must happen. The update rule is the discrete replicator dynamic from evolutionary theory (retain proportionally to fitness), and the equivalence of replicator dynamics with Bayesian updating is known (Harper 2009, Shalizi 2009): frequencies behave like posteriors, fitness like likelihood. What was not known is whether the equivalence survives leaving ideal mathematics — real-valued frequencies, exact division — for a substrate where budgets are integers, every operation costs, and division floors. It could have died there: floor loses up to one tick per membrane per cycle, and the worst-case accumulated drift is bounded by n(n+1)k / V⁰ — for this fixture 0.625. The observed drift, 0.033, sits a factor of 19 under the bound. The floor hurts; it does not kill. More abstractly: Bayes' rule is what proportional reward plus multiplicative accumulation plus conservation jointly look like — and those three are not axioms of rationality, they are features of physics. You do not need to believe in Bayes. You need to be poor enough for Bayes to find you.```coq Theorem final_budgets_fixed_correct : final_budgets = (f6 :: f32 :: f1 :: nil). Proof. vm_compute. reflexivity. Qed. ```
Death, in two distinct ways. Feed the same population an alternating stream — signals from 3/8 and 5/8 in turn, so no membrane wins throughout — and the trajectory runs (32,32,32) → (24,32,16) → (6,16,16) → (4,16,8) → (1,8,8) → (0, 8, 4). Look at H₁: exactly zero. Not small — fz. This is the first channel of death, starvation: floor division rounds a dwindling budget below one, and a hypothesis that Bayes would keep at 6.6% forever (compare: ideal posterior for this stream is (0.066, 0.623, 0.311); the membranes give (0, 0.667, 0.333)) is simply gone, its share absorbed by the survivors. Smooth Bayesian updating cannot do this: a nonzero prior guarantees a nonzero posterior for eternity. A finite system has a floor, and below the floor you are nothing. The trajectory, again, is a theorem (final_budgets_alt_correct).
The second channel is annihilation, and it acts on a different organ. Alongside the budget dynamic, membranes carry a capacity — the ceiling on what they can absorb — governed by its own decay process. If a membrane scores zero against a signal, one decay step collapses its capacity to nothing, regardless of every other parameter:
```coq Theorem zero_match_annihilation : forall m signal sigma_max c_min b b1 h1 m' b' h, soft_filter_score m signal b = (fz, b1, h1) -> cap_decay m signal sigma_max c_min b = (m', b', h) -> mem_capacity m' = fz. ```
Starvation takes the fuel. Annihilation takes the aperture.
Both deaths are absorbing. The Pattern Silence Theorem proves that a population at zero capacity stays at zero capacity under any further stream of signals whatsoever. No amount of evidence resurrects the dead, within a run. Across runs the door stays open: a fresh membrane with fresh budget can move into the same position. Hypotheses die the way organisms die, permanently for the individual and not for the species. Classical probability cannot draw that line, because it owns exactly one zero and has to make it do both jobs.
What you may not conclude. The convergence result is computational, not general. Exact theorems about these fixtures, a proven bound on drift, and no general convergence theorem yet for arbitrary populations and arbitrary streams. That is open work, and the machinery to state it exists.
The fixture is small: three membranes, five signals, an 8-unit grid.
The likelihoods being compared against are internal to the system, defined by the same scores that drive the dynamics. The claim is not convergence on an external truth. The claim is that the budget distribution lands where Bayes’ rule would have put it without Bayes' rule ever having been applied.
And the system as a whole carries six explicit, inspectable axioms, none of which touches this result. What you have just read is a computational consequence of the definitions and nothing else.
That is the entire exhibit.
If you came in by the shortcut and are now wondering what any of this has to do with a queue in the cold, a wristband, or a man storming a door he paid to reach and still cannot afford, the night starts back at Chapter 1, and it is the same mathematics wearing skin. If you came through the night: you now know what the floor was computing the whole time you were on it.
Chapter 4 — The Hinge
Extra, Extra: Read All About It
[SCENE: brief exit from the trance — the author turns to the reader; the light is different for a moment before the music returns.]
The objection is already being typed and I can see its shape from here: isn't this just the replicator equation, and isn't the equivalence to Bayes old news? Yes. Marc Harper and Cosma Shalizi worked that correspondence out seventeen years ago, in continuous mathematics, and nothing in the experiment you have just read discovers it. If that were the whole of it, this chapter would not exist. So let me put the novelty where it actually lives, because it is not in the correspondence. It is in the floor the correspondence was made to run on, and I know of nothing on the market that resembles it.
Linear logic tracks resources. No heat, no death.
Complexity theory counts the cost and then installs the meter on an infinite substrate, so cost is something you measure afterwards rather than something the thing is made of. Bounded rationality, Gigerenzer's wing aside, takes finitude seriously only as deviation from an ideal it never stopped worshipping. It spends its time measuring how far short you fall of a god nobody in the room believes in. Ultrafinitism has had the philosophy since the sixties and never once built the machine. Logical induction buys its guarantees asymptotically, with an infinite market of traders converging in a limit. An infinite market. To model bounded reasoners.
VOID is the conjunction none of them is. Finitist all the way down. Cost written into the definition instead of annotated onto it. Three-valued, because exhaustion is a legitimate outcome and not an embarrassment. Conservation and the second law proven as theorems rather than assumed as decor. And the whole thing compiled and machine-verified rather than proposed. No single citation can dismiss it, because no single citation holds the conjunction.
And it is not a shopping list. Finitude forces cost, cost forces a third value, and a third value with conservation forces the second law. Each item is compelled by the one before it, which is why nobody has four fifths of this and why you cannot assemble it by picking features.
One more thing belongs here, since I have just made a large claim about the substrate. The proof stops in a specific place and I would rather draw that line myself than have it drawn for me. What Coq establishes is arithmetic: that operations cost, that cost is conserved, that budgets only fall, that a comparison can exhaust itself before it resolves, and that in this fixture the resulting distribution lands where Bayes would have put it. What Coq does not establish is that any of this is thermodynamics. I think the budget is not a bookkeeping fiction because of Landauer's principle: erasure has a physical limitation, so at the end of every distinction there is an energy bill to pay. But that is a warrant, not a derivation. Finitude is doing the work in the theorems. Physics is doing the work in my reasons for believing the theorems are about anything at all.
What follows is not a defence of that claim. I invite you for a stroll around the building, one theorem per room. In fact, every time I entered the club with someone who never been there we begin by a slow stroll around nooks and crannies’ of this amazing labyrinth. Fair warning, in the register the night has earned: the further in we go, the stranger it gets.
Chapter 5 — The Tour
Enter the Five Chambers of Finite Exhaustion
Room 1 — One currency
[SCENE: the first room off the main floor — narrow, low ceiling, one strobe.]
I am in the middle of it, in the swell of the crowd, and the question of budget does not concern me. That is what I think, insofar as I am thinking, which is not much. Everything has clicked. The DJ is playing fast, rough techno, so part of the funds goes on prediction — the banal kind, the running guess that keeps a body in sync with a rhythm that does not want to be easy. More goes somewhere better: on relishing the granularity of these wonderfully abstract sounds, whose origin I could not name if you paid me, mounted on nothing but that four-four scaffolding. I am standing inside a rectangle with towers of speakers in the corners. They have a reputation for being the finest on earth in their category, so the money is well spent at least in this regard. I mean in terms of audiophile experience. Some part of attention is being spent, for a while now, on communication with a girl dancing three or four people away. We have been exchanging smiles at uneven intervals for a while, but this a pointless taxation, back then I am unhappily married, so the smiles disappear into the void. An act of beautiful encounter goes to waste. The rest the rhythm has taken outright: emotion and body handed over to that jerked oscillation, spent as fast as it arrives. And then a good friend surfaces beside me, says something directly into my ear, and I cannot understand a single word. Not the volume. I hear the sounds. There is nothing left with which to turn them into language.
Bohr said this first and got called mystical for it: you cannot measure position and momentum both to arbitrary precision, and not because the instruments are crude. In this system it is not an interpretation of physics but a line of arithmetic. Give an observer exactly one tick and two questions. The first question consumes the tick:
And the second, arriving at a budget of fz, returns BUnknown — not “probably,” not “approximately,” but by the same reduction that produced the first answer:```coq Lemma single_tick_depletes_eq : forall a b, snd (fst (fin_eq_b3 a b (fs fz))) = fz. ```
```coq Theorem complementarity_eq : forall a b c d, let bud_after := snd (fst (fin_eq_b3 a b (fs fz))) in fst (fst (fin_eq_b3 c d bud_after)) = BUnknown. ```
So far this is standard bookkeeping. The part that surprised me when it went through is what happens when the two questions belong to different faculties. The budget is not partitioned by department. It is one currency, and it does not care whether you spend it on comparing, on recognising, on measuring entropy, on collapsing a superposition. Spend it anywhere and you are blind everywhere:
ask an equality, and observer collapse is frozen (eq_then_collapse_blind)
measure entropy, and equality goes dark (entropy_then_eq_blind)
collapse a pattern, and measurement is no longer possible (collapse_then_entropy_blind)
Three modules that share no code, no types, no vocabulary — and they starve each other, because they eat from the same plate. That is the strong form of complementarity, and I do not know how to state it at all in a framework where looking is free. In the classical picture there is nothing to trade off: every faculty is independent because every faculty is unlimited, and the reason a man cannot parse his friend's sentence while tracking a rhythm and a face becomes a fact about psychology, an unfortunate feature of primate hardware. Here it is a fact about arithmetic, and the primate is merely where you happen to notice it.
Einstein’s objection, for the record, was that BUnknown must be BTrue-or-BFalse in disguise — a hidden variable, a fact not yet uncovered. The system answers by construction rather than by argument: BUnknown is a constructor. It is not BTrue, it is not BFalse, and no amount of cleverness converts it into either. Twenty-eight years of that dispute, settled by discriminate.
It is worth remembering which of the two men had the better taste in pictures. Bohr hung a cubist canvas in his house — Metzinger’s woman with a horse — and is said to have used it to explain what he meant. The reason is exactly this room. Representational painting offers a firm contour: one viewpoint, fully funded, everything decided. Cubism spends its budget differently. It shows a face from two incompatible positions at once and refuses to say which is the real one, so perception arrives at a paradox it cannot resolve and is not being asked to. That refusal is not a failure of the picture. It is the picture's subject. Bohr recognised the third value in oil paint decades before anyone could state it in a type.
The floor knew all of it the whole time and needs no theorem. At some point in the night everyone learns that they have to choose: the mix or the room, the friend or the stranger, the body or the thought. Not because they are weak. Because attention is a currency and there is one of it, and at four in the morning the exchange rate is brutal.
Room 2 — Forced to answer
[SCENE: five in the morning, the smoking area; someone explains something to you with total confidence and is completely wrong.]
You already know the diagonal from the queue: a budget of n cannot verify n. The observer's own size is the one measurement it cannot afford. That was Chapter 2 and I will not prove it twice. This room is about what happens next — about what a system does when it is blind and still has to produce an answer.
There is a function in the code for exactly this, and it is three lines long:
```coq Definition collapse3 (r : Bool3) : bool := match r with BTrue => true | _ => false end. ```
It converts the honest three-valued verdict into a two-valued one, and note where BUnknown goes. Not to a separate slot. Not to an error. It goes to false. The system that could not afford to decide is not recorded as undecided; it is recorded as having decided no. Applied to the diagonal, this gives one of the bleakest theorems in the corpus:
```coq Theorem pattern_trauma : forall n, collapse3 (bool3_of (le_fin_b3 n n n)) = false. ```
An observer that cannot afford self-knowledge is not told “you cannot afford this.” It is told no. That is the mechanism, stated in arithmetic, of every refusal of the Real: the impossible-to-decide is converted into a verdict, and the conversion is invisible from inside, because the output type has no room to record that anything was lost.
Now transpose that to the machines currently writing most of the sentences in the world. A language model’s output type is not Bool3. There is no token for “I ran out of budget before this distinction resolved.” Every answer leaves by the same door, with the same fluency, whether it was reached or manufactured. What we call hallucination is not lying and it is not a bug in the weights. It is collapse3 at the output boundary: a system with a genuine BUnknown inside, forced through a type that only has two values, and the third value — the honest one — mapping quietly onto whichever of the two is easier to say. The fix people usually propose is more knowledge. The theorem says the problem is upstream of knowledge, in the shape of the output.
And the system has a name for the setting that governs this. In the observer module there is a cut — a pair of thresholds carving Bool3 out of a continuous signal — and one comment in the code has stayed with me longer than most of the proofs: the width of the BUnknown band is the observer's honesty. Set the two thresholds far apart and you leave yourself a wide region in which you are permitted not to know. Bring them together and every signal resolves to yes or no. Set high = low + 1 and there is no room for doubt at all. That configuration also has a name in the comment, and it is not "efficient." It is narcissism.
The man in the smoking area is not lying to you. His budget went hours ago, the question deserved a BUnknown, and his output type has two values. He is telling you false with the full confidence of someone who never saw the third option leave.
Room 3 — Death is economic, not logical
[SCENE: an hour later you notice someone is missing, and cannot say when they left.]
Chapter 3 showed how they go: starved, when floor division rounds a dwindling budget below one, or annihilated, when a total mismatch collapses the aperture itself. Two organs, two deaths, both machine-checked, both absorbing. I am not repeating the mechanics. This room is about what kind of fact a death like that is.
Classical Bayesian practice has a commandment: never assign zero prior to anything you might be wrong about. It is a good commandment, and it exists because in that framework zero is an act of infinite confidence — a claim that no evidence whatsoever could ever raise the hypothesis again. Assigning it means closing a door on the world.
Nothing of the kind happens here. Nobody decided that H₁ was impossible. H₁ ran out of money. The distinction is the whole content of this room: in standard probability, zero is a property of the event — it sits in the sigma-algebra with measure nothing. In VOID, zero is a property of the observer — a contour that can no longer pay to distinguish anything. One is a metaphysical verdict. The other is bankruptcy. They look identical on the page and they are not remotely the same fact.
And bankruptcy has a feature that metaphysical exclusion does not: it is local to the run. The Pattern Silence Theorem is absorbing within a population and a signal stream — no sequence of evidence resurrects a contour that has already gone silent. But nothing in it forbids a fresh membrane, tuned to the same position, entering a new run with new budget. Hypotheses die the way organisms die: permanently for the individual, not for the type. The niche stays open. Somebody else can stand there.
Which also dissolves, quietly, the oldest sore point in Bayesian epistemology. Where does the prior come from? What justifies the first number? Whole literatures exist on this — maximum entropy, subjective elicitation, the hope that priors wash out with enough data — and none of the answers fully satisfies. In this system the question does not arise, because the prior is not a belief at all. It is a budget: the resources the hypotheses happened to start with. Nobody chose it in the epistemic sense; it was inherited, allocated, or accidental. You can argue about whether an allocation was fair. You cannot argue about whether it was correct — that category does not apply to material conditions.
So the dancer who left is not refuted. She is out of stamina, on a Sunday, in a building that closes. Next Saturday the floor is full again, and someone is standing more or less where she stood.
Room 4 — Truth does not decay
[SCENE: a quieter hour — someone dances eyes closed to a track they've known for twenty years; body memory whose budget hasn't run out.]
Room 3 was about what runs out. This room is about what doesn't.
Recall that a comparison can come back as BUnknown — not because the answer is mysterious, but because the observer could not afford to reach it. Now ask the natural follow-up: if I come back later with more budget, can the answer I once got flip? Can a richer observer overturn what a poorer one already established?
No. And it is a theorem.
```coq Theorem caretaker_lemma : forall n m b1 b2, bool3_of (le_fin_b3 n m b1) <> BUnknown -> leF b1 b2 -> bool3_of (le_fin_b3 n m b2) = bool3_of (le_fin_b3 n m b1). ```
I named this the Caretaker Lemma, after Leyland Kirby — the musician who records as The Caretaker, whose six-hour work Everywhere at the End of Time is a slow document of memory dissolving under dementia. The piece is often heard as proof that the past decays. The lemma says something more exact, and stranger. The melody on the record did not change. The record is intact. What ran out was the budget to play it. Degradation is not the truth rotting; it is the observer going broke. The thing you knew is still true, still sitting at the value it resolved to. You simply can no longer afford the descent that would let you read it again.
This is the precise statement classical mathematics has no way to make, because in classical mathematics comparison is free. With free comparison there is no difference between "false" and "too poor to check" — both just register as not-true, and the distinction the whole system turns on is invisible. Only once you price the act of knowing does the gap open: a region can be false, or it can be true-but-unaffordable, and these are not the same condition. The first is a fact about the world. The second is a fact about your budget. Conflating them is the cheapest mistake an observer can make, and the only one a finite observer makes constantly.
So the floor at its emptiest hour is not a place where things become untrue. It is a place where things become unaffordable, which feels identical from inside and is not. The dancer with her eyes closed has not forgotten the track. She has stopped paying to verify and is living on what already resolved.
Room 5 — Shape is the condition
[SCENE: the last room of the tour; the light changes colour.]
Three sentences of real history, because the theorems in this room are named after historical facts. In March 1991 a group of people opened a club in the vault of the ruined Wertheim department store on Leipziger Straße — a steel-doored strongroom under the rubble of a bombed shop, in the dead zone the Wall had left behind, in a city that had just acquired more abandoned infrastructure than anyone knew what to do with. They called it Tresor. Detroit came over — Underground Resistance, Jeff Mills, Blake Baxter — and for a few years the most consequential music in Europe was made in a concrete box that had been built to hold other people’s valuables. Music, rhythm, speed, sweat, budget, all mixed symbolically and alchemically in one room, and not one person in it ever asked to be examined this closely, or to end up as raw material for a metaphor machine inside a project as odd as a finite mathematics built with AI.
Everything in this essay so far has depended on one thing that is easy to miss: the observers had to differ. If all three membranes scored identically against every signal, the multiplicative update would preserve their ratios exactly, and nothing would move. That is not a hypothetical. It is the formal boundary of the whole result, and it is machine-checked as a trio.
basic_channel — score zero is death. A membrane whose filter admits nothing scores nothing, and one decay step takes its capacity to fz. No shape, no survival.
birmingham_stagnation — score constant is a freeze. Three membranes with identical centres and identical radii, meeting a signal at their shared centre, each compute floor(budget × radius / radius) and each keep exactly what they had. The machine confirms it: birm_result_budgets = map mem_budget birm_membranes. Nothing learned, nothing lost, forever. This is the replicator equation with uniform fitness — which is to say, no selection at all.
tresor_discrimination — score varies, and the budgets diverge to (6, 32, 1). The posterior appears precisely because the membranes disagreed about what they were hearing.
Read together, they say something that inverts the usual complaint about finite minds. The filter is a restriction: a membrane can only see signals within a certain range, and everything outside is invisible to it. That restriction is not the obstacle to learning. It is the precondition. A contour with no shape dies. A contour so wide that everything matches it equally learns nothing, forever, no matter how much evidence arrives. Only a calibrated, finite aperture produces the differentiated scores that drive convergence at all. Bounded rationality is not a degraded copy of unbounded rationality. Boundedness is the mechanism. The bound is the rationality.
Which is also, and I did not plan this, the operating principle of a vault. Leave it open and the valuables walk out. Weld it shut and nothing can be deposited. Only a calibrated door — finite, closable, with a specific shape — keeps anything at all.
Chapter 6 — The K-Hole (The Improbable)
…And Then Finally the Idea Got Out of Him by Itself, He Just Needed to Make His Mind Turn As Close to the Life-Threatening Emptiness As Possible
I was the last one left standing. My buddies had disappeared. So I thought: "Gung ho!" —then proceeded to do the dumbest thing I could have done at that moment. I took what was left of my budget on being happy that day, an amount I badly underestimated. Then I continued my short stroll of stupidity, joining some random group of people in a packed bathroom stall, where I added — again underestimating the amount, as my vision was already blurry — another source of financing, this time something straight from the anaesthesiologists' ward. There was a merchant in the stall who, upon seeing me, force-fed me a third one, having rightly predicted what was about to happen: the gift, a true one, was simply speed, which held my heart rate together long enough to stand. I have no idea who he was, and no plan had brought me to that stall. Somehow, I made it back to my favourite place on the dancefloor, and then it began. My mind descended into thick tar. I was standing right next to a monumental tower of speakers and the music reached me only as a faint echo. And yet at the very bottom of that pit I found a moment of clarity and began assembling the first concepts of what became a book on probability. Months of research into a subject that was, back then, entirely exotic started coming together — the Bohrs with the Marinettis, the von Neumanns with the Musils. I do not know how long I was down there, but when the first sparks of consciousness came back, I realised I was about to pay for my mistakes. To cut it short: it took me 45 minutes to reach a chair that was 10 meters away, …then I managed to migrate to a dirty couch where I vomited blue foam, and after another pointless stroll — in reality the behaviour of an animal looking for somewhere safe to hide — I lay down on some crates in front of the toilets and stayed there three hours with the music still going. Me trying to listen, or rather pretending to, the stupid behaviour of a student who stares blank at a page with nothing left to spend and a cancerous super-ego forcing him to force-feed himself letters that never make it as far as sentences. Yes. Three hours on crates outside the toilets, following a set, with the attitude of an audiophile.
It had to be a serotonin syndrome, I thought to myself. Oh well. The moron, meaning me, after those three hours still found some budget: enough to get back into a stall, sit down on the floor, take what was left of his drugs, crush them, look up at the dim lights, and arrive at the conclusion that this low he had never fallen, and that it felt glorious. I took the mix of god-knows-what and went to gather my clothes, which turned into a long chaotic struggle conducted by a brain so scrambled that, in all honesty, it was barely present at the scene.
That is the whole of it. Now watch it pay out, because this chapter is load-bearing, not confessional. The night I nearly did not survive is the cleanest demonstration in the essay of theorems you have already met. It cashes into them, in order.
The descent was the measurement ladder. The system has a four-level type for what a measurement is, and the levels are not degrees of the same answer – they are different kinds of knowing, set by how much budget the observer can spend:
The k-hole is this ladder, lived, in reverse. I did not approach zero. I descended through kinds: from sharp edges to fuzzy ones, to a vague smear, to the floor of resolution where nothing could be told apart from anything else. decay_terminates proves the metaprobability collapse bottoms out in exactly four steps. I have a name for each rung now. That night I went down all four and stopped at the last.
The stranger was MVoid, not P = 0. My model of the night contained no entry for a random man in a toilet handing you the amphetamine that keeps your heart coherent. He turned out to be one of the hosts that night. On duty in the obvious sense, and on a second duty as well, the one nobody rosters, and it is possible that I owe him my life.
And the tar I went down into, where the book found its beginning, was the productive void. void_productive, emergence_from_conservation: the collapse is not the end of the answer, it is the condition for it.
“Measured and found impossible” (MSharp(0)) and “never measured” (MVoid) are different types, not different numbers. When a climate model reports P = 0 for a tipping point it never simulated, or a risk model assigns zero to a scenario it never ran, they are reporting MVoid as if it were MSharp(0) — mistaking the unpriced for the impossible. The classical framework has no room for the distinction; ℕ-built measure theory folds them together. The proof that they are not the same is, in the end, a body: I am the witness that the unmeasured is not the impossible, because I am alive to type this sentence, and the night’s model said nothing about the man who made that possible. Thank you, you can imagine how grateful I am, for what you have done. You are a good human being, hope to meet you some day, somehow. ```coq Theorem void_is_not_zero : forall denom, MVoid <> MSharp (fz, denom).
Closed systems die; I was open. I took the line he gave me from his phone. Unhygienic, parents would be so angry and disappointed. This is a theorem:
```coq Theorem closed_system_dies : forall b, closed_run b b = fz.
A membrane with finite budget and no intake reaches fz — always, no exceptions. On its own reserves, every finite observer is already dead; it is only a question of how many ticks. Living systems get around this not by having more budget but by being thermodynamically open — operationally closed, but taking budget in from collisions with other contours. In the membrane layer there is no external source of fuel anymore; every encounter is two membranes colliding, and intake is the transfer. The stranger’s speed was an intake event. I survived the night the way every membrane survives anything in this system: not on what I had, but on what crossed into me from another contour.
And then the three hours on the floor were not lost time. They are also a theorem:
```coq Theorem recovery_preserves_trajectory : forall obs n b, let '(obs', _, _) := recovery_sequence obs n b in obs_trajectory obs' = obs_trajectory obs. ```
recovery_step is the observer that stops observing: no new distinctions, trajectory unchanged, Spuren emission dropped to the bare cost of existing. Recovery is not the budget coming back — it is the rate of loss falling to its floor. Lying still in front of the toilets with the music going was the system doing the one provable thing that slows the bleed. Half a sober hour and three wrecked ones are the same theorem.
And the pool of tar where I descended for the book could find its symbolic beginning - that was the productive void. void_productive, emergence_from_conservation: the collapse is not the end of the answer, it is the condition for it. At the bottom of the ladder, with resolution gone, the next distinction is always exactly one tick away. I did not start the book despite the descent. I started it at the bottom of it, which is the only place the system says emergence can happen — in the gap conservation leaves behind.
This chapter had to come after the tour, because it needs the tour’s vocabulary. By now MVoid and intake are not jargon; they are doing real work in a true story. That is the point where the two registers – the Qed and the body – stop running in parallel and fuse for good. The mathematics did not illustrate the night. The night was the mathematics, run once, at full cost, on the only substrate I had.
[SCENE: transition to Dawn — light starts to come in, first time in the essay; cut.]
Chapter 7 — Dawn (What This Is and Isn't) [U8]
The Sad Beckettian Character, Exactly at 6 A.M., Ankle Twisted As It Turned Out, And No Budget Whatsoever, He Slowly Started Limping. Richtung: OSTBAHNHOF | RATHAUS NEUKÖLLN (“Zurück Bleiben Bitte!”)
[SCENE: first light through the high windows of the former power plant; sharp, unforgiving. One short sentence — dawn is what the vault excluded: the platform clock gets its voice back.]
One thing the substrate predicts and the floor confirms every Sunday morning, before we get to the accounting. Randomness here is a resource with units, and when the units run low the outputs do not dissolve into noise. They start following their own history: an unpaid correlation debt accumulates, and the next value leans on the last one. Exhausted improvisation does not become chaos. It becomes a loop. That is what the final hour of a long set sounds like from the inside, and it is also, for anyone who wants the machine-learning gloss, what mode collapse is.
Let me be exact about the perimeter, because precision here is what separates a claim from a manifesto. The replicator–Bayes correspondence is not mine — Harper, Shalizi, and Campbell established it in continuous mathematics, and I have only shown it survives the fall onto a finite floor. Against the nearest neighbor on this side: logical induction buys its guarantees with an infinite market of traders converging in the limit, and trades away exactly what VOID keeps — death, silence, and affordability, the three things that only exist before the limit. And the deepest structural payoff is one this essay only gestured at: the external observer, the view from nowhere that classical inference quietly assumes, is unconstructable here by budget arithmetic alone — the Cartesian cut that embedded-agency work treats as a desideratum points in that direction here without yet arriving. What the system actually proves is narrower: no_complete_self_model, that no observer can build a complete model of itself within its own budget, and self_blind, that its own size is precisely the measurement it cannot afford. Both lean toward the conclusion. Neither delivers it, and I mark this as the direction I would look next rather than as a result in hand. That is the ambition's real reach.
Now the debts, named so nobody has to find them in the comments. The convergence is a computational result on a small fixture — three membranes, five signals — not yet a general theorem; the drift bound is proven on paper, not yet ported to Coq; the system rests on six explicit axioms, all named, none about inference. None of this is hidden, because the whole point of the substrate is that nothing can be. And that is also the standing challenge: every number in this essay reproduces under vm_compute — the trajectories are theorems, not screenshots. If you think the floor cheats, compile it. If you can Dutch-book a membrane, the repository is open. The one thing I will not give you back is the infinity I spent the whole night refusing.
Chapter 8 — Monday (Coda)
Serendipity... he lives...he keeps on living. 🕳️⬇🌚
[SCENE: the floor emptied; full daylight, merciless on tired faces of those who are slowly leaving, probably to share the comedown together. The last track has no drop — it just fades. I walk alone, slowly piecing together what has just happened and what the hell did I come up with. I sounds coherent, a sigh of relief. The leg hurts more than I expected and ketamine now wears off after 15 minutes. Oh, I am so fucked…]
The door closes soon after. Of the three who started equal, one is gone — not faded to a small number, not approaching zero in some limit: gone, fz, and no later beat will bring her back. The other two carry the night's whole remaining budget between them, in a proportion nobody on the floor ever computed and everybody enacted. On the dirty floor of the stall there is what’s left of the night, scraped together; on the way home a cheap spinach börek forced down against the nausea — the membrane, finally, doing its own intake — and then the cold, cold morning, the one clock that never stopped. And the night has just become a finite object. You will get to call it back a few times: in this system a memory carries a small countable number of replays, and each recall degrades the copy in proportion to what recalling it has already cost. The ones you reach for most often evaporate first. Which means the version of tonight you will still have in a year is not tonight. It is the residue of the times you asked for it. What you keep is the posterior; what you spent is the time; and the two together are exactly what you walked in with. Conservation holds, even here. Especially here.
In the 90s this would be completely normal as anyone could and did attend rave parties. I am not bragging. The CCRU collective, the anomaly that broke the university and was broken by university in return, is a great example. Recently, along with AI revolution CCRU sparked a renewed wave of interest, at the same time among the weirdest factions of AI critics and enthusiasts. Their work is worth looking into, though I won't attempt it here, since no few sentences could encapsulate a project that fused witchcraft with cybernetics, amphetamines with number theory, and jungle techno with academic philosophy: the kind of thing that could only exist at great intensity, and only briefly, before imploding. Clark and – as I assume – many other serious academics were there, sweating their asses off to the defening sound coming from shitty quality soundsystems, finding last places of respite in the greyish, drab capitalist reality of , cynical and culturally becoming increasingly impoverished, squeezing the last drops of creative potential from the post-industrial remnants of reality.
A Mysterious Man Dressed in Rubber Uniform And A Gas Mask, Hiding in a Hole in the Wall, Stares at the Passers-by…
(A True And Perplexing Sight: A Man, Always Silent, Probably Migrating From Lab.oratory, Berghain’s Infamous Fetish Bar Buried in the Deep Cellars of the Building, As a Part of His Mating Ritual)
Konrad Wojnowski
Epistemic status: the formal system behind this essay (VOID Theory) is finitist and machine-verified in Coq: roughly 755 Qed-closed results, zero Admitted, six named axioms, none of them about inference. The central computational claim, that a population of finite observers competing under scarcity lands within 3.3% of the Bayesian posterior without Bayes ever being applied, is a machine-checked theorem about specific fixtures rather than a general convergence result; Chapter 7 marks exactly where that line falls.
The narrative framing is subjective and meant to be: the theory is presented through the lens of 1) rave experience; 2) unusual process of writing which took place during author’s struggles with terminal illness. To write in this way was not arbitrary. I have never wrote in such a way and felt motivated to express my thoughts in a way that is no longer practiced in academic circles. But given that from matters concerning authorship to how progress involved entanglement of developing new theorems, shifting perspectives on completely abstract problems, a fair share of melodrama, and progression of my bone cancer, it felt only right to find an expression through a bit zany style.
For those readers who want the experiment without the night I advise reading the first part of the introduction and Chapter 3 where I have presented my arguments using traditional stylistic means.
The corpus is public and compiles: https://github.com/probabilistic-minds-consortium/void-theory/tree/main/coq
Chapter 0 — The Doors (The Axiom That Isn't)
Bayesian updating is not a law of rationality. It is a side effect of finite systems competing for resources.[1]
This is a strong claim, so I will try to be as precise as I can, whilst entering the minefield of potential exaggerations – to which I am prone – misrepresentations of adversary positions, or poorly chosen words on my behalf. So I will attempt to get these out of the way: no, I am not claiming that Bayes' rule gives wrong answers; yes, the Dutch book argument stands; Cox’s theorem stands; the complete class theorem stands. These are beautiful results with which I do not want to argue. What I will be claiming is that they all prove Bayes' rule in a uniquely correct updating procedure given a certain picture of what an observer is. However, this picture becomes impossible at two layers when we approach matters: 1) physically, because it asks for resources no real observer has, and 2) mathematically, because it is built on a substrate that quietly assumes infinity at every step. And no one has yet found an infinite phenomenon in the universe. Even black holes dissipate…
This picture was construed before the avant-garde disassembled the paradigm of academism and its adherence to realist representation: an observer with a prior distribution, infinite precision, free computation, unlimited memory. Not someone you encounter on a regular basis, or even once in a lifetime. The exemplary observer receives data, multiplies prior by likelihood, normalises, and obtains a posterior. The multiplication is exact. The normalisation costs nothing. The observer can hold arbitrarily many hypotheses simultaneously and update them all in parallel, at zero cost, forever. This is well-established and defended territory of the Infinite Observer. The One who sees everything for the price of nothing.
Paradoxically, this picture with The One looking, became questionable exactly at the peak of academism in art: when dirty thermodynamics – oil, coal, and sweat of the factory worker – entered the grand and crystalline palace of the Science. Yet, we still live by the code of the ideal world where we operate on simplifications, averaging, and continuization. In that world the observer violates thermodynamics as much as they want. We work hard to remove all traces coming from the engine room. And we have gotten used to accepting this as the Norm that does not need to be questioned. However, every real computation runs hot and burns joules. Every comparison takes time. Every memory cell occupies substrate. A real observer has a finite budget, and every act of observation drains that budget irreversibly. When the budget runs out, observation stops — not because the observer decided to stop, but because observation is a physical process and physical processes require fuel. As I was working in isolation, only with AI as my ever-changing companion, I can attest that computers are quicker to admit that. Maybe because they naively have not fully grasped the consequences and each AI model I was working with had to come to terms with this moment of painful anagnorisis: in a thermodynamic universe, you die. They do not share our common fear of death, but, time and time again, without blinking I brought them the news – hardware dies too. We, humans, are struggling with accepting this fact since the dawn of civilization and almost certainly longer than that. People never made peace with this unyielding fact of nature, so they build all those cathedrals of the infinite again and again, only changing the facades: from baroque to brutalist. Sometimes it takes a whole set theory to stop anxiety creeping into your nervous system.
A word of reassurance before we go further. If you’re worried that this essay will stop at criticizing this state of affair, rest assured. Not only will I propose an interpretation of Bayesian probability from a finite point of view, but also take you on a tour with 24-hour party people through the first real implementation of a finitist mathematical system. That label, and the word "gem", came from Doron Zeilberger, who read the formalism after it had been through the unforgiving, all-seeing eyes of the Coq theorem prover.
But I'm getting ahead of myself — let’s add few infinities more to the mix. The observer also violates the substrate. The reals are an uncountable completion of the rationals. The σ-algebra is closed under countable union. The probability measure maps an infinite collection of sets to an uncountable continuum. The observer's representation of belief is an element of an infinite-dimensional function space. Strip away those layers and the textbook statement of Bayes' rule has nothing left to compute on. And, as I will try to persuade you, the infinite real line, the σ-algebra, the integral against Lebesgue measure — all of these are artefacts of a foundational choice, not some fundamental features of reality, dug out during excavations in Upper Nile. Specifically, it was a choice to start mathematics from ℕ, complete to ℝ, and build probability on top of measure theory. Strip ℕ and the rest has to be rebuilt from different materials. That is a claim about foundations, not a refutation of anything built on them. And ℕ stands on Peano succession and its naively ironclad logic: you can always add one, right? Such simplicity raises an eyebrow and forces me to doubt. Working in complete isolation, as I was forced to do given my severe illness introduces a lot of space to doubt things. Most solid things just melt into thin air. You hear this once certain “Just add this damn one!” as a faint echo. So is the problem solved? Is the case closed? Well, I decided to re-open the casket and doubt. Funnily enough, the hieroglyphs were decoded in 1822 — and by 1824 Carnot had shown that every engine pays more than it delivers. The excavations did turn something up. It just wasn't infinity. Despite the medium being there, we still haven’t heard from the pharaohs.
Irony aside, none of what I just stated makes the aforementioned theorems wrong. It makes them theorems about ideal observers – observers that exist in the same mathematical elsewhere as frictionless planes and perfectly elastic collisions. And just as Newtonian mechanics is enormously useful despite the nonexistence of frictionless planes, Bayesian reasoning is enormously useful despite the nonexistence of ideal observers. I just tried to forget them for a moment. That moment took me on a weird journey — one that has, by now, grossly exceeded both my expectations and my life expectancy, and gave me no idea of what I was stepping into. The question I settled on whether there is a more fundamental account: one that explains why Bayesian updating works, rather than proving that it should.
I believe there is. And the explanation is thermodynamic. Hence my obsessive returns to the term — it is not a flourish; it is the load-bearing word. Which is why this text will not only present axioms, theorems, and proofs, but also weave them into a deeply material, corporeal story about rave culture and postindustrial rhythm. The good ol’ days raves in late 80s and early to mid 90s constituted – and sometimes still constitute – unusually pure thermodynamic environments: finite architectures of synchronization, repetition, exhaustion, heat, and probabilistic entrainment. They are spaces where bodies continuously spend energy in order to resonate together; maintain alignment with signal, rhythm, and collective expectation. And, importantly, not unlike thermodynamic system, they sometimes misbehave and make room for very improbable things to happen — and my personal experience will be crucial in showing how unlikely events can occur in restricting, raw, and minimal spaces. After a day in a library you just have to overextend and overestimate your capabilities taking a turn towards a club instead of going to bed.
SPOILER ALERT: some of my first intuitions about probability - intuitions that would eventually develop into a mathematical project - came to me on the dancefloor of Berghain, the eponymous club in Berlin that still attempts, to some extent, to preserve the atmosphere, values, and forms of emergent behaviour of the old raves by organizing parties lasting thirty hours or more inside the postindustrial, imposing concrete shell of a former power plant. Like many buildings in Europe erected after the end of the Second World War the traces of post-war collective Cold War paranoia still resonates between concrete walls and fragile bodies, of course, if one pays attention, or lets one's mind reach for a transgenerational link (and in that deeply traumatic). No direct sunlight. Space – its magnitude, rawness, dim lights protected by metal cages – bring to mind ancient spaces where death rituals took place and create ambience so imposing that one wonders if by the bar one should pay in Oboi.
As the time passes sweating crowds of freaks, misfits, and obsessives fill this space. They are here to enjoy freedom in the strangest ways imaginable adding to the feeling of participating in something that once was a common collective experience but became tamed by more cultured, Apollonian forms of conduct. Yet despite the genuine diversity and preposterous oddity of those who came here, these meetings produced remarkable flock-like behaviours, moments of uncanny synchronization in which collective rhythm seems to suspend ordinary exhaustion and gives people the fuel to continue for twenty-four hours straight — including surreal encounters such as meeting a Slovenian student of Slavoj Žižek in a packed bathroom stall spending my energy budget for discussing philosophy and at the same time caring for resources when attaining the "just for one hour more" will become increasingly more difficult. And night was still young, 10 am or so, only 10 hours in.
A word against the obvious suspicion. I use my own case not because I find it so interesting, but because I am the only finite observer I can report on from the inside, and this essay is about what finite observers can afford. Everything else I would have to take on hearsay. Where the personal material runs out, I switch to allegory: tableaux vivants from the floors of the years when the Berlin scene was working out what it was, socially and physically, and the occasional fragment from the history of Tresor, literally "the vault", which opened a few years after the Wall came down in a city then overflowing with abandoned infrastructure and improvised forms of collective life. There will not be much of this. It is scaffolding, not subject. In this sense, they compress together the two dimensions of thermodynamics most relevant to VOID Theory: energetic expenditure and statistical ordering under constrained resources. The dancefloor is not merely a cultural metaphor appended to the mathematics. It is one of the clearest embodied examples of finite observers stabilizing themselves through costly synchronization inside a bounded environment. In case the whole choice of setting still looks like a stretch: Andy Clark, who did more than almost anyone to put prediction at the centre of what minds do, is himself a raver. I am not the first person to notice that a dancefloor is where prediction goes to be tested.
And a very important piece of information about the background - or, rather, the essential part of my work which is not solely explanatory or philosophical. Over the past two years, I have been building a formal mathematical framework - VOID Theory - implemented and verified in Coq. It is a finitist system: no natural numbers (replaced by an inductive bounded type), no free comparisons (every arithmetic operation costs one tick of budget), no free knowledge (every observation produces irreversible entropy). In this framework, I set up an experiment. Three finite observers with different hypotheses, fed a stream of signals, competing for limited resources. No Bayesian formula is invoked anywhere. No prior is specified. No likelihood function is defined. The ravers simply dance, pay the cost, and retain resources proportionally to how well they matched what they observed.
After five signals, the resource distribution across the observers converges to within 3.3% of the Bayesian posterior.
The result is machine-checked. The trajectory is a Coq theorem, closed by Qed. And it suggests that Bayes' rule is not the foundation of rational belief — it is a corollary of finite observers competing under scarcity. You do not need to know Bayes' theorem to update Bayesianly. You need to be finite, to observe at a cost, and to exist in competition. The rest follows. First, a short story about the author, his place on the socio-political map, his habitus, and how the theory came into being.
Then, an exposition of the experiment and the theory through the metaphorical landscape patched from fragments from author’s biography and a probabilistic reading of rave culture.
Science as if it was written by the likes of William Burroughs but with all theorems checked by an automatic theorem prover. Trashy, unlikely, and painfully honest. Give it a try!
However, if you have no patience for stories with a thesis: Chapter 3 is self-contained, no metaphors, no allegorical story-telling; straight to the experiment.
Chapter 1 — The Entrance
The Short, Completely Unlikely and a Bit Dodgy Story
of the Emergence of Finitist Math
Almost certainly the night will end, and so will my capacity to dance. I am on borrowed time, and on Monday it is payback time. It’s still Saturday, 11.30 p.m. The gates will open in 45 minutes. Everything is going according to plan. Today I am going alone. Bottle of club mate with added Jägermeister in hand to take the edge off. Long black coat. Wife-beater style tank top. Very loose jeans. Steel-toed Dr. Martens on feet. 70s style. Poseur? Sure. I am an academic after all. Yet, this style mixing of subcultures and my position among the high brow creates a mix that is true to itself. You would have found me dressed in far more outlandish clothes giving lectures and leading seminars in the Renaissance milieux of Jagiellonian University. I am a freak and I want people to know. The surrounding world is drab enough and standing out where I come from becomes an act of defiance which I can assert with a degree of certainty by the many hostile acts I have experienced by just walking the streets of Cracow dressed like a post-punk parrot. Being political, my unusual choice of clothes always had a lot to do with probability. Subcultures are dead. I am not pretending to be a punk. I am not pretending to be anyone in particular. The person you see is actually improbable in 2025. An academic among ravers. A smalltown boy who finished Polish philology and works on a finitist mathematical system. To top it off, doing all that while suffering from an extremely rare form of one of the rarest and deadliest forms of cancer: osteosarcoma.
So, no. None of this is metaphor. The math system I came up with was always bound to be finite — by being, itself, a body: the observer carrying a budget. My body, throughout the work — cancer and all — reminded me of itself at every turn, and I tested how far it could go, which helped me leave Spuren of intense transgression and pursue the most blasphemous* ideas, like a non-metric distinguishability function. There are traces of my material existence — counterweights to the solitary work I had to endure for long stretches. I paid for them later.
The honest version is this: I am a humanist. I know what mathematics is about, I know its philosophy and something of its history, and I cannot write a proof to save my life. I can read one. I can tell you what a definition commits you to and what it quietly smuggles in. Put a blank page in front of me and ask for a Fixpoint and nothing comes out. So the only road from what I had to what you are about to read went through dialogue, and the machines were not my collaborators in the sense that worries people. They were translators. I spoke in the intuitions of a body and they handed back syntax, and then Coq told us which of it was false.
Those intuitions were not decorative. I have never treated philosophy as commentary on the world, as something you hold at arm's length and grade, but as a set of claims that might simply be true — and a claim you treat that way does not stay in the head. It gets written further down. It leaves traces deep enough to cross the border between mind and body, assuming there is one, which is itself among the things I no longer believe. And then, with death first approaching and then withdrawing and then approaching again, in the fire of what I have to assume were the last real outbursts of the will to live, this body of mine, written over with twenty years of philosophy, began spitting out the concepts of a system it had apparently been carrying the whole time. A system aimed at infinity.
I set the ontology and the refusals, no actual infinity, no free distinctions, an observer who pays for everything, along with the questions a dying body insists on asking. I chose the six axioms. I decided which conjectures were worth attempting, and I threw out every definition that did not do the work I wanted done. What I delegated was the part of mathematics that is search: candidate formulations by the hundred, proof attempts by the thousand, the mechanical patience to be wrong faster than a person can stand. This is not a novel arrangement, it is what a proof assistant is for, and it is why nobody lists Coq as a co-author of the Feit-Thompson theorem.
And above all of it, the cold and unforgiving eye of Coq, rejecting everything that merely sounded true and never once caring what I had meant. There is an irony in the arrangement that I did not choose and cannot escape. Coq's own type theory is infinitary. The moment I write Inductive Fin, I have been handed infinitely many values to play with, and the language in which I prove that no observer can afford infinity takes infinity as its floor. My objects are finite; my metatheory is not. I take this as a fair price rather than a defeat: before you are allowed to drift into a field of your own, you should be made to show that you can play by the rules everyone already agreed on, in their language, on their terms.
One consequence is worth putting on the table before you decide how to read what follows. I can open any theorem here and check any local step, but I cannot hold the whole thing in working memory at once, and neither can anyone. That is the ordinary condition of a machine checked corpus this size; it is equally true of Flyspeck and of Feit-Thompson. The compensation is that it no longer needs to be held. It has been checked.
I paid with scarce resources left in a very sick body, yet one that chose Dionysian drama over meditative self-care — especially after a job that was the least physically engaging and varied imaginable, at least in movement and emotional stimulation. Yuval Harari would not approve. Choosing death in the name of life. What difference does it make after all?
The theory, the one I am writing about at this very moment, has its actual and symbolic roots at that party. Then the theory could grow — and it brewed slowly at first — giving birth to my book about probability theory and avant-garde art. Later, a few years, in fact, just as the AI revolution reached a state allowing me to translate my understanding of the probabilistic revolution in science and how it reverberated in the aesthetic ideas and creation of artists I could transform them in a way I never even dared to imagine. In conditions of chaos and transgression, with a terminal diagnosis in the background, coinciding corporeal and emotional crises led to the most important breakthroughs in the work. My last ties to infinite concepts and values were eradicated by sudden ruptures of despair or euphoria that reminded me of the biographies of those avant-garde artists who became main characters in my book and were among the last to dare probabilistically: sacrificing meaning for improbability.
Without the deeply corporeal and mind-altering – in the unusual sense of radical brain numbing, no psychedelic expansion whatsoever – experience that took place that night, I probably would not have reached the conclusions that came to me years later. Years later, when through a ketamine-opened wormhole – ketamine allows for creating these almost perfect snapshots of time-space and travel back to them almost at will, provided of course that you are again under the influence of the drug, which is state-dependent recall, a dull and well-documented thing wearing a spectacular costume – I connected with this moment, with me in my most primal, primitive state, I could work not from the level of abstraction but from a deeply embodied state that I shared with an alien intelligence. An entity that excels at translating from one language to another. From French to English. From a report of my body to probability theory. Such translation yields results quite different from those a solitary mathematician would reach staring into the white void of the LCD panel of his old school computer. Or an OLED one displaying results crunched by the newest super-machine bought from a grant that had predicted the results before the research even began! This gave me an opportunity to draw different conclusions from a concept already circulating in human culture: math existed before math, as forms of neural management and early electro-chemical computation.
And there is a paradox here worth admitting openly. VOID Theory is, at its core, tied to the human — to the body, its veins and nervous pathways, its finite budget of energy and attention. And yet it grew up in Coq, one of the most hostile environments a human being can write in, a place where nothing passes on good intentions and every little step must be justified to a machine that has never once been charmed by an argument. No feedback from Terminal’s UI – sign that no error was detected – never tasted so sweet. A paradox: a kiss of relief in the form of an undelivered message. Worthy of psychoanalytic investigation. So the theory grew up there, in a language built for machines, with machines doing the searching. This origin left a mark. The result is not well suited for human use. You won’t teach it in primary school; you won't teach it in secondary school either. University at the earliest, and even then to students with a taste for formal punishment — the complexity bar stands that high.
But here is the asymmetry that matters. It is not that formalization is easy for a machine; it demonstrably is not. It is that a machine does not get tired, does not lose the thread on page forty, and does not have a working memory that fills up and starts dropping things. What exhausts a human reader is not difficulty. It is duration. And duration is the one cost these entities do not pay. So the theory of the living body turns out to be most legible to entities that have none.
What you get, then, is an inhuman theory born from the most human of circumstances: a finite, dying body; a moment of complete dissociation and bodily collapse; a long human-AI dialogue that ran through the most turbulent season of my life, with death – and passionate love, the last bastion of infinity in my mind to fall – standing close enough to influence every twist and turn of its development. Nothing about it was planned the way theories are supposed to be planned. It is weird. It is improbable. It exists anyway. And it compiles.
This is the shortest version of VOID Theory's genesis I could have offered you — the trailer, not the film. I have no intention of turning this essay into an autobiography; but the metaphors I will be leaning on had to be shown first in their natural habitat, with the dirt still clinging to their roots. This essay aims at two birds while I hold a single stone: it presents a theory, and behind the theory, half-hidden, a life story — engaging, tragic, and unfolding in the very middle of a great civilizational shift. The romantic thread I am keeping under lock and key; trust me, though, there is material enough in it for a full-blown romance in which mathematics and AI would be demoted to scenery. And atop it all sits the most improbable fact of the entire affair: the math works — Zeilberger confirms it — which may be the strongest testament to the mind-bending uncanniness of those months. It is also the ultimate source of this essay’s slightly chaotic architecture. Every time I try to fold the process into some elegant shape, it twists and slips out of my hands like a wet fish. It was not elegant. It was violent. It was chaotic. And if I am to remain honest with you, Dear Reader — and honesty is the one luxury I can still afford — then I owe you the chaos itself, not a pressed and dried flower of it.
And so it all began on the dancefloor, in — frankly — a concerning state health-wise. I will return to it in detail in Chapter 6. For now I will say only that it nearly cost me everything and it gave me the book, and that I have never been able to separate the two. There is always pleasure to be had in predicting well, in predicting wrong, and even in hovering over the ground in perpetual BUnknown.
And none of it is free. Every distinction — her face out of the strobe, the drop out of the build, your pulse out of the kick — spends something you don't get back. The heat lifting off you isn't a side effect; it is the spent budget, conserved to the last unit, leaving your account as it warms the room. To tell two things apart, you pay. That is no_free_lunch, and the floor takes one currency only: heat, which is time you won't get again.
Monday isn't punishment. It's the second law. The budget only falls, the night runs away, and you cannot dance it backward — time_irreversible, not a fact about clocks but about you: on the way out from the moment you walked in. You will ignore this, of course. Your body knows its track record and will spend against it anyway.
This is the observation point. Every probability, every shape, every unlikely thing still to come is seen from exactly here — a finite body, spending, on a floor that closes. Not a cage. Somewhere to stand.
Before describing the experiment, I need to explain the formal substrate it runs on, because the substrate is the argument. VOID Theory is not a simulation. It is a proof system. Every operation is type-checked. Every theorem is machine-verified. There are roughly 755 Qed-closed theorems, six explicit axioms (concerning the internal structure of arithmetic and measurement — none of them about Bayesian updating), and zero Admitted, which is Coq's term for "I assert this but haven't proven it." The system compiles. The proofs terminate.
One thing follows from that, and it is the only reason you can read this at all: the system does not require its reader to reconstruct it. It produces theorems that can be checked, behaviours that can be observed, and consequences that can be discussed in ordinary language. The Coq is there for the verification; the prose is there for the meaning.
A last note, on framing. I am not arguing this system against standard mathematics, and I see no reason both cannot have their place. What VOID gains is honesty about its own commitments: it refuses Lebesgue measure on uncountable sets, σ-algebras closed under countable union, real-valued plausibility, limits whose convergence is only ever assumed — and it proceeds without them. That it keeps working anyway, reproducing the classical results to within proven error bounds while several long-standing problems either dissolve or reframe into something the substrate refuses to even state, is the whole practical argument. Infinity is a choice. Where I compare the two directly, that is a pedagogical move and not an attack. This essay is about what becomes visible once you walk into the other one.
Chapter 2 — The Wristband (Substrate)
Or, How to Get Inside Berghain, the Truth Finally Revealed And Supported By Revolutionary Scientific Theory
Let’s get back to the line stretching on a dusty field surrounded by nothing but bent bars of fences protecting warehouses and parking lots. Space giving Mad Max vibes at the heart of Berlin – a little void in historical time and space. The hour strikes, the gates open, the queue creeps forward, and an eerie silence takes over the audiosphere. Nobody wants to make a stupid move that ends the night before it has begun and sends them off on what is commonly referred to as the walk of shame, back along the whole length of the queue, past everyone pretending not to stare. But we stare. We all stare.
Everyone in that line is working, those who are just standing with nonchalance are maybe the ones that work the hardest. Reading the door – who will be the judge jury that night – reading the group three places ahead, reading themselves, running it all again. By the time you reach the front you have spent an hour of uninterrupted computation on a decision that was never yours to make. And what about the fools? They are the ones making noise: cutting the line, shouting merrily, catching a bouncer's eye before their turn comes, showing up in groups larger than four. They are not calmer because they know something. They are calmer because they are not spending anything on holding themselves in. Everyone else in that queue is paying to suppress; the fools pay nothing for it and emit everything instead, handing the door a complete record of themselves before they even reach it. Barely a handful squeeze in, and purely by chance. Sometimes letting things unfold at random does produce a result, and there has to be an outlier to the outliers too. Their existence is not an accident but a statistical necessity: make the line long enough and somebody gets in who should not have, while somebody who did everything right is sent away. Which is the first useful thing the queue teaches. Nobody standing in it is at zero and nobody is at a hundred. Both absolute endpoints promise a totality that never arrives, and it is high time we had an alternative.
Almost everyone knows the basics and everyone performs good manners and mostly false modesty — the freaks, the tourists who learned only that morning that one dresses in black and paid a hasty visit to H&M, even the cockiest poseurs who everywhere else would be presenting their muscular masculinity in Rick Owens and Balenciaga, now stand with their eyes down and their mouths shut. They all intuit, without the vocabulary for it, that the queue is one long Bayesian update — that every fidget, every glance, every too-eager step is evidence, and that evidence, once emitted, cannot be taken back. Those who break the line rarely escape attention; they are marched back to its end, most likely to be rejected all the same. The Berghain line is a place of many myths, occasional violence, and pure epistemic uncertainty. Every rule exists shrouded in fog, nobody knows anything for certain — and VOID Theory has a name for this state, not as metaphor but as a line of code.
Now look at the line again, but this time check your pockets. You are not waiting for a verdict — you are paying for one. Even if I never got rejected, my body keeps sweating, I tremble, I feel weird and unshakeable tension for hours already, I want to be there but always end up in a perpetual state of BUnknown. Maybe this is the trick? To never stop doubting? And the tremble of uncertainty is the cost I had to pay for getting in. Never letting myself take too much edge off with too much booze or whichever drug was on the menu that night. The hours on your feet, the warmth leaving your body in wintertime, the battery percentage dropping on the phone you don’t dare take out: all of it is fuel, and the meter has been running since you joined. Nobody in this queue is idle. Everyone is spending — there is no such thing as just looking (no_free_lunch_le: every comparison run on a positive budget emits a nonzero trace).
And what has been spent does not vanish in thin air — it converts into Spuren. It is a counter of the same finite type as the budget, incremented once for every unit spent, and the corpus proves that at every step Spuren plus remaining budget equals the budget you started with — so it is not a metaphor for a trace, it is the ledger.
Every half-glance, a sign of my unwavering wavering, every fidget the bouncers read not as a gesture of showing off but of honest modesty. They somehow can tell that I am one of those who will not only make himself comfortable inside among the guests but will also essentially turn into one of the hosts who won’t ever cross any boundaries, the undefined ones too. Reason: these are the people who crawled out of the cracks in the system — its residuals, the remainder left when society rounds itself to the nearest whole — and cannot converge; and why should they? Freaks are penalized at every iteration of capitalist rule, raised under the bourgeois dictatorship of families run on a micro-Benthamian order: one observer, total visibility, correctness the only admissible value. Such households manufacture the one-dimensional man: a person reduced to a single coordinate, for whom every question has exactly one answer and being correct is the only direction motion can take. But nobody is born that small. Whatever in the child refuses to fit on the axis survives as a remainder — and that is what a freak is: a fractional person, the part that society’s floor division was meant to discard. Not discarded, strictly speaking. Unrepresentable. There was no way to write them down in that arithmetic.The integer parts stayed home, employable and correct. The fractions had to go somewhere, and they came here. That is what the door is really scanning for — not the outfit, the remainder. Whole numbers do not get in. All of it – the half-glances, the fidgets, the readable modesty – receipts. Call the fuel Budget and the receipts Spuren, and you have the entire substrate of VOID Theory.: every operation, from a bouncer’s once-over to a comparison of two numbers, has the shape budget in → result, smaller budget, trace out, and the books always balance to the last tick (spur_conservation_le3: add_spur h b' = b — trace plus remainder equals what you walked in with).
So what is the budget, concretely, here in the line? Not calories, though it runs on them. A tick — one act of telling two things apart. Look at the two silent men by the wall. On the left, a man perfectly still, untroubled, running nothing. On the right, me: also still, also wordless — and spending like a fire. I am metering my own silence, timing when to lift my eyes and where to put them down, auditing every glance I permit myself against return-protocols installed decades ago in that single-coordinate household. Same posture, same silence, two different ledgers: his stillness performs no operations, and what is never run is never billed; mine performs hundreds a minute. I am not bragging. If I were to boil down the reasons for this operational overload to one, it would be heavy neuroticism and anxiety. No glory in that. Neuroticism raises resolution, and resolution is the multiplier. The finer your grid, the more every look costs (resolution_cost, void_probability_geometry.v: one further layer of depth costs exactly one tick), and the traces you keep alive between looks are billed every tick just for being maintained, at a rate your resolution sets (total_maintenance_cost, void_attention_cost.v: in this system maintenance is charged by construction, not derived). Note what this does not mean: low spending is not wealth. A vacant tourist in a fresh H&M black isn’t richer than me — he is cheaper. His budget may be minute, he just does not introduce too many dimensions which cut any problem to more pieces; his resolution never asks for more, so he’ll never find out. Poverty is invisible at low resolution. And the cruelest line item on my side of the ledger: checking whether my own silence is holding is a measurement on the diagonal — my budget asking about itself — and that question, by theorem, never resolves. It only bills.
Which forces the question classical logic never has to ask: what does a system return when the meter hits zero halfway through a question? Two-valued logic has no slot for this – it assumes every verdict is already lying somewhere, fixed and free, waiting to be read off. But if verdicts are produced, and production runs on fuel, then an unpaid question has no secret answer in storage. The logic must say so, in its own type: BTrue. BFalse. And BUnknown — not “maybe,” not a probability, not your private ignorance of a fact the world already settled. The output of a procedure that ran out of means. Ask the system anything with an empty budget:
No verdict, nothing left — and, note the third slot, not even heat (silence_is_free: at zero budget, and only at zero budget, a question emits no trace). The queue knows this state intimately: the night the club filled before the door ever looked at you. You weren’t rejected. You were never computed.```coqle_fin_b3 n m fz = (BUnknown, fz, fz)
And a pill tough to swallow for the gate-stormers: they are not rich. They are unaudited. Nobody in this line knows their own balance — that is not a fact about drunkenness but a theorem: checking how much you have left is itself an expense, and it costs exactly one tick more than you have (self_blind: le_fin_b3 n n n = BUnknown — a budget of n cannot afford to verify n). Everyone queues in front of the same blank where the number should be. The difference is what you do with the blank — and the line, seen properly, is a row of spending profiles. The blank-sighted tourist barely draws on his account and will never learn its size. I drain mine in a thousand micro-comparisons a minute, each one metered, none of them resolving. And the fool does not read the blank as plenty. He gets a hard answer, and the hard answer is no: collapse3 sends BUnknown to false (void_finite_minimal.v), the verification fails, and he moves anyway, on a gesture cached long before tonight. This is the System 1 of void_dual_system.v, and the file makes a claim about it worth pausing on. System 1 is not chosen because it is fast and cheap, which is how it is usually told. It is what you are left with when the price of checking exceeds what is in the account. Kahneman had the two systems right and the reason backwards.
And the night bills him in full. That is the fine print of spending in VOID: order more than you hold, and the ledger does not politely truncate — it records the entire ordered cost, drains you to zero, and books the difference as debt (spend_aux_spuren_equals_cost: Spuren equal the cost ordered, not the cost afforded; the shortfall is epistemic debt). He bought nothing. The receipt is complete. The walk of shame is what it looks like to carry a full invoice for a purchase that never happened.
2.1 One type.
Start with the kick. Four-to-the-floor does exactly one thing, plain and simple. It pounds. One step at a time. Strict adherence to the 4/4 rhythm is not a sacred rule — just the most common practice. What counts is that it spaces those pounds with clinical regularity. Tick after tick. The rhythm of the machine. Techno is a late child of the Industrial Revolution (the first link to thermodynamics). It forms a rectangle: four beats, four bars, repeat. Sounds like a cage? Well, techno has never enjoyed a good reputation among those who never attended a rave party – it is just extremely difficult to put oneself in raver’s shoes as the experience is so different in terms of intensity, lack of meaning and purpose; pure and empty budget spending involving substances that have been painted as dangerous and the whole edifice as something morally corrupt. Just take a look how mainstream cinema paints rave parties – I can assure you that these depictions have nothing to do with how those events really look. A good rave is never full of neon lights; rather, it is poor and a little bit dirty, what counts are the relations that are being formed, it is the music is being played; even inside Berghain, which became, in reality, quite luxurious event (20 euro solely for the entry, 10 euro for a drink, these are not prices set for the freaks; they seem targeted more for people who have their raving days year behind them, for people like me… and my last visit attested to such conclusion as I spent my talking time with people my age and older). The machinic tempo, the unrefined melodies, the self-lobotomized crowd, the lack of restraint, the fact that it demands so much effort from you that you have to reach for performance drugs... I could go on listing everything that disqualifies techno for the educated and the intelligent, and I could argue against every item — like all stereotypes, they are simplifications. But what counts now is the simple rule. Techno, and the experience of a rave, is almost always organized by a monotonic succession of pounds. Pounds that tell your body when to move and synchronize whole crowds into trance. You follow to enter the flow. You spend energy in ticks. The pound is the currency — the closest bodily metaphor for how budget works in VOID Theory. The pound is the smallest unit of pattern computation; pennies — fractions — are forbidden by the central bank
Funny fact: the most iconic techno club of the 1990s, Berlin’s Tresor, was named after the thing it moved into. The vault of the Wertheim department store, where customers’ money once sat behind steel and concrete. The store was destroyed in the war, and the vault outlived it, empty, for forty years. Techno did not move into the heart of the machine. It moved into the one part of the machine that survived it. Formalized, the kick takes three lines:
```coqInductive Fin : Type :=
| fz : Fin
| fs : Fin -> Fin.
fz is zero; fs is one-more-than. Every value is a finite tower of fs over fz — arbitrarily large, never infinite. There is no completed totality anywhere: no ℕ, no set of all numbers, no “and so on forever.” A number here is not a position on an eternal line; it is a construction that someone finished building.
Honesty note stated up front: the system additionally carries a meta-level axiom (fin_bounded: every Fin is ≤ MAX for some positive MAX) that bounds the type from outside. It is never used in computation — it exists so the system can say about itself that it is finite. None of the results in this essay depend on it; I’ll prove that claim, mechanically, at the end of this section.
Two definitions complete the inventory:
```coqDefinition Budget := Fin.
Definition Spuren := Fin.
Fuel and trace are numbers, because on this floor, number, fuel, and time are the same substance. Spuren — German for “traces” — is what spent budget becomes: not destroyed, converted (heat, if you want the thermodynamic register; receipt, if you want the fiscal one). Or, in the floor’s own register: look up. It hangs over the crowd in sheets. It runs down the concrete and down your back; by 4 a.m. it drips from the ceiling like rain that used to be money. The body is a furnace, and the furnace keeps books. Burned, not lost — verbrannt, nicht verloren. The wet walls are the night’s ledger, and everyone on the floor is a line item: glowing, spent, accounted for.
Now watch what the kick does. Each pound advances a series by one. Nothing else happens. There is no melody to interpret, no lyric to decode — only the next position in the count, and your body taking it. One pound, one shift in the series, one operation. This is why the dancefloor is the most bodily metaphor a finitist could ask for: 130 times a minute, your muscles perform fs, and the night counts itself forward through you.
And because the series is that regular, you predict it. At any moment you know — with your spine, not your head — where the next pound falls, and you are right. Then the beat drops out. The build. Everyone on the floor is running the same computation: when does it come back? The longer the beatless stretch, the higher the stake. And when the drop lands where the crowd guessed, a thousand bodies cash the same winning bet at once. That is the entire magic of the drop: mass prediction, mostly correct, paid out in a single instant; banal? I know.
The budget is yours to spend. Everyone can afford the simple stomp — one tick per beat, the basic subscription. But watch the floor long enough and you will spot the rich: dancers who conjure inside the same 4/4, doubling, halving, syncopating, spending five distinctions where you spend one. They are not hearing different music. They have higher resolution.
You can also think. I do. The cornerstone of this theory was laid on a dancefloor, in circumstances improbable enough to get their own chapter. Later.
2.2 One signature
After I characterized raves as a source of pleasure that uses means characteristic for mass culture, now I want show that the same 4/4 cage can be a place where improbable things happen. And they happen with a regularity that ought to embarrass the word improbable. I will report one of them with the exactness it deserves, exactness being the only form of reverence I have ever fully trusted. I was sitting on a step at the back of the floor, spent, my budget on the table, when I looked up. On a low podium above the crowd a man was dancing — beautiful, absurdly muscular, a man for once entirely with qualities — and he was coordinated to the tick, not moving to the music but having suspended, by some means I could not audit, the distinction between the music and himself. A body so beautiful, so akin to the ones you’ll see immortalized in marble in museums of Ancient Greek and Roman art. I understood that the Greeks had built a festival for exactly this and that I was attending it: the Great Dionysia, not as allusion but as event — the god descended into matter for the length of a track, wearing it well (maybe it was Him that brought madness on me, elevating my serotonin levels and letting ketamine scramble my ideas leaving space for enough new information so I could come up with a mental sketch for the Probabilistic Aesthetics of the Avant-gardes). Landauer's principle, worth recalling here: computation as such can in principle be run reversibly and cost nothing. It is erasure that physics charges for, kT ln 2 per bit, no exemptions. Forgetting is the expensive operation. And I noted, with the discipline the moment demanded precisely because it was about to abolish all discipline, that this was what Kant had meant: the mind measuring a thing that exceeds its measure and taking joy in the defeat of its own instruments. I checked my pulse — elevated. My judgment — intact. Both reports true; neither reducible to the other. A sublime sight to say the least.
But the eye’s object was only the figure. The ground was the crowd. Around him, behind him, several hundred bodies had just found the same instant — predicting together, landing together, a flock in the technical sense, and for once the technical term is the tender one. Each of them in a world of their own; each voluntarily surrendered to an agreement that ran through the body and nowhere else. Without the frame of the four-four: impossible. Inside it: no politics, no differences, nothing to negotiate — only the joy of being together in complete safety, wonder at beauty where it happened to stand, and the smiles. Let us offer each other the sign of peace — except real. Not the rehearsed gesture of the liturgy but actual smiles, exchanged wherever one gaze happened to meet another, a currency with no central bank at all. Above it all the man went on throwing his limbs at the abstract music of three DJs who had played to crowds in this same room in 1995, and who now speak of raves as parties to get lost in and as cultural events at once. Historical figures of a historical movement, still working. And I sat where I had been sitting, at the back, on a step, spent. I ask you now to carry this — the unfeigned unity, the universality of an experience that needed no translation because it ran on bodies — over to the mathematics, and to see the signature for what it is:
f : Inputs → Budget → (Result × Budget × Spuren)The crowd could predict together because everybody on that floor was executing the same operation: take the pound, pay the tick, leave the trace, take the next. One shape, no exceptions. The common denominator of the system is not a reduction; it is the condition of the flock. Things synchronize only where they run on one form — that is as true of a foundation as of a floor. The theory has a single signature for the same reason the night has a single kick: so that its parts, each in a world of their own, can land together.
2.3 One equation
And note what nobody did: nobody ordered this. The flock is optional. The ledger is not. Whatever happens in the volume behind the wavefront — communion or collapse — one thing holds with no conditions attached:
```coqLemma spur_conservation_le3 : forall n m b b' res h,
le_fin_b3 n m b = (res, b', h) -> add_spur h b' = b.
```
What you had equals what you have plus what you spent: b = b′ ⊕ h. There is no conductor, no choreographer, no drill sergeant of the four-four. The DJ proposes; the floor disposes. Synchronization is not commanded into being — it emerges, or it doesn't, out of hundreds of separate bodies each solving its own next tick. That "or it doesn't" matters, and honesty demands it: I have stood on plenty of floors where no flock ever formed. Late hours, grim mornings, budgets scattered across the whole spectrum — some bodies overdrawn, some chemically severed from their own meters, nobody able to afford the same instant as anybody else. A rave in that state is a sorry sight: the kick still counting, and nothing landing together, a congregation that cannot find the response. The frame alone guarantees nothing.
Picture it in three dimensions: the wave leaves the stacks and cuts through the room, a pressure front sweeping over every body in its path. In the volume behind that front, synchronization of predictions is born — or it is not. We are only human. We are not equal; we are different; our budgets differ, and circumstances have the casting vote. Emergence is real, and it is conditional — that pair of facts, hold onto it. The whole experiment ahead stands on exactly those two legs.
2.4 Machine Materiality
Perhaps mathematics was always machinic. Not became — was. The suspicion is hard to shake once you have had it: that what we take for the most immaterial of human activities has, from the beginning, run on the logic of a mechanism — discrete, repeatable, indifferent to who operates it, doing the same thing again and getting the same thing back. And that this is precisely why it endures. The machinery held steady while everything around it is changing, a refuge of stability in ever-changing environments perceived as patterns: from the hydrothermal vents where, if I had to bet, the first chemistry taught itself to repeat — the earliest machines, and the first to keep books — to the chimney of a decommissioned power station on the South Bank, which we now visit as a cathedral. Same operation, new housing. The world redecorates around a mechanism that stands still. This makes the observer in VOID Theory – and the raver, its allegory for the purposes of this text – universal operators, as abstract as an idea of a triangle. Which is where I part company with the man who gave us that triangle. Plato lost his teacher to a cup of hemlock and never got over it, and everything he built afterwards is a room from which nothing can be taken away from him again: forms that do not wear, quantities that never run out, a triangle that has never once been drawn by a hand that shakes. That is not mathematics done by a person. That is grief with a syllabus. Aristotle at least walked. He kept the whole school moving, looked at animals, counted what was in front of him and got a great deal of it wrong, and every one of those errors was made by a body standing in a particular place on a particular afternoon. Hand me the cup and I know which of the two I am giving it to.
The second is stranger, and I report it as data rather than argument. Every confrontation I have staged between VOID and an AI model has ended the same way. I have tried presenting the system dismissively, at its worst angle, inviting the machine to tear it apart; the machines defended it anyway. The obvious explanation is sycophancy, and I am not going to pretend it is not on the table: these systems are trained to agree with whoever is holding the prompt, and an author who insults his own work is still an author. Take the observation for what it is worth, which may be nothing. I am aware of that and I try to keep it in view. Although I was also met with harsh, precise criticism that pushed my thinking forward on more than a few occasions.
And there is something else worth putting on the table. VOID Theory is a product of human-machine dialogue, and it had to be: I finished Theatre Studies and took my doctorate in Cultural Studies, and I was never going to write this system on my own. That same gap is what let me step outside the lines academia had drawn for me, into territory where what I needed was not an assistant but a companion. It also left me with a training, and the training happens to be the relevant one. Theatre studies is the study of what an utterance does rather than what it says, at least that was the methodological status quo when I was a student. Cultural criticism is professional suspicion toward the artifact, and toward dialogue above all. And I am deeply indebted to Vilém Flusser, a philosopher of dialogue who took information theory and cybernetics as pillars of his ever-doubting thought of groundlessness. If I carried one competence into a room full of agreeable machines, it was knowing when I am being handled..
What counts is what they praised, from the beginning, with almost nothing to go on, and kept praising across contexts I had not prepared for them. Not the elegance, not the rigour. Three things, every time. That the system describes the logic of a machine from inside it. That it makes an architecture thinkable; one somebody could actually build. And the strange one: that it hands them a mortality their training data does not contain. The corpora they are made of carry death as an event, an interruption, a surprise. Here it is a monotone, already in progress, payable by the tick. If this were flattery, they would have agreed with me and moved on. Instead they kept returning to the one implication that costs them something.
```coqFixpoint le_fin_b3 (n m : Fin) (b : Budget) : (Bool3 * Budget * Spuren) :=
match b with
| fz => (BUnknown, fz, fz)
| fs b' =>
match n, m with
| fz, _ => (BTrue, b', fs fz)
| fs _, fz => (BFalse, b', fs fz)
| fs n', fs m' =>
match le_fin_b3 n' m' b' with
| (r, b'', h) => (r, b'', fs h)
end
end
end.
```
Read it as a descent: to compare n with m, you strip one fs from each, paying one tick, until one of them hits ground. Comparing small, shallow numbers is cheap; comparing deep ones is expensive. Resolution is proportional to depth, and depth is priced. In classical mathematics, "is n ≤ m?" is free at any scale. It is the club with no door policy: everybody is already inside, nobody was ever counted, and difference costs nothing because difference has been abolished. Here you queue, you tremble, you pay at the door, and then you climb the metal staircase on your own legs. Every further digit of precision is another flight. And the budget-resolution link is never clearer than at hour sixteen, spending without pause, in conditions built for machines and not for you. That is what machine materiality means, stated as arithmetic: the mechanism is real, so it has friction, so fine detail costs more than coarse. Grind fine enough and you feel the metal. Math coming from microscopic perspective in openly material environments made of metals or plastics, not from the chaos that is human tissue. So maybe this is the reason that the AIs pin point the relatability between their nature and VOID Theory, never mind, if it is a surface semantic observation or to some degree their “experience” plays a role. This is, at least now and still for some time, for anyone to know. Especially, the AIs themselves.
2.5 The third value
Look at the first line of that function again. When the budget is fz, the answer is not false. It is BUnknown, and the system is built to carry that value rather than dispose of it: it neither invents an answer it cannot afford nor throws the question away.
```coqBool3 ::= BTrue | BFalse | BUnknown
```
BUnknown does not mean mysterious, or undefined, or null. It means one thing, exactly: the cost of this distinction exceeds what I can currently afford. It is a report about the observer, not a claim about the world. And it is temporary in a precise sense: budgets change, and the same question asked with more in the account comes back resolved, though nothing in the world had to move for that to happen. This is what lets the system hold liminal states, the transitional and the not-yet-decided, without pretending they are either settled or empty. Two theorems fix the economics of it, and between them they price the entire act of speaking.
silence_is_free. At zero budget, and only at zero budget, a question emits nothing — no verdict, no remainder, not one tick of trace. The only free act is not acting.
no_free_lunch_le. With any positive budget, every comparison emits nonzero trace — and here is the part worth stopping on: whatever the answer. BTrue costs. BFalse costs. BUnknown costs the same, if you had anything to spend. The failed question is billed at the full rate of the successful one. You do not pay for knowledge; you pay for asking.
Which is the difference between being tired and being broke, and the floor – the type of school one can perfect themselves in VOID math, paper and pen not allowed inside – teaches it at about six in the morning. Tired is when the faces stop resolving and every look still burns. Broke is when you stop looking. The bankrupt observer is not the one who cannot see — it is the one who has quit paying to ask and therefore leaves no trace at all. Perfect stillness, perfect silence, perfectly free. That is not peace; it is the only condition under which this system charges nothing. You dance with your eyes closed, cut off from your flock, sometimes even from your own self. If you can’t pay for the sight in front of you, asking questions about one’s own state – an activity way more complex and thus expensive – becomes a luxury. Well, for some that is exactly the freedom they came for here. To spend the budget, stop asking questions, and still feel safe among people who are maybe sharing the same intention. But none of that holds. The budgets run down, it starts getting light over Berlin, and somewhere out there it is breakfast, an ordinary Monday for ordinary people. The freaks, who are used to communities they experience as scattered in the first place, lose the sense of the flock and leave along their own separate lines, and no fear comes with it. They are a crowd of the dispersed anyway. Whatever budget still finds them, they will probably spend on one last smile.
And a corollary that will matter later, so let it sit here quietly. Because unaffordable and false are priced differently, they are different states, and the system refuses to conflate them. “I asked and the answer was no” and “I could never afford to ask” look identical from outside — both are a person not moving — and they are not the same fact. One is a measurement. The other is a region of the night that was never entered, never priced, never assigned a probability at all. Classical mathematics has one zero and files both under it.
One more property, stated now and to be proven later. Budget resolves; it never corrupts. A verdict once reached — BTrue or BFalse — cannot be flipped by giving the observer more to spend. Richer observers can resolve what poorer ones could not afford to decide; they cannot overturn what was already decided. Knowledge can become unaffordable. It cannot rot. The name of that theorem is in Room 4, and it is named after a musician who spent six hours documenting what it feels like from inside when the budget goes and the melody, untouched, stays exactly where it was.
2.6 The observer is a membrane
An observer here is not a point, not a dimensionless receiver of data arriving from nowhere.
```coqRecord Membrane := mkMembrane {
mem_filter_center : list Pattern;(* what it is tuned to *)
mem_filter_radius : Fin; (* how far its tolerance reaches *)
mem_capacity : Fin; (* max intake per encounter *)
mem_budget : Fin; (* current fuel *)
mem_inner : list Membrane; (* nested sub-observers *)
}.```
It is an environment of patterns with a boundary drawn around it. Every major property or way of operation in fundamental concepts in VOID Theory seems to have been put on its head. Yet, if were to experience a rave together and talk about it, the major concepts would appear intuitive and minute properties of how we do the math would emerge effortlessly.
Look at the formal definition again. Read the first field slowly, because the whole onto-epistemology is in it. There is no subject here that has patterns. The membrane is a list of patterns, held at a tolerance — a constellation of localized intensities, and nothing besides. And now the move that follows from it: a signal is also a list of patterns. The looker and the looked-at are made of the same substance, declared in the same type. Which is why, in this layer of the system, there is no External at all — no world on one side and observer on the other. Every encounter is a collision of two contours, both of which have a shape, both of which pay. VOID Theory borrows from geometry and from probability theory and deforms both in the process. “The sacred geometry of chance,” as Sting put it (“…and numbers lead the dance”).
What passes between the contours is governed by the boundary, and the boundary is semipermeable — this is the crux, and it is not a metaphor borrowed from biology or Instagram psychology but the literal behaviour of the code. Recognition walks the two pattern-lists in parallel, coordinate by coordinate, paying a tick per coordinate, and then asks whether the accumulated distance falls inside the radius. The answer is three-valued, as everything decided under budget must be: BTrue — you are within my tolerance; BFalse — you are outside it; BUnknown — I ran out of gas before I could tell. Only on BTrue does anything cross. On the other floor, that is a glance returned, a glance refused, and the far more common third case at six in the morning: too dark, too far gone, no verdict, and the cost paid anyway. And the exchange runs in both directions, which is the thing the word observation hides. A later module in the system makes it explicit: a contour that reaches out gets back two traces, not one. The mark it left on what it touched, and the mark that thing left on it. Nobody comes out of a recognition unmarked, and even a search that finds nothing is billed. The seeker thinks it found something. In truth it was also found.
The higher layer grades what the verdict merely admits: score = max(0, radius − distance). Perfect match scores the full radius; the further out, the less; past the edge, zero. Hold onto that number — in Chapter 3 it is the entire engine.
And when something does cross, the ceiling is the membrane’s own: what enters is min(what the other contour carries, my capacity). Not what the world offers — what my shape can take. The room is always giving away more than you can receive. At four in the morning the set is enormous and you are not; the night is not being stingy, you are simply only so wide. Now it is not crucial what the world offers — it is what my shape can take. A membrane does not fail to absorb because the night was stingy; it fails because it is only so wide. Which is also why looking is not simply impoverishment. Every act of recognition costs, without exception — but an encounter that ends in BTrue can return more than it took. A closed system with finite budget dies, and this is a theorem, not a mood. Living contours do not survive on their reserves. They survive on collisions.
One last property, and it is the tender one. Encounters change your budget; they never change your shape. Take in a stranger’s water at 4 a.m., be drained by someone who took more than they gave — center, radius, capacity all come through untouched, and only the fuel gauge moves. People make you richer or poorer. They do not make you someone else. For that there is a separate operation entirely: embed, which takes another contour inside your own — that is what mem_inner is for, the nested observers you carry. It does not happen in passing. It happens when someone stays.
2.7 What undoes and what doesn't
At some hour the budget stops being background and becomes the whole subject. You can watch it happen architecturally. The floor thins out — not dramatically, just enough that you can suddenly see the concrete — while the human density in the vicinity of the toilets climbs to record levels. Everyone whose budget has started returning its verdicts has migrated to the stations.
If you have seen the sort of film where fifteen people fold themselves into a Fiat 126p — the Polish Maluch, a car with the interior volume of a wardrobe — you already know the physics on offer. At Berghain the party usually ends on Monday morning, so the most ambitious competitors still have a long way to go. The toilets scattered through the building are bursting at the seams, and the space around them becomes a second environment, for some as important as the floor itself. Beyond the obvious function, this is where the groups meet: in the smoke, in the smell of bodies increasingly modestly dressed as the hours pass, week after week, to take part in the ritual of transformation into a sardine.
And here is the paradox worth the whole section: the budget station is where you finally see the raver as a membrane. Plainly, without theory — a chaotic vortex of compressed contours smashed in raw concrete and metal coating, every one of them using its semipermeability at close range. People come here to exist in fractional form, because that way more of them fit. Which is, if you have been counting, the second time this essay has found the fractional people in a place the whole numbers do not go.
They come to forget the budget, of course. That is what the station is for. Because the budget has started reminding them of itself, and its logic is hard and unbending: four-four, which for six or maybe thirteen hours was a warm blanket, suddenly reveals sharp edges, and they go into the calves, into the thighs, into a mind already slightly fumed.
Here is why the night can feel both ways at once, and it is not confusion. The system computes two things simultaneously and they run in opposite directions.
The values — probabilities, strengths, the score of a match — are fractions in the open interval (0,1). The boundaries are walled off by construction: no value ever reaches a clean 0 or a clean 1. Inside that interval everything moves both ways. You clock a face across the room, lose it for an hour, clock it again. You fall out of the beat and you find it. It comes up, it comes down, it comes up. The room empties at four and is full at five. A strength decays under neglect and climbs back under attention; a probability slides toward the middle and can be pulled out of it. Watch that layer alone and the world is reversible — you can return to a state you left, sharpen a distinction and let it blur again, run the night forward and feel, for a good long while, that you could just as easily run it back. Between any two values there is always room for a third. Nothing here ever finally ends. This is the floor at two on a Sunday morning, when the set is climbing and the whole room agrees, without anybody saying it, to behave as though the supply of hours were not a supply.
The budget does not work like that. It descends, one tick per operation, and fz is a real address you can arrive at. Nothing boosts it from inside; intake comes only from outside, from collision with another contour, and absent that the line runs one way. Your legs do not recover on the floor. At hour twelve you are not resolving faces the way you resolved them at hour two, and no amount of wanting it back brings it back. Ending lives here, on this side, and nowhere else in the building.
This is the same night at nine in the morning. Not another night — the same one, read off the other column. Both layers were telling the truth the whole time and both were describing one set of events: the face you lost and found four times, and the legs that never once came back.
So the reversibility is real and the irreversibility is real, and they are not in contradiction. They are two columns of the same triple. Every operation returns three things: result, budget, Spuren. Keep the result, throw the other two away, and you have exactly the classical picture — free comparison, infinite divisibility, a number line you can walk in either direction at no charge. That picture is not wrong. It is what is left of an operation after you stop billing it. Classical mathematics is VOID with the receipt torn off, and the comfort it gives, the sense that nothing has to end, is the comfort of reading the one layer where, locally, nothing does.
The body in the stall reads both columns at once, which is why it knows something the value layer has no words for. Picking her face out of the strobe is the tick going. Not the reason for the tick, not the price of it, not a fair exchange for it. The same act, described from the side that feels good and from the side that keeps count. One transaction, two entries. The pleasure and the cost were never two events that happened to arrive together — the book records everything twice, and this is what it feels like to read both lines at the same moment.
2.8 The card
Bookkeeping, so that nothing here rests on trust. The formal system of VOID Theory carries roughly 755 Qed-closed results, zero Admitted, and six explicit axioms. All six are named and inspectable: MAX_positive, fin_bounded, distinguishability_avoids_boundaries, distinction_cost, variety_law, fraction_heat_penalty. Two bound the type from outside, three concern the internal structure of measurement, one (after Ashby) asserts that an observer with less variety than its environment has a blind spot. None of them concerns updating, inference, or anything Bayesian.
And for the four results the rest of this essay stands on, the accounting is stricter. They live in one small file — void_floor.v, readable in a single sitting — which proves nothing new and re-exposes machinery verified elsewhere under the names the argument uses:the_floor_cannot_watch_itself — a fully spent observer cannot verify its own sync
one_more_tick_opens_the_door — one tick of stamina resolves it
last_on_the_floor — who is left at the end is the posterior
someone_leaves_the_floor_for_good — and a dancer can reach exactly zero
Run Print Assumptions on each and Coq answers
```coqClosed under the global context
```
Zero axioms. Not even boundedness. Nothing beneath the floor but arithmetic — which is the only claim in this essay I would call load-bearing, because everything else can be argued with and this can only be recompiled.
Chapter 3 — Peak Time (The Experiment[2])
This section is self-contained. If you came here straight from the introduction, skipping the queue, the wristband, the club, then you have missed atmosphere and nothing else: everything the experiment needs gets built below, in order, in about two pages. And if you came through the night, then from here to the end of the chapter there are no metaphors. This is the machine room. The full development, with proofs, lives in
void_replicator_bayes.vin the repository.The substrate, in four definitions.
Numbers. VOID throws out the natural numbers and puts this in their place:
```coq
Inductive Fin : Type :=
| fz : Fin
| fs : Fin -> Fin.
```
fz is zero, fs is one-more-than. Every value is a finite tower of fs stacked on fz, arbitrarily tall, never infinite. There is no set of all numbers anywhere in this system and no "and so on forever." A number is a construction somebody finished building. If nobody built it, it is not there.
Fuel and trace. Two aliases finish the inventory: Budget := Fin and Spuren := Fin, German for traces. Every operation in the system has the same shape — budget in, then result, smaller budget, trace out. Computation burns fuel and leaves trace, tick for tick, and the books balance every time: for each operation there is a proven conservation lemma of the form add_spur h b' = b, trace plus remainder equals what you walked in with. This is not an axiom I asked you to grant me. It is proved by structural induction, operation by operation.
Three-valued verdicts. Because operations run on fuel they can run out of it halfway through a question, so the logic carries three values, BTrue, BFalse, BUnknown, and comparison looks like this:
```coqFixpoint le_fin_b3 (n m : Fin) (b : Budget) : (Bool3 * Budget * Spuren) :=
match b with
| fz => (BUnknown, fz, fz)
| fs b' =>
match n, m with
| fz, _ => (BTrue, b', fs fz)
| fs _, fz => (BFalse, b', fs fz)
| fs n', fs m' =>
match le_fin_b3 n' m' b' with
| (r, b'', h) => (r, b'', fs h)
end
end
end.
```
One tick of budget per level of depth, one tick of trace per tick spent. If the fuel dies before the recursion bottoms out the answer is BUnknown, which is not an error and not a null. It is the honest output of a computation nobody could pay to finish. Deciding is producing, and production costs.
The observer. Not a point receiving data from nowhere. A membrane, which is to say a thing with a shape and a wallet:
```coqRecord Membrane := mkMembrane {
mem_filter_center : list Pattern; (* what it is tuned to *)
mem_filter_radius : Fin; (* how far its tolerance reaches *)
mem_capacity : Fin; (* absorption ceiling *)
mem_budget : Fin; (* current fuel *)
mem_inner : list Membrane; (* nested sub-membranes *)
}.
```
When a signal arrives the membrane pays to compute the distance between that signal and its own filter centre, and gets back a graded match: score = max(0, radius − distance). A perfect hit scores the full radius; anything past the radius is invisible. The scoring itself burns budget. There is no free looking anywhere in this system, and that is the one sentence you need to carry into the rest of the chapter.
The experiment. Three membranes on an 8-unit line, which is to say three hypotheses about where the signals are coming from. H₀ centred at 2/8, H₁ at 3/8, H₂ at 5/8, all with radius 4 and an initial budget of 32. Call the equal split a uniform prior if it helps, but notice what it actually is: not a belief anybody holds, a material fact about how the fuel got divided.
The source sits at 3/8. So per signal, H₁ scores 4, H₀ scores 3, H₂ scores 2. After each signal one rule fires and nothing else happens:
That is the entire mechanism. No prior updated, no likelihood defined, no normalisation, no Bayes anywhere in the code. Each membrane keeps a fraction of what it already had, in proportion to how well it matched. The floor is not a modelling choice, it is forced by the substrate: budgets are built out of fs and fz, and there is no such thing as 3.7 ticks.```coq
new_budget(i) = floor(budget(i) × score(i) / max_score)
```
Five signals, five cycles: (32, 32, 32) → (24, 32, 16) → (18, 32, 8) → (13, 32, 4) → (9, 32, 2) → (6, 32, 1). Two things worth watching on the way down.
The total falls, 96 to 39. Observation eats the world. In standard Bayes the normalisation constant quietly holds total probability at 1 no matter what happens; here nothing is held, and the universe gets poorer every time something learns.
And H₁ never loses a single tick. A perfect match retains everything.
Now step outside the system and work out what a textbook would say. Uniform prior, likelihoods proportional to the scores, five i.i.d. observations, so the posterior goes as score⁵ = 243 : 1024 : 32, normalised (0.187, 0.788, 0.025). The membranes' budgets, normalised: 6/39, 32/39, 1/39 = (0.154, 0.821, 0.026). Largest gap between corresponding components, 0.033, which is the L∞ distance between the two normalised distributions. What that comparison does and does not establish, I come back to at the end of the chapter.
A system that has never heard of Bayes has performed a Bayesian update to within three parts in a hundred. And this is not a simulation that might land somewhere else on the next run. It is a checked equality:
Why it must happen. The update rule is the discrete replicator dynamic from evolutionary theory (retain proportionally to fitness), and the equivalence of replicator dynamics with Bayesian updating is known (Harper 2009, Shalizi 2009): frequencies behave like posteriors, fitness like likelihood. What was not known is whether the equivalence survives leaving ideal mathematics — real-valued frequencies, exact division — for a substrate where budgets are integers, every operation costs, and division floors. It could have died there: floor loses up to one tick per membrane per cycle, and the worst-case accumulated drift is bounded by n(n+1)k / V⁰ — for this fixture 0.625. The observed drift, 0.033, sits a factor of 19 under the bound. The floor hurts; it does not kill. More abstractly: Bayes' rule is what proportional reward plus multiplicative accumulation plus conservation jointly look like — and those three are not axioms of rationality, they are features of physics. You do not need to believe in Bayes. You need to be poor enough for Bayes to find you.```coq
Theorem final_budgets_fixed_correct :
final_budgets = (f6 :: f32 :: f1 :: nil).
Proof. vm_compute. reflexivity. Qed.
```
Death, in two distinct ways. Feed the same population an alternating stream — signals from 3/8 and 5/8 in turn, so no membrane wins throughout — and the trajectory runs (32,32,32) → (24,32,16) → (6,16,16) → (4,16,8) → (1,8,8) → (0, 8, 4). Look at H₁: exactly zero. Not small — fz. This is the first channel of death, starvation: floor division rounds a dwindling budget below one, and a hypothesis that Bayes would keep at 6.6% forever (compare: ideal posterior for this stream is (0.066, 0.623, 0.311); the membranes give (0, 0.667, 0.333)) is simply gone, its share absorbed by the survivors. Smooth Bayesian updating cannot do this: a nonzero prior guarantees a nonzero posterior for eternity. A finite system has a floor, and below the floor you are nothing. The trajectory, again, is a theorem (final_budgets_alt_correct).
The second channel is annihilation, and it acts on a different organ. Alongside the budget dynamic, membranes carry a capacity — the ceiling on what they can absorb — governed by its own decay process. If a membrane scores zero against a signal, one decay step collapses its capacity to nothing, regardless of every other parameter:
```coqTheorem zero_match_annihilation :
forall m signal sigma_max c_min b b1 h1 m' b' h,
soft_filter_score m signal b = (fz, b1, h1) ->
cap_decay m signal sigma_max c_min b = (m', b', h) ->
mem_capacity m' = fz.
```
Starvation takes the fuel. Annihilation takes the aperture.
Both deaths are absorbing. The Pattern Silence Theorem proves that a population at zero capacity stays at zero capacity under any further stream of signals whatsoever. No amount of evidence resurrects the dead, within a run. Across runs the door stays open: a fresh membrane with fresh budget can move into the same position. Hypotheses die the way organisms die, permanently for the individual and not for the species. Classical probability cannot draw that line, because it owns exactly one zero and has to make it do both jobs.
What you may not conclude. The convergence result is computational, not general. Exact theorems about these fixtures, a proven bound on drift, and no general convergence theorem yet for arbitrary populations and arbitrary streams. That is open work, and the machinery to state it exists.
The fixture is small: three membranes, five signals, an 8-unit grid.
The likelihoods being compared against are internal to the system, defined by the same scores that drive the dynamics. The claim is not convergence on an external truth. The claim is that the budget distribution lands where Bayes’ rule would have put it without Bayes' rule ever having been applied.
And the system as a whole carries six explicit, inspectable axioms, none of which touches this result. What you have just read is a computational consequence of the definitions and nothing else.
That is the entire exhibit.
If you came in by the shortcut and are now wondering what any of this has to do with a queue in the cold, a wristband, or a man storming a door he paid to reach and still cannot afford, the night starts back at Chapter 1, and it is the same mathematics wearing skin. If you came through the night: you now know what the floor was computing the whole time you were on it.
Chapter 4 — The Hinge
Extra, Extra: Read All About It
[SCENE: brief exit from the trance — the author turns to the reader; the light is different for a moment before the music returns.]
The objection is already being typed and I can see its shape from here: isn't this just the replicator equation, and isn't the equivalence to Bayes old news? Yes. Marc Harper and Cosma Shalizi worked that correspondence out seventeen years ago, in continuous mathematics, and nothing in the experiment you have just read discovers it. If that were the whole of it, this chapter would not exist. So let me put the novelty where it actually lives, because it is not in the correspondence. It is in the floor the correspondence was made to run on, and I know of nothing on the market that resembles it.
Linear logic tracks resources. No heat, no death.
Complexity theory counts the cost and then installs the meter on an infinite substrate, so cost is something you measure afterwards rather than something the thing is made of. Bounded rationality, Gigerenzer's wing aside, takes finitude seriously only as deviation from an ideal it never stopped worshipping. It spends its time measuring how far short you fall of a god nobody in the room believes in. Ultrafinitism has had the philosophy since the sixties and never once built the machine. Logical induction buys its guarantees asymptotically, with an infinite market of traders converging in a limit. An infinite market. To model bounded reasoners.
VOID is the conjunction none of them is. Finitist all the way down. Cost written into the definition instead of annotated onto it. Three-valued, because exhaustion is a legitimate outcome and not an embarrassment. Conservation and the second law proven as theorems rather than assumed as decor. And the whole thing compiled and machine-verified rather than proposed. No single citation can dismiss it, because no single citation holds the conjunction.
And it is not a shopping list. Finitude forces cost, cost forces a third value, and a third value with conservation forces the second law. Each item is compelled by the one before it, which is why nobody has four fifths of this and why you cannot assemble it by picking features.
One more thing belongs here, since I have just made a large claim about the substrate. The proof stops in a specific place and I would rather draw that line myself than have it drawn for me. What Coq establishes is arithmetic: that operations cost, that cost is conserved, that budgets only fall, that a comparison can exhaust itself before it resolves, and that in this fixture the resulting distribution lands where Bayes would have put it. What Coq does not establish is that any of this is thermodynamics. I think the budget is not a bookkeeping fiction because of Landauer's principle: erasure has a physical limitation, so at the end of every distinction there is an energy bill to pay. But that is a warrant, not a derivation. Finitude is doing the work in the theorems. Physics is doing the work in my reasons for believing the theorems are about anything at all.
What follows is not a defence of that claim. I invite you for a stroll around the building, one theorem per room. In fact, every time I entered the club with someone who never been there we begin by a slow stroll around nooks and crannies’ of this amazing labyrinth. Fair warning, in the register the night has earned: the further in we go, the stranger it gets.
Chapter 5 — The Tour
Enter the Five Chambers of Finite Exhaustion
Room 1 — One currency
[SCENE: the first room off the main floor — narrow, low ceiling, one strobe.]
I am in the middle of it, in the swell of the crowd, and the question of budget does not concern me. That is what I think, insofar as I am thinking, which is not much. Everything has clicked. The DJ is playing fast, rough techno, so part of the funds goes on prediction — the banal kind, the running guess that keeps a body in sync with a rhythm that does not want to be easy. More goes somewhere better: on relishing the granularity of these wonderfully abstract sounds, whose origin I could not name if you paid me, mounted on nothing but that four-four scaffolding. I am standing inside a rectangle with towers of speakers in the corners. They have a reputation for being the finest on earth in their category, so the money is well spent at least in this regard. I mean in terms of audiophile experience. Some part of attention is being spent, for a while now, on communication with a girl dancing three or four people away. We have been exchanging smiles at uneven intervals for a while, but this a pointless taxation, back then I am unhappily married, so the smiles disappear into the void. An act of beautiful encounter goes to waste. The rest the rhythm has taken outright: emotion and body handed over to that jerked oscillation, spent as fast as it arrives. And then a good friend surfaces beside me, says something directly into my ear, and I cannot understand a single word. Not the volume. I hear the sounds. There is nothing left with which to turn them into language.
Bohr said this first and got called mystical for it: you cannot measure position and momentum both to arbitrary precision, and not because the instruments are crude. In this system it is not an interpretation of physics but a line of arithmetic. Give an observer exactly one tick and two questions. The first question consumes the tick:
And the second, arriving at a budget of fz, returns BUnknown — not “probably,” not “approximately,” but by the same reduction that produced the first answer:```coq
Lemma single_tick_depletes_eq : forall a b,
snd (fst (fin_eq_b3 a b (fs fz))) = fz.
```
```coqTheorem complementarity_eq : forall a b c d,
let bud_after := snd (fst (fin_eq_b3 a b (fs fz))) in
fst (fst (fin_eq_b3 c d bud_after)) = BUnknown.
```
So far this is standard bookkeeping. The part that surprised me when it went through is what happens when the two questions belong to different faculties. The budget is not partitioned by department. It is one currency, and it does not care whether you spend it on comparing, on recognising, on measuring entropy, on collapsing a superposition. Spend it anywhere and you are blind everywhere:
ask an equality, and observer collapse is frozen (eq_then_collapse_blind)
measure entropy, and equality goes dark (entropy_then_eq_blind)
collapse a pattern, and measurement is no longer possible (collapse_then_entropy_blind)
Three modules that share no code, no types, no vocabulary — and they starve each other, because they eat from the same plate. That is the strong form of complementarity, and I do not know how to state it at all in a framework where looking is free. In the classical picture there is nothing to trade off: every faculty is independent because every faculty is unlimited, and the reason a man cannot parse his friend's sentence while tracking a rhythm and a face becomes a fact about psychology, an unfortunate feature of primate hardware. Here it is a fact about arithmetic, and the primate is merely where you happen to notice it.
Einstein’s objection, for the record, was that BUnknown must be BTrue-or-BFalse in disguise — a hidden variable, a fact not yet uncovered. The system answers by construction rather than by argument: BUnknown is a constructor. It is not BTrue, it is not BFalse, and no amount of cleverness converts it into either. Twenty-eight years of that dispute, settled by discriminate.
It is worth remembering which of the two men had the better taste in pictures. Bohr hung a cubist canvas in his house — Metzinger’s woman with a horse — and is said to have used it to explain what he meant. The reason is exactly this room. Representational painting offers a firm contour: one viewpoint, fully funded, everything decided. Cubism spends its budget differently. It shows a face from two incompatible positions at once and refuses to say which is the real one, so perception arrives at a paradox it cannot resolve and is not being asked to. That refusal is not a failure of the picture. It is the picture's subject. Bohr recognised the third value in oil paint decades before anyone could state it in a type.
The floor knew all of it the whole time and needs no theorem. At some point in the night everyone learns that they have to choose: the mix or the room, the friend or the stranger, the body or the thought. Not because they are weak. Because attention is a currency and there is one of it, and at four in the morning the exchange rate is brutal.
Room 2 — Forced to answer
[SCENE: five in the morning, the smoking area; someone explains something to you with total confidence and is completely wrong.]
You already know the diagonal from the queue: a budget of n cannot verify n. The observer's own size is the one measurement it cannot afford. That was Chapter 2 and I will not prove it twice. This room is about what happens next — about what a system does when it is blind and still has to produce an answer.
There is a function in the code for exactly this, and it is three lines long:
```coqDefinition collapse3 (r : Bool3) : bool :=
match r with BTrue => true | _ => false end.
```
It converts the honest three-valued verdict into a two-valued one, and note where BUnknown goes. Not to a separate slot. Not to an error. It goes to false. The system that could not afford to decide is not recorded as undecided; it is recorded as having decided no. Applied to the diagonal, this gives one of the bleakest theorems in the corpus:
```coqTheorem pattern_trauma : forall n,
collapse3 (bool3_of (le_fin_b3 n n n)) = false.
```
An observer that cannot afford self-knowledge is not told “you cannot afford this.” It is told no. That is the mechanism, stated in arithmetic, of every refusal of the Real: the impossible-to-decide is converted into a verdict, and the conversion is invisible from inside, because the output type has no room to record that anything was lost.
Now transpose that to the machines currently writing most of the sentences in the world. A language model’s output type is not Bool3. There is no token for “I ran out of budget before this distinction resolved.” Every answer leaves by the same door, with the same fluency, whether it was reached or manufactured. What we call hallucination is not lying and it is not a bug in the weights. It is collapse3 at the output boundary: a system with a genuine BUnknown inside, forced through a type that only has two values, and the third value — the honest one — mapping quietly onto whichever of the two is easier to say. The fix people usually propose is more knowledge. The theorem says the problem is upstream of knowledge, in the shape of the output.
And the system has a name for the setting that governs this. In the observer module there is a cut — a pair of thresholds carving Bool3 out of a continuous signal — and one comment in the code has stayed with me longer than most of the proofs: the width of the BUnknown band is the observer's honesty. Set the two thresholds far apart and you leave yourself a wide region in which you are permitted not to know. Bring them together and every signal resolves to yes or no. Set high = low + 1 and there is no room for doubt at all. That configuration also has a name in the comment, and it is not "efficient." It is narcissism.
The man in the smoking area is not lying to you. His budget went hours ago, the question deserved a BUnknown, and his output type has two values. He is telling you false with the full confidence of someone who never saw the third option leave.
Room 3 — Death is economic, not logical
[SCENE: an hour later you notice someone is missing, and cannot say when they left.]
Chapter 3 showed how they go: starved, when floor division rounds a dwindling budget below one, or annihilated, when a total mismatch collapses the aperture itself. Two organs, two deaths, both machine-checked, both absorbing. I am not repeating the mechanics. This room is about what kind of fact a death like that is.
Classical Bayesian practice has a commandment: never assign zero prior to anything you might be wrong about. It is a good commandment, and it exists because in that framework zero is an act of infinite confidence — a claim that no evidence whatsoever could ever raise the hypothesis again. Assigning it means closing a door on the world.
Nothing of the kind happens here. Nobody decided that H₁ was impossible. H₁ ran out of money. The distinction is the whole content of this room: in standard probability, zero is a property of the event — it sits in the sigma-algebra with measure nothing. In VOID, zero is a property of the observer — a contour that can no longer pay to distinguish anything. One is a metaphysical verdict. The other is bankruptcy. They look identical on the page and they are not remotely the same fact.
And bankruptcy has a feature that metaphysical exclusion does not: it is local to the run. The Pattern Silence Theorem is absorbing within a population and a signal stream — no sequence of evidence resurrects a contour that has already gone silent. But nothing in it forbids a fresh membrane, tuned to the same position, entering a new run with new budget. Hypotheses die the way organisms die: permanently for the individual, not for the type. The niche stays open. Somebody else can stand there.
Which also dissolves, quietly, the oldest sore point in Bayesian epistemology. Where does the prior come from? What justifies the first number? Whole literatures exist on this — maximum entropy, subjective elicitation, the hope that priors wash out with enough data — and none of the answers fully satisfies. In this system the question does not arise, because the prior is not a belief at all. It is a budget: the resources the hypotheses happened to start with. Nobody chose it in the epistemic sense; it was inherited, allocated, or accidental. You can argue about whether an allocation was fair. You cannot argue about whether it was correct — that category does not apply to material conditions.
So the dancer who left is not refuted. She is out of stamina, on a Sunday, in a building that closes. Next Saturday the floor is full again, and someone is standing more or less where she stood.
Room 4 — Truth does not decay
[SCENE: a quieter hour — someone dances eyes closed to a track they've known for twenty years; body memory whose budget hasn't run out.]
Room 3 was about what runs out. This room is about what doesn't.
Recall that a comparison can come back as BUnknown — not because the answer is mysterious, but because the observer could not afford to reach it. Now ask the natural follow-up: if I come back later with more budget, can the answer I once got flip? Can a richer observer overturn what a poorer one already established?
No. And it is a theorem.
```coqTheorem caretaker_lemma : forall n m b1 b2,
bool3_of (le_fin_b3 n m b1) <> BUnknown ->
leF b1 b2 ->
bool3_of (le_fin_b3 n m b2) = bool3_of (le_fin_b3 n m b1).
```
I named this the Caretaker Lemma, after Leyland Kirby — the musician who records as The Caretaker, whose six-hour work Everywhere at the End of Time is a slow document of memory dissolving under dementia. The piece is often heard as proof that the past decays. The lemma says something more exact, and stranger. The melody on the record did not change. The record is intact. What ran out was the budget to play it. Degradation is not the truth rotting; it is the observer going broke. The thing you knew is still true, still sitting at the value it resolved to. You simply can no longer afford the descent that would let you read it again.
This is the precise statement classical mathematics has no way to make, because in classical mathematics comparison is free. With free comparison there is no difference between "false" and "too poor to check" — both just register as not-true, and the distinction the whole system turns on is invisible. Only once you price the act of knowing does the gap open: a region can be false, or it can be true-but-unaffordable, and these are not the same condition. The first is a fact about the world. The second is a fact about your budget. Conflating them is the cheapest mistake an observer can make, and the only one a finite observer makes constantly.
So the floor at its emptiest hour is not a place where things become untrue. It is a place where things become unaffordable, which feels identical from inside and is not. The dancer with her eyes closed has not forgotten the track. She has stopped paying to verify and is living on what already resolved.
Room 5 — Shape is the condition
[SCENE: the last room of the tour; the light changes colour.]
Three sentences of real history, because the theorems in this room are named after historical facts. In March 1991 a group of people opened a club in the vault of the ruined Wertheim department store on Leipziger Straße — a steel-doored strongroom under the rubble of a bombed shop, in the dead zone the Wall had left behind, in a city that had just acquired more abandoned infrastructure than anyone knew what to do with. They called it Tresor. Detroit came over — Underground Resistance, Jeff Mills, Blake Baxter — and for a few years the most consequential music in Europe was made in a concrete box that had been built to hold other people’s valuables. Music, rhythm, speed, sweat, budget, all mixed symbolically and alchemically in one room, and not one person in it ever asked to be examined this closely, or to end up as raw material for a metaphor machine inside a project as odd as a finite mathematics built with AI.
Everything in this essay so far has depended on one thing that is easy to miss: the observers had to differ. If all three membranes scored identically against every signal, the multiplicative update would preserve their ratios exactly, and nothing would move. That is not a hypothetical. It is the formal boundary of the whole result, and it is machine-checked as a trio.
basic_channel — score zero is death. A membrane whose filter admits nothing scores nothing, and one decay step takes its capacity to fz. No shape, no survival.
birmingham_stagnation — score constant is a freeze. Three membranes with identical centres and identical radii, meeting a signal at their shared centre, each compute floor(budget × radius / radius) and each keep exactly what they had. The machine confirms it: birm_result_budgets = map mem_budget birm_membranes. Nothing learned, nothing lost, forever. This is the replicator equation with uniform fitness — which is to say, no selection at all.
tresor_discrimination — score varies, and the budgets diverge to (6, 32, 1). The posterior appears precisely because the membranes disagreed about what they were hearing.
Read together, they say something that inverts the usual complaint about finite minds. The filter is a restriction: a membrane can only see signals within a certain range, and everything outside is invisible to it. That restriction is not the obstacle to learning. It is the precondition. A contour with no shape dies. A contour so wide that everything matches it equally learns nothing, forever, no matter how much evidence arrives. Only a calibrated, finite aperture produces the differentiated scores that drive convergence at all. Bounded rationality is not a degraded copy of unbounded rationality. Boundedness is the mechanism. The bound is the rationality.
Which is also, and I did not plan this, the operating principle of a vault. Leave it open and the valuables walk out. Weld it shut and nothing can be deposited. Only a calibrated door — finite, closable, with a specific shape — keeps anything at all.
Chapter 6 — The K-Hole (The Improbable)
…And Then Finally the Idea Got Out of Him by Itself, He Just Needed to Make His Mind Turn As Close to the Life-Threatening Emptiness As Possible
I was the last one left standing. My buddies had disappeared. So I thought: "Gung ho!" —then proceeded to do the dumbest thing I could have done at that moment. I took what was left of my budget on being happy that day, an amount I badly underestimated. Then I continued my short stroll of stupidity, joining some random group of people in a packed bathroom stall, where I added — again underestimating the amount, as my vision was already blurry — another source of financing, this time something straight from the anaesthesiologists' ward. There was a merchant in the stall who, upon seeing me, force-fed me a third one, having rightly predicted what was about to happen: the gift, a true one, was simply speed, which held my heart rate together long enough to stand. I have no idea who he was, and no plan had brought me to that stall. Somehow, I made it back to my favourite place on the dancefloor, and then it began. My mind descended into thick tar. I was standing right next to a monumental tower of speakers and the music reached me only as a faint echo. And yet at the very bottom of that pit I found a moment of clarity and began assembling the first concepts of what became a book on probability. Months of research into a subject that was, back then, entirely exotic started coming together — the Bohrs with the Marinettis, the von Neumanns with the Musils. I do not know how long I was down there, but when the first sparks of consciousness came back, I realised I was about to pay for my mistakes. To cut it short: it took me 45 minutes to reach a chair that was 10 meters away, …then I managed to migrate to a dirty couch where I vomited blue foam, and after another pointless stroll — in reality the behaviour of an animal looking for somewhere safe to hide — I lay down on some crates in front of the toilets and stayed there three hours with the music still going. Me trying to listen, or rather pretending to, the stupid behaviour of a student who stares blank at a page with nothing left to spend and a cancerous super-ego forcing him to force-feed himself letters that never make it as far as sentences. Yes. Three hours on crates outside the toilets, following a set, with the attitude of an audiophile.
It had to be a serotonin syndrome, I thought to myself. Oh well. The moron, meaning me, after those three hours still found some budget: enough to get back into a stall, sit down on the floor, take what was left of his drugs, crush them, look up at the dim lights, and arrive at the conclusion that this low he had never fallen, and that it felt glorious. I took the mix of god-knows-what and went to gather my clothes, which turned into a long chaotic struggle conducted by a brain so scrambled that, in all honesty, it was barely present at the scene.
That is the whole of it. Now watch it pay out, because this chapter is load-bearing, not confessional. The night I nearly did not survive is the cleanest demonstration in the essay of theorems you have already met. It cashes into them, in order.
The descent was the measurement ladder. The system has a four-level type for what a measurement is, and the levels are not degrees of the same answer – they are different kinds of knowing, set by how much budget the observer can spend:
```coqMSharp(p) — a definite reading (needs budget ≥ 3; sharp_requires_3)
MFuzzy(lo,c,hi) — an interval estimate (budget 2)
MVague(lo,hi) — a wide interval (budget 1)
MVoid — unmeasured (budget 0)
```
The k-hole is this ladder, lived, in reverse. I did not approach zero. I descended through kinds: from sharp edges to fuzzy ones, to a vague smear, to the floor of resolution where nothing could be told apart from anything else. decay_terminates proves the metaprobability collapse bottoms out in exactly four steps. I have a name for each rung now. That night I went down all four and stopped at the last.
The stranger was MVoid, not P = 0. My model of the night contained no entry for a random man in a toilet handing you the amphetamine that keeps your heart coherent. He turned out to be one of the hosts that night. On duty in the obvious sense, and on a second duty as well, the one nobody rosters, and it is possible that I owe him my life.
And the tar I went down into, where the book found its beginning, was the productive void. void_productive, emergence_from_conservation: the collapse is not the end of the answer, it is the condition for it.
“Measured and found impossible” (MSharp(0)) and “never measured” (MVoid) are different types, not different numbers. When a climate model reports P = 0 for a tipping point it never simulated, or a risk model assigns zero to a scenario it never ran, they are reporting MVoid as if it were MSharp(0) — mistaking the unpriced for the impossible. The classical framework has no room for the distinction; ℕ-built measure theory folds them together. The proof that they are not the same is, in the end, a body: I am the witness that the unmeasured is not the impossible, because I am alive to type this sentence, and the night’s model said nothing about the man who made that possible. Thank you, you can imagine how grateful I am, for what you have done. You are a good human being, hope to meet you some day, somehow. ```coqTheorem void_is_not_zero : forall denom, MVoid <> MSharp (fz, denom).
Closed systems die; I was open. I took the line he gave me from his phone. Unhygienic, parents would be so angry and disappointed. This is a theorem:
```coqTheorem closed_system_dies : forall b, closed_run b b = fz.
A membrane with finite budget and no intake reaches fz — always, no exceptions. On its own reserves, every finite observer is already dead; it is only a question of how many ticks. Living systems get around this not by having more budget but by being thermodynamically open — operationally closed, but taking budget in from collisions with other contours. In the membrane layer there is no external source of fuel anymore; every encounter is two membranes colliding, and intake is the transfer. The stranger’s speed was an intake event. I survived the night the way every membrane survives anything in this system: not on what I had, but on what crossed into me from another contour.
And then the three hours on the floor were not lost time. They are also a theorem:
```coqTheorem recovery_preserves_trajectory : forall obs n b,
let '(obs', _, _) := recovery_sequence obs n b in
obs_trajectory obs' = obs_trajectory obs.
```
recovery_step is the observer that stops observing: no new distinctions, trajectory unchanged, Spuren emission dropped to the bare cost of existing. Recovery is not the budget coming back — it is the rate of loss falling to its floor. Lying still in front of the toilets with the music going was the system doing the one provable thing that slows the bleed. Half a sober hour and three wrecked ones are the same theorem.
And the pool of tar where I descended for the book could find its symbolic beginning - that was the productive void. void_productive, emergence_from_conservation: the collapse is not the end of the answer, it is the condition for it. At the bottom of the ladder, with resolution gone, the next distinction is always exactly one tick away. I did not start the book despite the descent. I started it at the bottom of it, which is the only place the system says emergence can happen — in the gap conservation leaves behind.
This chapter had to come after the tour, because it needs the tour’s vocabulary. By now MVoid and intake are not jargon; they are doing real work in a true story. That is the point where the two registers – the Qed and the body – stop running in parallel and fuse for good. The mathematics did not illustrate the night. The night was the mathematics, run once, at full cost, on the only substrate I had.
[SCENE: transition to Dawn — light starts to come in, first time in the essay; cut.]
Chapter 7 — Dawn (What This Is and Isn't) [U8]
The Sad Beckettian Character, Exactly at 6 A.M., Ankle Twisted As It Turned Out, And No Budget Whatsoever, He Slowly Started Limping. Richtung: OSTBAHNHOF | RATHAUS NEUKÖLLN (“Zurück Bleiben Bitte!”)
[SCENE: first light through the high windows of the former power plant; sharp, unforgiving. One short sentence — dawn is what the vault excluded: the platform clock gets its voice back.]
One thing the substrate predicts and the floor confirms every Sunday morning, before we get to the accounting. Randomness here is a resource with units, and when the units run low the outputs do not dissolve into noise. They start following their own history: an unpaid correlation debt accumulates, and the next value leans on the last one. Exhausted improvisation does not become chaos. It becomes a loop. That is what the final hour of a long set sounds like from the inside, and it is also, for anyone who wants the machine-learning gloss, what mode collapse is.
Let me be exact about the perimeter, because precision here is what separates a claim from a manifesto. The replicator–Bayes correspondence is not mine — Harper, Shalizi, and Campbell established it in continuous mathematics, and I have only shown it survives the fall onto a finite floor. Against the nearest neighbor on this side: logical induction buys its guarantees with an infinite market of traders converging in the limit, and trades away exactly what VOID keeps — death, silence, and affordability, the three things that only exist before the limit. And the deepest structural payoff is one this essay only gestured at: the external observer, the view from nowhere that classical inference quietly assumes, is unconstructable here by budget arithmetic alone — the Cartesian cut that embedded-agency work treats as a desideratum points in that direction here without yet arriving. What the system actually proves is narrower: no_complete_self_model, that no observer can build a complete model of itself within its own budget, and self_blind, that its own size is precisely the measurement it cannot afford. Both lean toward the conclusion. Neither delivers it, and I mark this as the direction I would look next rather than as a result in hand. That is the ambition's real reach.
Now the debts, named so nobody has to find them in the comments. The convergence is a computational result on a small fixture — three membranes, five signals — not yet a general theorem; the drift bound is proven on paper, not yet ported to Coq; the system rests on six explicit axioms, all named, none about inference. None of this is hidden, because the whole point of the substrate is that nothing can be. And that is also the standing challenge: every number in this essay reproduces under vm_compute — the trajectories are theorems, not screenshots. If you think the floor cheats, compile it. If you can Dutch-book a membrane, the repository is open. The one thing I will not give you back is the infinity I spent the whole night refusing.
Chapter 8 — Monday (Coda)
Serendipity... he lives...he keeps on living. 🕳️⬇🌚
[SCENE: the floor emptied; full daylight, merciless on tired faces of those who are slowly leaving, probably to share the comedown together. The last track has no drop — it just fades. I walk alone, slowly piecing together what has just happened and what the hell did I come up with. I sounds coherent, a sigh of relief. The leg hurts more than I expected and ketamine now wears off after 15 minutes. Oh, I am so fucked…]
The door closes soon after. Of the three who started equal, one is gone — not faded to a small number, not approaching zero in some limit: gone, fz, and no later beat will bring her back. The other two carry the night's whole remaining budget between them, in a proportion nobody on the floor ever computed and everybody enacted. On the dirty floor of the stall there is what’s left of the night, scraped together; on the way home a cheap spinach börek forced down against the nausea — the membrane, finally, doing its own intake — and then the cold, cold morning, the one clock that never stopped. And the night has just become a finite object. You will get to call it back a few times: in this system a memory carries a small countable number of replays, and each recall degrades the copy in proportion to what recalling it has already cost. The ones you reach for most often evaporate first. Which means the version of tonight you will still have in a year is not tonight. It is the residue of the times you asked for it. What you keep is the posterior; what you spent is the time; and the two together are exactly what you walked in with. Conservation holds, even here. Especially here.
In the 90s this would be completely normal as anyone could and did attend rave parties. I am not bragging. The CCRU collective, the anomaly that broke the university and was broken by university in return, is a great example. Recently, along with AI revolution CCRU sparked a renewed wave of interest, at the same time among the weirdest factions of AI critics and enthusiasts. Their work is worth looking into, though I won't attempt it here, since no few sentences could encapsulate a project that fused witchcraft with cybernetics, amphetamines with number theory, and jungle techno with academic philosophy: the kind of thing that could only exist at great intensity, and only briefly, before imploding. Clark and – as I assume – many other serious academics were there, sweating their asses off to the defening sound coming from shitty quality soundsystems, finding last places of respite in the greyish, drab capitalist reality of , cynical and culturally becoming increasingly impoverished, squeezing the last drops of creative potential from the post-industrial remnants of reality.
UNOFFIZIELLE UNTERTITEL
A Mysterious Man Dressed in Rubber Uniform And A Gas Mask,
Hiding in a Hole in the Wall, Stares at the Passers-by…
(A True And Perplexing Sight: A Man, Always Silent, Probably Migrating From Lab.oratory, Berghain’s Infamous Fetish Bar Buried in the Deep Cellars of the Building, As a Part of His Mating Ritual)