No single ingredient is new.
Their composition is.
Take the strongest form of the doubt first, because it is the honest place to begin. Every piece of what we built was made by someone else, and made long ago. The algebra of observables is more than half a century old. Machine-checked physics is a real and growing craft. The conviction that health lives in coordination and not in any single level is the working premise of an entire living field. A formal ontology of medicine exists, carries a name, and is in daily use. Set our work beside any one of these and it can seem to disappear into the older thing. The novelty, we think, lives in the composition — a single object that holds all of them at once, around one center they were never built to share: a definition of health, proved outward from a primitive into the observable physics of the boundary, and run against the measured surface of a living body. As far as we have been able to find, nothing else stands in that place. What follows is a map of the nearest occupied places, drawn as fairly as we can draw it, because the people most able to test the claim are the ones who built the country next door.
The phrase itself belongs to physics. Rudolf Haag and Daniel Kastler set it down in 1964: to every region of spacetime, assign the algebra of the observables one could measure inside it, and let the whole theory be the net of those algebras and the maps between them. It is one of the most powerful abstractions the twentieth century produced, the backbone of the algebraic account of quantum fields, and it has carried physics for sixty years. Its observables are the observables of a quantum field, organized around locality and causality, indifferent to whether anything is alive. It answers to no body. We take from it the oldest instinct in the subject — observables first, gathered into an algebra — and carry that instinct into a country it was never pointed toward.
Nor is it new to hand physics to a proof assistant and have the machine check the proof. Mike Stannett and István Németi verified first-order relativity in Isabelle in 2014; special relativity has been formalized in Coq; and in the last few years the Lean library has taken on Schwarzschild curvature and the thermodynamics of chemistry, the kernel confirming each derivation line by line. This is real work, and it shares our tools. Almost all of it formalizes a theory already established, and does so to ask a mathematician's question about the theory — whether its axioms are consistent, whether a famous derivation truly holds, whether one assumption leans secretly on another. It is formalization turned back on mathematics, to study it. Ours is turned outward, onto a measurement — a system that takes in a real capture and hands back a state, the proofs standing guarantee over the computation that made it. The recent Lean work on general relativity names the very wall we had to climb, the long gap between tensor calculus written by hand and tensor calculus a machine will certify, and we climbed it at the size of a working library.
The nearest neighbor is a field, and we name it plainly, because pretending otherwise would fool no one who works in it. Over the last fifteen years Plamen Ivanov and the network physiologists have taken the body as a web of coupled systems — heart and lungs and brain and muscle and the metabolic tides beneath them — and read health and disease from the coherence and the timing and the coupling that runs between them, watching the whole organism hold together while its parts keep step and come apart when the coupling fails, in sepsis, in coma, in the slow uncouplings of chronic disease. That is our own conviction, reached by others, from another direction, and its being a real and serious field is the best evidence we have that we are aimed at something that is there. Network physiology reads the coordination from the outside; it measures the coupling and sets it against the clinical record, an empirical science of correlation, sure-footed and growing. We begin somewhere else — at a definition of health written down first, built outward step by step, the kernel checking each step as it is laid. The field watches the body keep time. We wrote down what keeping time means and proved the consequences.
The word we use in public, ontology, already has an exact and separate life in medicine. On the Basic Formal Ontology sits the Ontology for General Medical Science, a formal, logic-coded theory of the entities of a clinical encounter — disease, disorder, diagnosis, patient — written in description logic and used to give structure to the great terminologies like SNOMED. A formal ontology of medicine exists, and honesty requires us to say precisely how ours differs. Those ontologies classify; they fix the names and the logical relations among categories so that facts can be recorded and machines can reason over them. Ours computes; it takes physical observables and returns a state, and proves how that state moves. And there is a detail in the older ontology worth stopping on, because it says the thing this whole note keeps circling: the most developed formal ontology in medicine is a theory of disease. Even here, in the most rigorous corner of the field, the thing that got written down was illness. Health was left undefined.
There is real mathematics of the healthy steady state as well, the neighbor closest to our own method. Martin Golubitsky and Ian Stewart built a dynamical-systems account of homeostasis, in which holding a variable steady against a changing input is a precise and provable property of a network; control theory frames the same holding as a feedback loop keeping a quantity inside a band. This is the family our primitive was born into — staying inside a band, under disturbance, is much of what it formalizes. That work lives where it began, a study of the phenomenon itself, proven by hand, at home in the abstract. Ours carries the same band-holding idea up through a kernel that certifies it, outward into physical observables, and into an instrument laid against a body. And the homeostasis literature confesses openly what medicine's ontology showed in silence — that a precise definition of its own subject has stayed out of reach. We took the confession as the assignment.
Two things fall out of the map, and both are worth saying straight. The absence we began from — medicine's long habit of defining disease and leaving health unwritten — stands in plain view inside the field's most rigorous work, in the ontology that formalized illness and the mathematics that could not pin the healthy state down. We found the gap already there. And the intuition beneath everything we built, that health is coordination, belongs to a whole field standing beside us. We are glad to stand in company there. It suggests the target is real, and the thing we carried to it was the form.
Which raises the fair question of why, if every piece was lying about in the open, no one set them together before now. Two things had to arrive in the same moment, and never had. The tools had to cross a line: a proof assistant carrying a mathematical library deep enough to bear applied analysis — the measure theory and functional analysis and linear algebra a physical algebra leans on — reached that depth only in the last few years, and machine-checking a whole working library of applied mathematics, in place of one admired theorem, was out of reach before it. The continuous measurement of a body from hardware already worn on the wrist, and the compute to read it, are newer still. And the knowledge had to gather into very few hands: to try this at all, one person must be at home at once in formal methods, in the mathematics of observable physics, in signal processing, in physiology, and in the old unanswered question of what health is, and then carry the single idea of setting a definition of health at the center of all of it. That gathering is rare, and it had to meet the tools while they were ready. The pieces waited a long time in plain sight for a moment that had not yet come.
Beneath the accounting there is a stranger thing, and it is the part we find genuinely new. A scientific object is usually one kind of thing — a theory, or a model, or a dataset, or an instrument — and lives its whole life as that one kind. This one refuses to settle. It is a definition and a proof and an instrument at the same time, and it is alive, calibrating to the body in front of it and shifting as the science shifts beneath it. That refusal is why the public word for it is ontology and the working word is algebra. An ontology says what there is and how it holds together; the algebra is the engine that runs inside it. To call it a proof-checked algebra of observables names the machinery. To call it a formal ontology of health names the whole, and the whole is a kind of object we have not found standing in the world before.
One boundary holds over all of it, and we draw it in the open. None of this says the definition is true of biology. The proofs reach the properties of the definition and its mathematics — that it holds together, that it settles, that it stays inside its bounds, that it accounts for every state and conserves what it should and keeps its shape across scale. Whether it tracks the health of a living body is a separate question, and an empirical one, still open, still being asked against real captures, and nothing on this page answers it. A thing can be the first of its kind and still be pointed at nothing. We have reason to believe this one is pointed well. The bodies will settle it, and we will say so when they have, and not before.
A companion note, A boundary-observable certification algebra, describes what kind of object this is and how it was built. The instrument carries the same signature — an old and proven way of reading a hidden interior from its boundary, brought to a living surface it had not reached, made admissible by a bespoke algebra — described in Reading the living boundary. On what it does and does not prove, and the empirical work underway, see the science.