Every transfer of value — coin or a signed credential such as a ticket — has a verified sender and a verified recipient, and no move on the chain lowers a wallet's balance unless that wallet is the payer. No ghost accounts, no bots, no hand in anyone's coin: fake-participant fraud becomes a demonstrated impossibility, not a managed risk.

The money supply grows only at the settlement of an authenticated live experience — the participant's grant, the supply side, and the published service envelope that pays the infrastructure which made it possible — and at no other moment. Value is born of lived participation, never of an arbitrary entry in a ledger.

A person can have their identity erased — as European and UK data law requires — without losing a penny of their assets. Privacy and property stop being in conflict.

No block ever commits with a supply invariant broken — the chain halts first, rather than continue on a false basis. Safety outranks availability.

Model Zero is the chain written as a state machine in Lean 4 (core only, no libraries): every move it can make, the starting state, and the four theorems stated as invariants over reachable states. Four hypotheses are named on the left of the turnstile and never proved — H1 a valid signature came from the named issuer's key; H2 consensus delivers one ordered log; H3 an accredited instance attests only real humans; H4 an authenticated experience happened with the people it lists. Eighteen statements; fifteen proved on the model; three open, all ledger arithmetic. Nothing is proved of any code — the proofs are short and the difficulty lies in the definitions and in the implementation. The model's English read-back was validated sentence by sentence by the designer before publication. The model was constructed with AI assistance — the assistant drafting definitions and proofs, the designer ruling, the Lean kernel checking — under the project's published design corpus, with every step logged. Whether AI-assisted proof engineering can carry a system like this from model to verified implementation at production scale is an open question, and it is the one this programme exists to answer. The file is available on request; open-source release follows the first external reading.

Every transaction a bank settles has a counter-item: the thing the money is paid for. That is what we call the entitlement leg, as against the settlement leg (the money leg), where the money moves. The four theorems are not claims about money in general: they are about a counter-item of a particular kind. They apply in full when that counter-item has four properties: it is held by a verified person (or organisation); it is tied to a moment that can be authenticated — a gate passed, a presence, a hand-over; it cannot be duplicated — one right, one holder, one use; and the fraud lives in the right rather than in the money — a fake right, a right sold twice, a right sent to an impersonator. Where all four hold, ROCKR's entitlement leg answers in full. Where only the first holds, Theorem 1 alone still makes a difference. Where none holds, the theorems change nothing — and we say so.

Full reach — all four theorems act on the counter-item

Rights to attend or use: tickets, memberships, courses and training, transport passes, appointments, access to a venue or club. The founding case; the gate is literal. Grants, vouchers and allowances issued against participation: Lloyds's skills programme, Projet Banlieues workshops, employee volunteering hours — and, the sharpest French example, the pass Culture, a state entitlement to young people spendable only on cultural experiences; it is exactly the shape of the RUIPA credit, and Theorem 2 is its whole point. Peer-to-peer marketplace payments for a right or a collection: the use case Lloyds itself has named, click-and-collect, a second-hand ticket — buyer and seller verified (Theorem 1), escrowed value conserved (Theorem 4), hand-over authenticated (Theorem 2). Benefits in kind with a redemption moment: meals, school-trip places, sports-club subsidies.

Partial reach — Theorem 1 does the work, the other three lie dormant

Person-to-person transfers — the false-adviser class: the recipient is a verified identity, so there is no anonymous mule account and no "safe account" to send money to. Theorems 2 to 4 add nothing, for want of an event and a conserved right — but this is the largest gain by value, because it is where the £1bn-plus that Lloyds intercepted in 2025 and the €245m of French manipulation fraud in the first half of 2025 both sit. Direct debits and subscriptions: a verified payee removes the fake mandate; nothing else changes. Account opening and credit origination: Theorem 1's uniqueness — one human, one identity — defeats synthetic and duplicate identities at the door; the loan itself, a promise to repay, has no event to authenticate. Tokenised securities, funds and bonds — BNP Paribas's own work, and Lloyds's tokenised gilt: holder verification and conservation are real but already delivered by permissioned tokens; ROCKR adds Theorem 3 — erasure without loss of holdings, which the GDPR (General Data Protection Regulation) makes valuable — and nothing they cannot otherwise obtain on Theorems 1 and 4.

Out of reach — the theorems do not apply, and we do not stretch them

Money for money: foreign exchange, interbank and treasury settlement, interest, dividends. Both legs are money; there is no right to prove. This is the whole domain of Pontes, Qivalis, Great British Tokenised Deposits and tokenised central-bank money — which is why we call it the settlement leg and leave it to the banks. Cash: anonymity is its principle; Theorem 1 is its opposite. Insurance and guarantees: money for a contingent promise; the claim is adjudicated, not gated. Home-delivered goods and streamed or downloaded content: no authenticatable moment at which a verified person receives a conserved right. Institution-to-institution flows with no human holder: clearing, netting, intra-group; nothing in our architecture is built for it, and we do not claim it.

Two honesty reservations. Even in the full-reach cases, the bank realises the gain only if its settlement leg settles atomically against ROCKR's entitlement leg — that join is a design promise, not yet a demonstration. And proportion matters: by transaction count the theorems reach a minority of what a bank processes; by fraud value in the consumer book, the majority. We defend the second claim, not the first: the theorems reach the part of the book where the Payment Services Regulation liability lives — not "the bank's transactions".

ROCKR Proof Labs Ltd is the United Kingdom research vehicle of the programme: a company incorporated in July 2026, in London, to carry the proof work to the UK research community and its funders.

To conduct formal verification work on trusted digital infrastructure — identity, settlement, and the authentication of real-world activity; to seek and manage public research funding; to contract with scientists and laboratories; and to publish all results open access.

Our proofs are produced with AI assistance under a published design corpus: the assistant drafts definitions and proofs, the designer rules on every question the drafting surfaces, and the Lean kernel is the only referee. Every step and every ruling is logged. Whether AI-assisted proof engineering can carry a security-critical system from model to verified implementation at production scale has never been shown; answering that question — under adversarial review, in the open — is as much the company's purpose as the four theorems are.

The four theorems come from a real system: the ROCKR–ROCKRCOIN architecture, an open-source settlement protocol built on verified identity, serving the live experience economy. The research itself is generic — its results are meant to serve far beyond the system that posed the questions.

Development is funded exclusively through public research programmes — never venture capital — to preserve independence, transparency, and the free availability of the results.

The UK vehicle of the proof programme: public UK research funding, cooperation with scientists and laboratories, open-access publication.

The French twin carries the same programme to the French and European research community and its funders. Cooperation between the two research vehicles is written into the association's founding purpose — not left to custom. rockrpreuves.fr

The platform that puts verified participation to work for the live experience economy — concerts, classes, gatherings: everything that brings real people together in a real place.

The open-source settlement protocol built on verified identity — the source of the four theorems. Whitepaper.

Researchers, laboratories, venues, funders and adversarial reviewers welcome. If this programme should exist, say so — a short supportive statement, published here with your name, helps the proofs get funded. Hard questions improve the work just as much — and the most valuable response of all is a reader who attacks the definitions and theorem statements of Model Zero: every strike is a one-line change and a re-compile.

Anyone following the projects we study is welcome to follow our exchanges too: transparency is our working method, not a risk to be managed.

In 1965 Roger Penrose proved that when a massive star collapses, it must form a singularity — a point where gravity becomes infinite and the laws of physics simply stop working. The work earned him the 2020 Nobel Prize in Physics, and it left a question that shaped the rest of his career: what kind of theory could describe reality where our best equations fail? His answer, pursued over decades, was geometric — beneath space and time there is structure, and understanding it would take more than computation.

Kurt Gödel proved that any sufficiently rich mathematical system contains truths that cannot be proven by following that system's own rules. Yet human mathematicians can step outside the rules and simply see that those statements are true. Penrose drew a bold conclusion: human understanding is not, at bottom, rule-following — not a computation.

His proposed physical mechanism for this sits at the speculative edge of physics, is contested, and he says so. What matters for this story is the door it opens: if minds can grasp truths no algorithm reaches, where do those truths live?

Euler's identity — e^iπ + 1 = 0 — cannot be reinterpreted by a demagogue or twisted to justify a war. Its meaning is contained entirely within itself: sealed against misinterpretation. Plato held that such truths — and perhaps beauty, perhaps goodness — exist independently of us: the mind does not invent them, it discovers them.

Penrose takes that view seriously all the way down into the geometry of the universe. The moral extension is a hypothesis, not a result — but the mathematical core is plain fact: some truths cannot be hijacked.

Democracy, capitalism, socialism, religion, science: none is intrinsically good or bad. They are built from language, and language is porous — a regime can imprison dissidents in the name of "protecting democracy", and no fundamental constant of the universe exists to expose the misuse. When we try to carry an absolute — justice, equity, meaning — into institutions, something is lost in translation: the ideal arrives as an "-ism", a vessel that saints and tyrants can pick up alike.

No system will save us by existing. Every system needs vigilant, ethical operators — and citizens with the disposition to look for what is true. As Plato taught, all anyone can do is inculcate the disposition to discover truth.

ROCKR exists to create an environment where inculcating that disposition — the disposition to discover what is true — is independently possible, for every individual and every community. We cannot make an ideology intrinsically good; nobody can. What we can do is make two moves at once: move a system's load-bearing promises out of hijackable language and into mathematics, the one medium where truth survives translation — and move the system itself out of distant institutions and into the living spaces of the local community. The four theorems are the first move made real: the guarantees people must rely on — real people, real presence, erasure without expropriation, a supply that cannot lie — stated as machine-checkable mathematics rather than terms of service (WP 8.1, Background).

And the philosophy sets the purpose as well as the method: a community that curates its own live experiences — every kind, every genre, chosen bottom up — is an environment where the disposition to discover what is true can grow. RUIPA grants make that environment open to everyone; the theorems make the liquidity behind it incorruptible.

We do not claim ROCKR is intrinsically good; nothing built by people is. We claim its guarantees are written in the one language that cannot be hijacked — and that everything else stays, as it must, in the hands of the individual and the community.