Tout transfert de valeur — de la monnaie ou un justificatif signé, tel qu'un billet — a un émetteur vérifié et un destinataire vérifié, et aucune opération de la chaîne ne diminue le solde d'un portefeuille sans que ce portefeuille en soit le payeur. Pas de comptes fantômes, pas de robots, aucune main sur la monnaie de quiconque : la fraude au faux participant devient une impossibilité démontrée, non un risque géré.

La masse monétaire n'augmente qu'au règlement d'une expérience vécue authentifiée — la dotation du participant, le côté offre, et l'enveloppe de service publiée qui rémunère l'infrastructure qui l'a rendue possible — et à aucun autre moment. La valeur naît de la participation vécue, jamais d'une écriture arbitraire.

Une personne peut faire effacer son identité — droit européen oblige — sans perdre un centime de ses avoirs. Vie privée et propriété cessent d'être en conflit.

Aucun bloc n'est jamais validé avec un invariant d'offre rompu — la chaîne s'arrête d'abord, plutôt que de continuer sur une base fausse. La sûreté prime la disponibilité.

Le Modèle Zéro, c'est la chaîne écrite comme une machine à états en Lean 4 (noyau seul, sans bibliothèque) : chaque opération qu'elle peut effectuer, l'état de départ, et les quatre théorèmes énoncés comme invariants sur les états atteignables. Quatre hypothèses sont nommées à gauche du symbole et jamais prouvées — H1 une signature valide provient de la clé de l'émetteur nommé ; H2 le consensus livre un journal unique et ordonné ; H3 une instance accréditée n'atteste que des humains réels ; H4 une expérience authentifiée a bien eu lieu, avec les personnes qu'elle recense. Dix-huit énoncés ; quinze prouvés sur le modèle ; trois ouverts, tous d'arithmétique de grand livre. Rien n'est prouvé du code — les preuves sont courtes, et la difficulté réside dans les définitions et dans l'implémentation. La relecture en langue naturelle du modèle a été validée phrase par phrase par le concepteur avant publication. Le modèle a été construit avec l'assistance d'une IA — l'assistant rédige définitions et preuves, le concepteur tranche, le noyau Lean vérifie — à partir du corpus de conception publié du projet, chaque étape étant journalisée. Savoir si l'ingénierie de preuve assistée par IA peut mener un tel système du modèle à une implémentation vérifiée, à l'échelle de la production, est une question ouverte — et c'est celle à laquelle ce programme existe pour répondre. Le fichier est disponible sur demande ; la publication en source ouverte suivra la première relecture externe.

Toute transaction qu'une banque règle a une contrepartie : la chose pour laquelle l'argent est versé. C'est ce que nous appelons la jambe du droit d'entrée, par opposition à la jambe monétaire, celle où l'argent circule. Les quatre théorèmes ne sont pas des affirmations sur l'argent en général : ils portent sur une contrepartie d'un type précis. Ils s'appliquent pleinement lorsque cette contrepartie possède quatre propriétés : elle est détenue par une personne (ou une organisation) vérifiée ; elle est liée à un moment qui peut être authentifié — une porte franchie, une présence, une remise en main propre ; elle ne peut pas être dupliquée — un droit, un titulaire, un usage ; et la fraude vit dans le droit plutôt que dans l'argent — un faux droit, un droit vendu deux fois, un droit envoyé à un usurpateur. Lorsque les quatre propriétés sont réunies, la jambe du droit d'entrée de ROCKR répond entièrement. Lorsque seule la première est réunie, le théorème 1 suffit encore à faire une différence. Lorsqu'aucune ne l'est, les théorèmes ne changent rien — et nous le disons.

Portée pleine — les quatre théorèmes agissent sur la contrepartie

Les droits d'assister ou d'utiliser : billets, adhésions, cours et formations, titres de transport, rendez-vous, accès à une salle ou un club. Le cas fondateur ; la porte est littérale. Les subventions, bons et allocations versés contre une participation : le programme de compétences de Lloyds, les ateliers du Projet Banlieues, les heures de bénévolat des salariés — et, exemple français le plus net, le pass Culture, un droit accordé par l'État aux jeunes et dépensable seulement en expériences culturelles ; c'est exactement la forme du crédit RUIPA, et le théorème 2 en est tout l'objet. Les paiements de place de marché entre particuliers pour un droit ou un retrait : le cas d'usage que Lloyds a lui-même nommé, le retrait en magasin, le billet d'occasion — acheteur et vendeur vérifiés (théorème 1), valeur séquestrée conservée (théorème 4), remise authentifiée (théorème 2). Les avantages en nature avec un moment de retrait : repas, places de sortie scolaire, subventions de club sportif.

Portée partielle — le théorème 1 fait le travail, les trois autres restent en sommeil

Les virements entre particuliers — la classe du faux conseiller : le bénéficiaire est une identité vérifiée, il n'y a donc ni compte mule anonyme ni « compte sécurisé » où envoyer l'argent. Les théorèmes 2 à 4 n'ajoutent rien, faute d'événement et de droit conservé — mais c'est le gain le plus important en valeur, parce que c'est là que vivent les 245 millions d'euros de fraude par manipulation du premier semestre 2025 en France. Les prélèvements et abonnements : un créancier vérifié supprime le faux mandat ; rien d'autre ne change. L'ouverture de compte et l'octroi de crédit : l'unicité du théorème 1 — un humain, une identité — défait les identités synthétiques et les doublons à l'entrée ; le prêt lui-même, promesse de rembourser, n'a pas d'événement à authentifier. Les titres, fonds et obligations tokenisés — le propre chantier de BNP Paribas : la vérification du détenteur et la conservation sont réelles mais déjà assurées par des jetons à accès restreint ; ROCKR y ajoute le théorème 3 — l'effacement sans perte des avoirs, que le RGPD (règlement général sur la protection des données) rend précieux — et rien qu'ils ne puissent obtenir autrement sur les théorèmes 1 et 4.

Hors de portée — les théorèmes ne s'appliquent pas, et nous ne les étirons pas

L'argent contre l'argent : le change, le règlement interbancaire et de trésorerie, les intérêts, les dividendes. Les deux jambes sont de l'argent ; il n'y a pas de droit à prouver. C'est tout le domaine de Pontes, de Qivalis et de la monnaie de banque centrale tokenisée — c'est pourquoi nous l'appelons la jambe monétaire et la laissons aux banques. Les espèces : l'anonymat est le principe même ; le théorème 1 est son contraire. L'assurance et les garanties : de l'argent contre une promesse conditionnelle ; le sinistre est instruit, non franchi. Les biens livrés à domicile et les contenus diffusés ou téléchargés : aucun moment authentifiable où une personne vérifiée reçoit un droit conservé — et la fraude à la carte est déjà tombée sous 0,05 % en France. Les flux d'institution à institution sans détenteur humain : compensation, netting, opérations intragroupe ; rien dans notre architecture n'est construit pour cela, et nous ne le revendiquons pas.

Deux réserves d'honnêteté. Même dans les cas de portée pleine, la banque ne réalise le gain que si sa jambe monétaire se règle atomiquement contre la jambe du droit d'entrée de ROCKR — cette jonction est une promesse de conception, pas encore une démonstration. Et la proportion compte : en nombre de transactions, les théorèmes atteignent une minorité de ce qu'une banque traite ; en valeur de fraude dans le portefeuille des particuliers, la majorité. C'est la seconde affirmation que nous défendons, pas la première : les théorèmes atteignent la partie du portefeuille où vit la responsabilité du règlement européen sur les services de paiement — non « les transactions de la banque ».

ROCKR Preuves — dénomination développée : Association pour la vérification formelle des infrastructures numériques de confiance — est une association loi 1901 constituée le 11 août 2026 à Grand-Brassac, France, par ses membres fondateurs.

Conduire des travaux de vérification formelle sur les infrastructures numériques de confiance — protocoles d'identité, de règlement et d'authentification d'activités réelles ; solliciter et gérer des financements publics de recherche ; contracter avec des scientifiques et des laboratoires ; publier l'intégralité des résultats en accès libre.

Nos preuves sont produites avec l'assistance d'une IA, à partir d'un corpus de conception publié : l'assistant rédige définitions et preuves, le concepteur tranche chaque question que la rédaction fait surgir, et le noyau Lean est le seul arbitre. Chaque étape et chaque décision sont journalisées. Que l'ingénierie de preuve assistée par IA puisse mener un système critique pour la sécurité du modèle à une implémentation vérifiée, à l'échelle de la production, n'a jamais été démontré ; répondre à cette question — sous revue adverse, au grand jour — fait autant partie de l'objet de l'association que les quatre théorèmes.

Les quatre théorèmes sont issus d'un système réel : l'architecture ROCKR–ROCKRCOIN, un protocole de règlement open source, fondé sur l'identité vérifiée, au service de l'économie de l'expérience vécue. La recherche elle-même est générique — ses résultats ont vocation à servir bien au-delà du système qui a posé les questions.

Le développement est financé exclusivement par des programmes publics de recherche — jamais par du capital-risque — afin de préserver l'indépendance, la transparence et la libre disponibilité des résultats.

Le véhicule français et européen du programme de preuve : financements publics français et européens, coopération avec les scientifiques et laboratoires, publication en accès libre.

Le jumeau britannique porte le même programme auprès de la communauté et des financeurs du Royaume-Uni. La coopération entre les deux véhicules est inscrite dans l'objet même de l'association — non laissée à l'usage. rockrprooflabs.org

La plateforme qui met la participation vérifiée au service de l'économie de l'expérience vécue — concerts, cours, rencontres : tout ce qui rassemble de vraies personnes en un lieu réel.

Le protocole de règlement open source fondé sur l'identité vérifiée — la source des quatre théorèmes. Livre blanc.

Chercheurs, laboratoires, financeurs et relecteurs adverses bienvenus. Les questions difficiles améliorent le travail — et la réponse la plus précieuse de toutes est celle d'un relecteur qui s'attaque aux définitions et aux énoncés des théorèmes du Modèle Zéro : chaque objection est une ligne à changer et une recompilation.

Toute personne qui suit les projets étudiés est bienvenue pour suivre également nos échanges : la transparence est notre méthode de travail, non un risque à maîtriser.

En 1965, Roger Penrose démontre que l'effondrement d'une étoile massive produit nécessairement une singularité — un point où la gravité devient infinie et où les lois de la physique cessent simplement de fonctionner. Ces travaux lui vaudront le prix Nobel de physique 2020, et laissent une question qui façonnera toute sa carrière : quelle théorie pourrait décrire la réalité là où nos meilleures équations échouent ? Sa réponse, poursuivie sur des décennies, est géométrique — sous l'espace et le temps il y a une structure, et la comprendre demandera plus que du calcul.

Kurt Gödel a démontré que tout système mathématique suffisamment riche contient des vérités qui ne peuvent être prouvées en suivant les règles de ce système. Et pourtant, les mathématiciens humains savent sortir des règles et simplement voir que ces énoncés sont vrais. Penrose en tire une conclusion audacieuse : la compréhension humaine n'est pas, au fond, une exécution de règles — pas un calcul.

Le mécanisme physique qu'il propose se situe à la lisière spéculative de la physique ; il est contesté, et il le dit lui-même. Ce qui compte pour notre histoire, c'est la porte que cela ouvre : si l'esprit peut saisir des vérités qu'aucun algorithme n'atteint, où ces vérités vivent-elles ?

L'identité d'Euler — e^iπ + 1 = 0 — ne peut être réinterprétée par un démagogue ni tordue pour justifier une guerre. Son sens est contenu tout entier en elle-même : scellé contre la mésinterprétation. Platon soutenait que de telles vérités — et peut-être la beauté, peut-être le bien — existent indépendamment de nous : l'esprit ne les invente pas, il les découvre.

Penrose prend cette vue au sérieux jusque dans la géométrie de l'univers. L'extension morale est une hypothèse, pas un résultat — mais le cœur mathématique est un fait simple : certaines vérités ne peuvent pas être détournées.

Démocratie, capitalisme, socialisme, religion, science : aucun n'est intrinsèquement bon ou mauvais. Ils sont faits de langage, et le langage est poreux — un régime peut emprisonner ses opposants au nom de la « protection de la démocratie », et aucune constante fondamentale de l'univers n'existe pour dénoncer l'abus. Quand nous tentons de porter un absolu — la justice, l'équité, le sens — dans des institutions, quelque chose se perd à la traduction : l'idéal arrive en « -isme », un récipient que saints et tyrans peuvent saisir également.

Aucun système ne nous sauvera par sa seule existence. Tout système exige des opérateurs vigilants et éthiques — et des citoyens disposés à chercher ce qui est vrai. Comme l'enseignait Platon, tout ce que l'on peut faire, c'est inculquer la disposition à découvrir la vérité.

ROCKR existe pour créer un environnement où inculquer cette disposition — la disposition à découvrir ce qui est vrai — soit possible de manière indépendante, pour chaque individu et chaque communauté. Nous ne pouvons pas rendre une idéologie intrinsèquement bonne ; personne ne le peut. Ce que nous pouvons faire, c'est accomplir deux gestes à la fois : sortir les promesses porteuses d'un système du langage détournable pour les porter dans les mathématiques, le seul médium où la vérité survit à la traduction — et sortir le système lui-même des institutions lointaines pour le porter dans les lieux de vie de la communauté locale. Les quatre théorèmes sont le premier geste devenu réel : les garanties sur lesquelles chacun doit pouvoir compter — de vraies personnes, une vraie présence, l'effacement sans spoliation, une masse monétaire qui ne peut pas mentir — énoncées en mathématiques vérifiables par machine plutôt qu'en conditions générales (LB 8.1, contexte).

Et la philosophie fixe le but autant que la méthode : une communauté qui organise elle-même ses expériences vécues — de tout type, de tout genre, choisies de bas en haut — est un environnement où la disposition à découvrir ce qui est vrai peut grandir. Les crédits RUIPA ouvrent cet environnement à tous ; les théorèmes rendent incorruptible la liquidité qui le porte.

Nous ne prétendons pas que ROCKR est intrinsèquement bon ; rien de ce que bâtissent les humains ne l'est. Nous affirmons que ses garanties sont écrites dans le seul langage qui ne peut pas être détourné — et que tout le reste demeure, comme il se doit, entre les mains de l'individu et de la communauté.