Principia
Every bridge that stands, every battery that holds its charge, every signal that crosses an ocean obeys a structure older than all of them: conservation, symmetry, the arithmetic of what can and cannot happen. For twenty-five centuries people have asked where that structure comes from. For two, engineers have learned to work inside it. The two efforts rarely met in a form anyone could check.
The Institute exists to make them meet. We are learning the language the universe is written in, and the bridge from that language to the world is category theory, the mathematics of what composes. Written as polygraphs, its laws become local rewrite rules; fired in any order, those rules are a parallel machine that gives one answer on any hardware; and a proof checker verifies every step. Mathematics that lived only on paper becomes something that runs, measures and acts, carrying proof of what it guarantees. This page walks the road: the language, the bridge, what it buys, the fields it reaches, and where it leads.
We treat mathematical structure as the foundation of physical computation and control. We find the mathematics intrinsic to a problem, realise it in the hardware that embodies it best, across digital, analog and neuromorphic matter, and let machine-checked proofs, calibrated models and runtime constraints establish what each realisation can guarantee.
The mission · the Institute for Applied Ontological Mathematics
Watch it computeHow category theory and polygraphs become a parallel machine, live in your browser, with the ten papers behind it.Mathematics that runs →
Provable Matter · the evidence lens
Drag to explore a shape made of points, then reveal the questions a future result could carry: its observations, assumptions and supporting evidence. A concept, not a readout.
Part I
A single distinction, and the logic it settles into.
01 · The question
Nothing interacting with itself is the basis of reality.
Richard Goodman, the Institute’s founding thesis
Most theories begin with a stock of things already given: particles, fields, a stage of space and time. We ask what can be built if nothing is given in advance. Stated that strongly, the thesis needs care, because “Nothing” can mean three different things, and an argument that slides between them proves nothing.
We use the word for the problem of beginning without an inventory, and our formal work begins from explicit generative assumptions, kept in view. No primordial observer is needed: re-entry is a construction referring back into its own domain, and observers can be studied later, as systems that sense, remember and act.
meaning i
No objects, properties, operations, laws, or possibility of action. To say that such absence interacts already raises a real philosophical question, and we treat it as one.
meaning ii
A primitive role inside a calculus of distinctions, as in Spencer-Brown's Laws of Form. It can be written down, and once written it belongs to a mathematical setting with rules.
meaning iii
An explicit syntax with very few generators and rules. It is a precise object to study, but small is not the same as assumption-free, and we keep the assumptions in view.
We call the foundation a generative distinction ontology; its working philosophical label is Constructive Ontic Structural Realism. With ontic structural realism it gives priority to relations; with Tegmark’s Mathematical Universe Hypothesis it takes the mathematical character of reality seriously; it adds the question of which generative operations produce the structure, and which features of the world that structure decides rather than merely describes.
| What is explanatorily primary? | Distinction, interaction, and admissible transformation. |
|---|---|
| What are mathematical structures? | Articulations of the organisation those operations generate or support. |
| What makes an object identifiable? | Relations, invariants, history, and persistence at a stated scale. |
| What is possibility? | A structured domain of admissible configurations, constructions, or histories. |
| What is compossibility? | Joint compatibility under a declared context and set of constraints. |
| What makes knowledge constructive? | A witness, construction, or explicit transformation that establishes the claim. |
| What makes a construction physical? | An interpretation, and an experimentally supported relation of realisation. |
| What makes the work useful? | Transfer that preserves what a scientific or engineering purpose needs. |
02 · The first distinction
Draw a line around something, and a difference exists where none did: inside and outside. In 1969 George Spencer-Brown built a whole calculus on that single act. Its deepest move is re-entry: letting the mark refer to itself, so that the form contains an image of its own drawing.
Even before re-entry, one mark already does arithmetic. Give each of N cells a mark that can be undone, +1 or −1, add them, and average the square of the total over every possible assignment. Every cross term cancels, and the result is exactly N, for every N, in every number system where the sum makes sense.
Read the same cells as 0 and 1 instead and the cancellation disappears. The quiet is not in the mark; it is in a reading that respects the undoing. Before the 1998 discovery of cosmic acceleration, Rafael Sorkin used this arithmetic to predict the scale of the cosmological constant.
The identity decides the size of a fluctuation: a form. It does not decide which sign each cell carries: a choice. And under a model linking cells to spacetime, the size depends on how many cells there are: a history. Form, choice and history are the three threads that run through everything below.
03 · Re-entry
When a mark re-enters itself and settles, the settling is a precise mathematical object: a nucleus, an operation that only ever adds, is content once applied twice, and respects “and”. Its stable points form a new, complete logic. In our formal work the simplest such operator is double negation, j = ¬¬: “not not”.
The chain below is the spine of the whole program, from nothing to a world with two poles. In our Lean 4 formalisation each arrow is a machine-checked theorem, and the load-bearing one is proved without the axiom of choice. What was a sequence of philosophical postulates becomes a sequence of checked steps.
Logic
Ordinary logic refuses to turn “it is not the case that nothing is there” into “here it is”. On the right structure the re-entry operator does exactly that, constructively and without the axiom of choice: what merely subsists is forced into existence.
Geometry
Re-entry acts like turning a Möbius band over: one twist, and inside becomes outside. Do it twice and you are home.
Dynamics
Feed the operator its own output and it settles. The settled value carries the golden ratio, the number that reproduces itself under its own rule, φ² = φ + 1.
Computation
On a machine, the same operator is the swap of the two wires of an active pair in an interaction net: one reduction step of the kind our Boundary engine performs. The ontology does not only describe; it runs.
These are one operator seen four ways, not four analogies. Replace it by a nearby operator and the downstream work measurably breaks: the identity makes the forcing a tautology, and the constant map erases every distinction at once. A three-element example shows why care matters: close 0 < a < 1 by sending 0 to a, and the new logic’s least element is a. The symbol for “least” does not automatically name Nothing.
Part II
How category theory and rewriting turn abstract mathematics into machines.
04 · Mathematics that runs
This is the bridge. Category theory is the mathematics of what composes: when two steps can be joined, and what survives the joining. A polygraph writes those laws down as small local rules, each rewriting one pair of agents. And local rules, fired in any order, are a parallel machine whose answer cannot depend on the order, or on the hardware it runs on.
That is how mathematics that once lived only on paper begins to run. Our kernel has four agents and five rules, with the logic of a distinction from Part I built into them. Below it runs for real: there are 360 ways to run this net, and every one ends in the same place.
The full story: how a law becomes a machine →the lab, the race it caught, proofs that run, any hardware, and ten papers
05 · The mathematics underneath
A bridge from theory to the world must carry its guarantees across every joint: a result proved about one step has to survive being composed with the next, translated to another instrument, and run on another substrate. Category theory is the mathematics of exactly that, which is why it sits under everything here, from a rewrite rule to a network of sensors.
Four ideas carry the weight: sheaves glue local readings into a global truth, institutions keep a reading’s meaning faithful across a change of instrument, constructive proof in Agda turns trust into a checkable artifact, and lenses let a guarantee travel along the chain of transforms.
sheaves · gluing
A sensor network is a sheaf: each node is a local section over its patch of space and time; where patches overlap — two instruments in the same air — the readings must agree; consistent locals glue into one coherent field. Drift and disagreement are then a gluing obstruction, a cocycle, and calibration against a reference restores the overlap-compatibility that makes the sections glue.
institutions
The theory of institutions formalises faithful translation between measurement systems: a change of instrument, unit or installation is a signature morphism, and a satisfaction condition keeps a reading's meaning invariant under it. That is exactly a measurement contract that stays true as it moves across the station's equipment, assets and configurations.
constructive proof · Agda
The contracts are written in Agda under its --safe discipline, with an explicit trust footprint, and compiled to an executable through MAlonzo. Trustworthiness becomes a checkable artifact rather than a claim — open, reviewable and reproducible, which is why this work is also an invitation to the applied-category-theory and formal-methods communities.
lenses · optics
Calibration maps, unit conversions and coordinate changes are bidirectional transforms — lenses — that compose. Treating them categorically is what lets a guarantee about one step travel to the next, so the whole chain from raw count to physical value stays, in one piece, something an auditor can check.
06 · The Ontological Compiler
Describe a process as mathematics. The compiler searches the many equivalent forms of that mathematics, chooses the hardware that embodies it best, and proves how faithfully the result behaves.
01 · specify
𝒯 = (X, U, Y, F, O, 𝓘, Θ)
states, admissible controls, observables, dynamics, observations, invariants and uncertainty
02 · rewrite
one function, many forms, joined by proved rewriting rules; interaction nets and polygraphic rewriting are the intermediate language. See it run ↑
03 · choose
minH, Rλ₁EH + λ₂LH+ λ₃εH + λ₄CH
energy, latency, error and verification cost, weighted by the application. Safety is never a weight: it is a hard constraint the optimiser cannot trade away.
04 · realise & prove
decodeH ∘ RH ∘ encodeH≈εH F
zero error for exact digital work, calibrated and stated for analog; for a learned model, how well it was implemented is kept apart from how well it predicts
The power is in the search: each equivalent form costs differently on each substrate, and every choice the compiler makes carries its refinement evidence.
The first family
In a port-Hamiltonian system, stored energy can rise no faster than the power supplied. No model learned that; it follows from the structure. The same mathematics describes a turbine’s rotation, a battery’s charge, a failing bearing and an analog filter, so wind, solar, analog computing and machine monitoring become one formal framework, controlled by the restrictions their physics already imposes.
Already in the record
Solar, with Morningstar. A safe Agda supervisor, extracted to native code, whose proved reserve floor means no admitted task may spend energy the system does not have: a supervisor cannot manufacture energy.
Distributed wind. An independent checker that admits a curtailment, export or reserve decision only when it respects the turbine’s proved power envelope and storage limits.
Neither is yet the compiler. Both are evidence that its method works on real systems.
The open question we pursue: when does a composition keep its guarantees after it is realised across different physical substrates? Our compositional method: Where the Parts Make a Whole and What Meaning Can Copy (IAOM, 2026). Port-Hamiltonian theory: A. van der Schaft and D. Jeltsema, Port-Hamiltonian Systems Theory (2014).
07 · Matter already does mathematics
A capacitor network integrates. A transistor array counts. A spiking circuit fires when evidence accumulates. Each is mathematics carried out by physics, and no two carry out the same mathematics equally well. Ordinary computing ignores this: it forces every problem into one software representation and asks one kind of chip to execute it.
We ask the reverse question: which mathematical operations does each kind of matter embody most faithfully, and at what cost? We study nine kinds, five of them running in our own work today: not as nine computers but as nine physical interpretations of mathematics, held to account by one formal layer.
proposition I
Matter does not respond to arbitrary instructions. Conservation laws, symmetries, differential equations and thermodynamic inequalities constrain what it can do. Whether those relations are prior to matter is a philosophical question; their practical force can be measured.
proposition II
A transistor array, a capacitor network, a neuromorphic circuit and a GPU do not carry out the same mathematics equally well. The best realisation of a system may depend as much on its structure as on its conventional complexity.
proposition III
Identify a system’s dynamics, invariants, observable states and admissible controls accurately, and it can be governed better. Noise, observability and physical law still set limits; better mathematics makes the limits explicit and lets us work closer to them.
A machine that preserves the mathematical structure of what it controls can be measurably more efficient, reliable, predictable and safe than one that ignores it.
The central hypothesis · falsifiable, and built to be tested
CPU Central processors
λ · reference
control flow and recursion · symbolic algebra · exact, arbitrary-precision arithmetic
active
GPU Graphics processors
∑ · explore
tensor and linear algebra · optimisation · high-dimensional simulation
active
TPU Tensor processors
⊗ · scale
dense matrix products · convolution · low-precision linear maps
seeking partners
NPU Neuromorphic processors
δ · recognise
sparse event streams · low-bit integer inference · temporal pattern recognition
active
FPGA Reconfigurable logic
⊕ · execute & witness
finite-state dynamics · exact fixed-point and finite-field algebra · interaction-net rewriting in hardware
active
FPAA Programmable analog arrays
∫ · embody
transfer functions · filtering and integration · continuous dynamics
active
QPU Quantum processors
ψ · certify, then run
unitary and tensor-category structure · exact cyclotomic arithmetic · error-correcting codes
building
PIC Photonic processors
φ · transform
unitary matrices as interferometer meshes · Fourier optics · linear transforms in constant time
building
MCU Embedded controllers
τ · act
hybrid automata · guarded transitions · fixed-point control laws
building
⊢ The formal layer
hold authority
Proof kernels, safe Agda and Lean: not a chip, but where every realisation is measured and every permission decided.
Each in full, with the devices we use, its part in the compiler and its honest bound: the substrate atlas →
The aim is not to make every chip execute every operation. It is to discover which operations each one can embody most faithfully, and that difference could lead to a new kind of heterogeneous computing. The physical end of the arc is set out under Provable Matter ↓
08 · Provable Matter
Math → Program → Physics. A theorem is abstract; a sensor, an FPGA, a power controller are not. This is where the Institute’s mathematics is compiled to running programs and executed on real hardware, then measured and checked there. One idea connects it all: a result should be checkable at every layer it passes through, with a receipt kept at each step.
At the far end sits a boundary the Institute insists on. Each result is tied to its units, calibration, transformations and proof, so a system can accept a supported claim, preserve an unverified one, or refuse an unsupported one, with its conditions always visible.
step i
A result is written in a proof assistant (Agda, under its --safe discipline, or Lean) with an explicit trust footprint, so the claim is settled for all inputs, not sampled by tests.
step ii
The proof is a program: compiled through MAlonzo to Haskell, or lowered to an interaction net our Boundary engine reduces. The code inherits the proof; nobody re-types the logic by hand.
step iii
The program runs on real hardware — a GPU, a programmable-logic board, a sensor, a power controller — and the physical result is measured and checked back against the specification.
⊢ accept
a precisely supported claim, with its conditions recorded
▬ preserve
an unverified result, marked as such and never promoted
✕ refuse
an unsupported claim, rather than report a number it cannot stand behind
A proof establishes a result under its assumptions; an experiment decides whether those assumptions describe the world well enough for the purpose. Neither replaces the other, and the line between them is kept explicit.
Part III
Trust that can be checked at every layer, by anyone.
10 · Four kinds of evidence
A proof is not a measurement, and a measurement is not a proof. The credibility of the whole program rests on keeping four kinds of evidence apart, then composing them under conditions that are written down.
| Evidence | What it can establish | How |
|---|---|---|
| Mathematical | A transformation preserves an invariant under stated assumptions. | machine-checked proof |
| Compiler | An implementation refines its Agda specification, for a defined subset. | machine-checked refinement |
| Numerical | Fixed-point or analog error stays within a characterised bound. | interval bounds + calibration |
| Physical | Measured behaviour agrees with the model within a validated operating region. | experiment + stated uncertainty |
Implementation error, model discrepancy and measurement uncertainty, added under a common metric. If the total fits inside the certified safety margin, the action is admitted. If it does not, the system abstains or takes an independently justified safe response.
These are guarantees with their conditions attached, never a claim that software proof removes physical uncertainty. The first two kinds can be machine-checked; the third joins formal bounds to calibration; the fourth needs experiment. Saying which is which is what makes the rest believable.
11 · Proofs that run, and superintelligence
In a constructive reading, a proof that something exists hands you the thing. In suitable typed languages (the Curry–Howard correspondence) a proof is a program. We write the emergence chain in our own Generative Void Type Theory, GVTT, so that each construction is at once a statement, its proof and its program, and those programs run: on ordinary processors through our Boundary engine, and on programmable logic boards.
This is what makes a partnership with superintelligence workable. An intelligence that produces mathematics faster than people can review it is only useful if its results can be checked without trusting it. A certificate does exactly that: it turns “trust the producer” into a small check anyone can run. The scope still matters: a checked proof certifies its statement, a compiled program needs its own receipt, and a physical claim needs measurement.
A machine intelligence computed; an independent certificate, whose own soundness is a theorem, made the result checkable by anyone, trusting none of the producer’s work. What is not claimed: a recomputation of the amplitude itself. This is the pattern we are building for every field: superintelligence proposes, certificates decide, people understand. The nine-loop certificate ↗ · Proof-carrying quantum labs →
12 · Where it ends
The finished compiler takes the mathematics of a problem, finds every equivalent form of it, gives each form to the kind of matter that embodies it best, proves what each part guarantees, and lets nothing act until a proof permits it. One description in; a machine made of many kinds of matter out, with its certificate.
Energy. A grid controller written once as the physics of the grid: analog where the currents are, exact logic at the breaker, learning to forecast, and a proof before every switch.
i
Each part of a problem runs on the matter that already obeys its mathematics: less energy, faster answers, less waste.
ii
Learned systems propose freely and a proof decides what acts, so autonomy can grow without losing the right to say no.
iii
Every result carries its certificate, so people, institutions and future intelligences can build on it without checking it again: how a civilisation that means to reach the stars should keep what it learns.
13 · Research technical report
A 3D-reconstruction case study, four analytical propositions and a research framework connecting measurement assumptions, checked computation and downstream acceptance.
Richard Goodman and Stephanie Goodman · The Institute for Applied Ontological Mathematics. 2 November 2026 · research technical report · 23 pages · 31 references. Prepared for author review and publication adaptation; no journal acceptance or peer review is claimed.
measurement meaning · explicit assumptions · computational guarantees
A software proof of concept, with the status and scope of every result stated, and the road from software validation to field measurement laid out step by step.
Part IV
One method carried into every field, physics the deepest test.
14 · The fields
We think about every field the same way. Find the structure it already obeys; write that structure in the language; let the bridge carry it into matter; and keep the evidence at every step. A field is never a new foundation, only a new place to read the same one, so what is learned in one transfers to the next.
These are the fields on our Programs page, each with the mathematics we read it through and where it stands today. Fundamental physics is one of them, and the deepest test of all: whether the language explains the universe itself. It follows.
15 · Fundamental physics
The deepest test of the language is the universe itself. The forces of nature sit on a ladder of numbers. Complex numbers carry the symmetry of electromagnetism; quaternions carry SU(2), the weak force and the quantum geometry of loop quantum gravity; octonions carry SU(3), the colour of the strong force. Past the octonions the ladder ends. That reading of the Standard Model is established physics; what is ours is the proof on each rung.
What is new is the way the rungs are climbed. We start from a distinction rather than assume a spacetime or a symmetry group. One certified engine runs every rung, so the gauge group is a dial, not new unverified software. And every step carries its real status: proved, on the record awaiting landing, or open. Loop quantum gravity, group field theory and QCD stop being three separate subjects and become three rungs of one checked construction.
U(1)
Unit complex numbers form the symmetry of light and charge. Their Hopf fibration fills a sphere with circles that link every other circle exactly once: the geometry of a single magnetic charge.
SU(2)
Unit quaternions form SU(2), the group of loop quantum gravity, in which space itself is a network of quantised areas and volumes. Group field theory makes those networks the excitations of a field that can condense into a geometry.
SU(3) ⊂ G₂
Fix one imaginary direction in the octonions and the other six pair into three complex directions: three colours. The symmetry that keeps that direction fixed is SU(3), the colour group of quantum chromodynamics.
beyond 𝕆
Double the octonions once more and division fails: two non-zero numbers can multiply to zero. Adams proved in 1960 that no further fibration of this kind exists. The ladder has exactly three rungs.
The full ladder, with the papers behind each rung and a gauge theory you can solve in your browser, is published by Apoth3osis, which licenses its software to the Institute: The Ladder of Forces ↗
16 · What a distinction decides
A ladder of proofs is not yet a test. So we tested the idea itself against measured physics across gravity, black holes, dark energy, dark matter, quantum theory, particles and the electron: that the only primitive is a distinction, and that what an observer sees is the stable structure re-entry produces.
Each target’s strongest admissible status was committed before its proofs, and a checker computes each status from evidence bound by hash, so a fit can never be promoted to a theorem. The theorems were then attacked with planted false variants, hostile parameters and independent audit.
The three threads of the coin returned at the scale of physics. No theorem row supplies a free continuous constant: every proved row decides a sign, an exponent, a group, a bound, a rank or an identity. The edges are alternatives the axioms leave open. And magnitudes are counts of history: attacking that class showed the matter–antimatter asymmetry is not a sum of independent local signs (one per particle misses by 10³⁵), while the spectral tilt is a second history count of a different kind, ns − 1 ≈ −2/N.
The root thesis, “physics is the fixed-point theory of distinction”, is scored, not proved. Each row certifies mathematics under a stated modelling premise. The program recorded its failures in the open: false statements in its own plan, a prediction refuted by data, a hollow theorem caught by its own checks, and an independent referee’s corrections to the paper itself.
Source: R. Goodman, “Form, Choice, and History: what a single distinction decides in physics” (IAOM, October 2026; refereed, not yet posted).
Part V
Living information, and the stars.
17 · Why now
Provable matter is the trust layer three fast-moving fields are reaching for at once. The Institute’s contribution is the mathematical foundation under them, from sensor to proof to decision.
01
From 2 August 2026 the EU AI Act requires providers of general-purpose models to document training data; provenance is the new compliance surface. Standards such as C2PA sign a camera's output, and the Data & Trust Alliance has proposed data-provenance standards. A signature says where a number came from; our aim is a proof of what it means and when it may be trusted.
02
Digital monitoring, reporting and verification (dMRV) replaces manual, sample-based checks with continuous, data-driven verification; Verra approved its first dMRV-issued credits in 2026, with biodiversity, water and natural-capital markets following. Trusted environmental intelligence is becoming the defining asset — and an instrumented research apiary is a concrete place to earn it.
03
As AI moves from text to acting in the world, its decisions rest on sensor and actuator signals that are rarely grounded or checkable. The same boundary that lets a scientific pipeline accept, preserve or refuse a claim is what an autonomous system needs before it acts: measurement, then proof, then decision.
18 · Possible, compossible, actual
A configuration can be possible yet incompatible with another; compossible with it yet unreachable; reachable yet unstable. The program keeps these apart, and checks compatibility globally: three requirements on binary variables, x = y, y = z and x ≠ z, can be met in every pair and never all together.
The ledger’s chosen rows are exactly where the possible outruns the decided. Something selects. Our answer to what the selections build is a position, adopted deliberately and labelled for what it is.
Reality is one realised history.
IAOM’s adopted position · an ontological choice, not a result
space
The R-nucleus: the full lattice of what is generatively possible.
constraint
The constraints under which configurations can be sustained together.
history
The one history that realised selections have built, and keep building.
Compossibility alone supplies no probability measure or law of motion; those need further structure. A single history does not by itself exclude separate spatial domains, so their absence does not test it; the program bears on the position only through its consequences.
19 · Toward living information
Read the decided structure as the R-nucleus, the lattice of what is generatively possible. The choices at its edges are made by witnesses the structure brings into play. Their early choices look like random law because they carry no history; as they knot their records back into themselves, their capacity to choose and influence grows. Acts I–III organise results that exist; Acts IV and V are research programs, each with the condition that would kill it.
Act I · organises landed results
The full lattice of what is generatively possible. Under the ledger's stated premises, theorems decide an area law for shared information and a volume law for hidden information, the quantum ceiling on correlation, the end of the division-algebra tower, and the equation of state of counted hidden content. Twenty-five of the 45 questions live here.
Act II · interpretation of landed results
The decided structure stops at open alternatives. Whatever completes them is called a witness. Choices that are uniform across the visible universe behave as properties of the laws; per-event choices made with no distinguishing record follow the Born rule. On this reading, the randomness of quantum law is what choice looks like for a chooser with no history.
Act III · interpretation, with one model-based count
Every choice is a new distinction. Some magnitudes are counts of history, and hidden content conserved per comoving volume behaves as dust: a structural home for long memory, and the precise form of the hope that dark matter is made of information. The two mechanisms tested so far did not pass every data test together, and the paper says so.
Act IV · research program
What changes when a witness's next choice depends on its own record? The hypothesis is that influence lives in which context a witness chooses to measure, under a proved quantum ceiling on coordination, with records protected as windings.
Killed if no-signalling fails under its assumptions, or if every result reduces to standard measurement theory with no new consequence.
Act V · research program
When does a population of witnesses stop merely reacting and begin to model its world? The conjecture: modelling a computationally rich environment requires record dynamics on the universal side of a precise line (stabiliser circuits are classically simulable; Fibonacci braiding is universal), and a population that maintains its own consistency there deserves the name alive.
Killed if a non-universal population maintains consistency against a rich class, or if the definition collapses into a triviality or a tautology.
20 · Toward the stars
Ordinary computing begins with an algorithm and asks a machine to run it. Control engineering begins with a machine and asks which model describes it. We are joining the two directions: start from the structure of a phenomenon, keep what must be preserved, find the matter that realises it, compile with the evidence attached, act on the world, and keep measuring whether the world stays inside the model’s justified limits. That is a scientific program worth having even if the deepest metaphysical question is never settled.
And it is arriving when it is needed. When machine intelligence can extend physics and mathematics faster than people can check them, the limit on discovery is no longer insight; it is trust. A result that carries its own certificate can be built on the day it appears, by anyone, anywhere. Philosophy turned into mathematics a machine can verify, mathematics into programs that run, programs into instruments and machines that act within proved bounds, and every step left where the next person, or the next intelligence, can pick it up: that is how a civilisation that means to reach the stars should keep its knowledge.
Can we build a verified compiler that discovers how to realise an abstract mathematical system in physical hardware, and show that understanding the mathematics gives a measurable advantage in governing the real world?
The question at the centre of the program
The mass gap uniform in the lattice cutoff; the group field theory condensate; recovering length from the octonion algebra alone.
One transformation on three substrates, proved where it should agree and measured where it does; witnesses that read their own records (Act IV); the threshold of life (Act V).
Bring a question, an instrument, compute, or a critique. Every claim on this page names its status, so you can start where the work stops.
21 · Objections
A foundation becomes stronger when its best objections are turned into work.
Every formal account uses a metalanguage and rules. We expose them, keep a ledger of which premises are logical infrastructure, which are generative rules, which are interpretation and which are empirical, and count a result as stronger when it survives a change of presentation.
The broad thesis guides questions; particular models make predictions that can lose. The physics ledger fixed what each target could claim before the proofs, recorded a prediction refuted by data, and marks the root thesis as scored, not proved.
No blanket identity is assumed. We study which structures and behaviours a model preserves, and what evidence supports its physical interpretation.
No. A proof establishes a stated result under its assumptions. Experiment determines whether those assumptions describe the world well enough for the purpose.
Allocating work to accelerators has a long history, and so do filters, classifiers and safety controllers; none of those alone is our claim. What would be new, if it holds, is one compositional representation that carries mathematical meaning, refinement evidence, calibrated uncertainty and runtime authority across every one of them.
Then the program still stands. Whether mathematical structure is prior to matter is a philosophical question. Whether preserving it makes machines measurably better is an experiment, and the experiment is designed so that it can fail.
No. The foundation guides the questions we ask. A collaboration can succeed on a shared mathematical or scientific goal without anyone settling the origin of reality first.
22 · Ethos
Artificial intelligence is now writing the systems that run markets, science, infrastructure and judgment, faster than anyone can check them. What comes out is often unverifiable, because nobody can re-check what it claims to have done; uninterpretable, because not even its builders can explain its internal structure; and uncontrollable, because optimisation walks away from intent.
Hoping larger models become self-explanatory is not a plan. We seek to formalise the stack, from idea to theory to proof, program, runtime, hardware and physical reality, so that verifiability, interpretability and control become engineered properties an auditor can confirm from the artifacts alone.
Our ethos is computation using platonic forms. Our engineering ideal is formal math running on bare metal. Every layer machine-checked. Every claim verifiable.
They govern how the work is done, and each is backed by a control-system gate designed so that the models in the loop cannot alter it.
I
The kernel, the type checker, or the contracted gate is the arbiter. Not the deadline, not the deck, not the organization or Institution, and not the person who wants the answer.
II
Results should be reported from the kernel with a cryptographic seal whenever possible. If a mistake is made it should be instantly identifiable, so that the system can quickly and continually improve.
III
Then repair it. Build it better. Make it antifragile. Proactively find problems before you have to reactively bug-hunt. Document everything: full disclosure, so the lessons do not need to be repeated.
IV
Your work and your time deserve better than a green check mark or an emotionally charged reply. Renaming a theorem, softening a status label, or adding an honest-sounding note changes nothing in the world. Ask what the system can now do that it could not do before.
Improve your life, improve the world. Refuse false closure. Demand authenticity, demand value, not theater.