proof-native semantic computer
The horizon map
Every consequential act is one primitive, so a stranger holding a single root can check a whole history — re-running nothing, and trusting no one. This page is where that stands.
A research programme, not a product schedule. Nothing on this page carries a date, and every entry states its own scope. Where a fraction is known it is printed, because the fractions are the work.
Scope
A turn is the exercise of an attenuable, proof-carrying capability over owned state, leaving a receipt.
Read it backwards and it unpacks. A receipt is a witness anyone can check. A turn is one authorized step that leaves one. A capability is authority held by being able to produce its proof rather than by being named in a table, and it can be handed on weakened but never strengthened. Owned state is a cell: value that moves and is never minted, history that only grows.
The intended consequence is that illegal acts are not policed but unwitnessable — tamper with a field an act did not legitimately write and no proof exists. The project states this as its thesis; this page records how far it currently holds, and where it does not.
Status by area
Left is what holds today; then what is under active work, what is queued behind it, and the far shore — direction, without commitment. Read a row across to follow one line of research, or a column down to see the whole programme at one degree of certainty.
Seventeen lines · 151 entries · scrolls sideways on a narrow screen. A capture-ready copy sits at /horizonmap-plate/.
Standard of evidence
The word is not one thing. It marks a position on a slope, and the useful question is how high — a distinction the project draws for itself, and applies to its own results.
One rule makes the ladder mean anything: a passing check counts only if it fails when the thing it guards breaks. A theorem can be true and hollow; a gate can pass because it guards nothing. So each claim carries its own falsifier — the forgery, the mutation, the specific bad case — and that falsifier has to bite.
Limitations
Each was surfaced by the project's own instruments — the gates, the ratchets, the vacuity sweeps, the linters that read theorem statements rather than trusting their names.
A substantial body of proven material is not yet on the deployed path: exported functions without callers, an optimizer nothing runs, folding tests outside any automated lane, a seam that is off by default. Proving a thing and routing the running system through it are separate pieces of work.
Consensus is leaderless in the protocol and runs today on a single validator, tolerating zero faults; fault tolerance is established in simulation at four and seven nodes. The light client re-runs nothing and catches reordering conditional on the proof system, while the minting and omitting legs remain open and are named as such in the tree.
Several assumptions were stated in a form that is false at deployed parameters, and were refuted rather than renamed, then re-grounded on adversary-quantified games. The re-grounding is largely mechanical and is being applied across roughly nineteen hundred carriers.
A review of previously published material against current code found several statements the code does not support, including one on the flagship tamper property. Corrections belong in public, beside the original claim, rather than by quiet amendment.
Priority
One world, live on a durable public node, that an outsider can play and independently verify the root of — with nobody from the project present and no trusted server in the loop.
The objective in miniature is that sentence. It requires nothing frozen to begin, so it proceeds alongside the proof work rather than behind it; and until it happens, every other line here hardens a building no stranger has entered.
Evidence
Six hundred and seven entries were read out of the tree — the goal trails, the horizon log, the memory index, and the code — one reader per line of research. Each carries the file, theorem or commit it came from. The map above is distilled from these; this is the layer underneath it.
Authority is constructive knowledge. You hold a capability if and only if you can produce the witness for it — being named in a table counts for nothing. Everything else in the system is that one move, refracted.
A circuit here is not a machine. It is a refusal, written in polynomials: a grid of numbers, and laws that must come out to zero on every row. Multiply a law by a selector and it becomes active on the rows that owe it, vacuous on the rest — which is how one circuit can hold thirty-odd different effects.
Every proof stops somewhere, and the discipline is to say where and then attack your own floor. A security claim stated as “no solution exists” is empty at real parameters, because a compressing hash has collisions, by pigeonhole. So a floor that cannot be defended gets deleted or proven false — never quietly renamed.
A proof that re-verifies a proof that re-verifies a proof, where the shape never changes with depth. The cost of folding grows with the history; the cost of checking does not. Pin one anchor and you have the whole story.
Every block cites everything its author has seen, so the record is a weave rather than a chain. Nobody leads. An ordering falls out of the structure, and a supermajority ratifies it — and a node that signs two versions of one slot has published its own eviction notice.
The interesting move is not building a bridge. It is re-deriving another chain's proof system from that chain's own sources, so a foreign fact arrives as evidence you can check rather than as hearsay from whoever runs the bridge.
Testing can only ever show a bug is present; it can never show one is absent. And absent is the only thing that keeps you safe. This is the ordinary plumbing of the web — parsers, handshakes, proxies — with absence proved instead of hoped for.
Forty years of authoring systems hit the same ceiling. HyperCard let everyone author and never networked. Smalltalk was a live image you edit from inside, with no security or provenance. Xanadu wanted transclusion and shipped vapour. Here a window is a capability, a button is a verified turn, and a conflict is an object you carry rather than a merge that failed.
An illegal move is not forbidden by application code. There is simply no proof of it, so it cannot be witnessed. Rules become theorems, and the referee shows its work — which also means re-writing a game as mathematics tends to find the bugs the old implementation was hiding.
A glass box. Inside it a mind earns, spends, and runs a small business; the box is glass because every move drops a receipt anyone can check. You do not have to trust the keeper — and neither does anything else.
Batch clearing where everyone in the batch pays the same price, and an unfair clearing is not punished after the fact but refused, because the certificate does not verify. The price ends up public. The book never is.
Two auditors agreeing is an aggregation of assertions, and the classical impossibility results say there is no well-behaved adjudicator there. A witness is different: it is a realizability fact, and a Byzantine majority cannot conjure one. Hence the aim — a verdict should be a witness, not a vote.
There is no save button. The log of what happened, plus deterministic replay, is the persistence — so recovery is just replay, and a forged or shortened log has no matching root to pass itself off with.
Arithmetic carried out on values nobody involved is allowed to read, with the invariant enforced on the ciphertext and only the outcome ever decrypted — by a committee, none of whom can open it alone.
You got an answer over TLS. Can you show a third party what the model said, without handing over your API key or asking them to trust a screenshot? Three legs — it really came from that session, it parses, it was not injected — composed into one theorem.
Macaroons and biscuits, taken seriously: an attenuable token whose exercise is a derivation, and a derivation is a circuit. You can hand on less than you hold, never more, and the proof rides along with the grant.
Everything the mathematics earns is worth nothing to an outsider until a stranger can clone the repository into an empty directory and get the same green the author gets. This line is the difference between a result and a fact.
The whole dark egg remains whole.
One capability, proven once and carried everywhere — to the chip, the cell, the screen, the row in a database, an agent's next action. The proof that a light client cannot be fooled is the proof that the person at the glass cannot be fooled either.