Toda transferencia de valor — moneda o un justificante firmado, como una entrada — tiene un emisor verificado y un destinatario verificado, y ninguna operación de la cadena reduce el saldo de una cartera sin que esa cartera sea el pagador. Sin cuentas fantasma, sin robots, ninguna mano sobre el dinero de nadie: el fraude del falso participante se convierte en una imposibilidad demostrada, no en un riesgo gestionado.

La masa monetaria sólo aumenta en la liquidación de una experiencia vivida autenticada — la dotación del participante, el lado de la oferta, y el sobre de servicio publicado que remunera la infraestructura que la hizo posible — y en ningún otro momento. El valor nace de la participación vivida, nunca de un apunte arbitrario.

Una persona puede hacer borrar su identidad — el derecho europeo obliga — sin perder un céntimo de sus activos. Privacidad y propiedad dejan de estar en conflicto.

Ningún bloque se valida jamás con un invariante de oferta roto — la cadena se detiene antes, en lugar de continuar sobre una base falsa. La seguridad prima sobre la disponibilidad.

El Modelo Cero es la cadena escrita como una máquina de estados en Lean 4 (sólo el núcleo, sin biblioteca): cada operación que puede efectuar, el estado de partida, y los cuatro teoremas enunciados como invariantes sobre los estados alcanzables. Cuatro hipótesis se nombran a la izquierda del símbolo y nunca se prueban — H1 una firma válida procede de la clave del emisor nombrado; H2 el consenso entrega un diario único y ordenado; H3 una instancia acreditada sólo atesta humanos reales; H4 una experiencia autenticada tuvo lugar realmente, con las personas que recoge. Dieciocho enunciados; quince probados sobre el modelo; tres abiertos, todos de aritmética de libro mayor. Nada está probado del código — las pruebas son cortas, y la dificultad reside en las definiciones y en la implementación. La relectura en lengua natural del modelo fue validada frase a frase por el diseñador antes de su publicación. El modelo se construyó con la asistencia de una IA — el asistente redacta definiciones y pruebas, el diseñador decide, el núcleo Lean verifica — a partir del corpus de diseño publicado del proyecto, con cada paso registrado. Si la ingeniería de prueba asistida por IA puede llevar un sistema así del modelo a una implementación verificada, a escala de producción, es una pregunta abierta — y es aquella a la que este programa existe para responder. El fichero está disponible bajo petición; la publicación en código abierto seguirá a la primera relectura externa.

Toda transacción que un banco liquida tiene una contrapartida: aquello por lo que se paga el dinero. Es lo que llamamos la pierna del derecho de entrada, frente a la pierna monetaria, aquella por la que circula el dinero. Los cuatro teoremas no son afirmaciones sobre el dinero en general: tratan de una contrapartida de un tipo preciso. Se aplican plenamente cuando esa contrapartida reúne cuatro propiedades: está en manos de una persona (u organización) verificada; está ligada a un momento que puede autenticarse — una puerta cruzada, una presencia, una entrega en mano; no puede duplicarse — un derecho, un titular, un uso; y el fraude vive en el derecho y no en el dinero — un derecho falso, un derecho vendido dos veces, un derecho enviado a un suplantador. Cuando se dan las cuatro, la pierna del derecho de entrada de ROCKR responde por completo. Cuando sólo se da la primera, el teorema 1 sigue bastando para marcar una diferencia. Cuando no se da ninguna, los teoremas no cambian nada — y lo decimos.

Alcance pleno — los cuatro teoremas actúan sobre la contrapartida

Los derechos de asistir o de usar: entradas, socios, cursos y formaciones, títulos de transporte, citas, acceso a una sala o a un club. El caso fundacional; la puerta es literal. Las subvenciones, bonos y ayudas emitidos contra una participación: el programa de competencias de Lloyds, los talleres del Projet Banlieues, las horas de voluntariado de los empleados — y, el ejemplo francés más nítido, el pass Culture, un derecho concedido por el Estado a los jóvenes y gastable sólo en experiencias culturales; es exactamente la forma del crédito RUIPA, y el teorema 2 es todo su objeto. Los pagos de mercado entre particulares por un derecho o una recogida: el caso de uso que el propio Lloyds ha nombrado, la recogida en tienda, la entrada de segunda mano — comprador y vendedor verificados (teorema 1), valor en garantía conservado (teorema 4), entrega autenticada (teorema 2). Las prestaciones en especie con un momento de canje: comidas, plazas de excursión escolar, ayudas a clubes deportivos.

Alcance parcial — el teorema 1 hace el trabajo, los otros tres quedan dormidos

Las transferencias entre particulares — la clase del falso asesor: el beneficiario es una identidad verificada, así que no hay cuenta mula anónima ni «cuenta segura» a la que enviar el dinero. Los teoremas 2 a 4 no añaden nada, por falta de evento y de derecho conservado — pero es la mayor ganancia en valor, porque ahí viven los 245 millones de euros de fraude por manipulación del primer semestre de 2025 en Francia, y las 429.677 estafas informáticas de 2025 en España. Los recibos domiciliados y suscripciones: un acreedor verificado elimina el mandato falso; nada más cambia. La apertura de cuenta y la concesión de crédito: la unicidad del teorema 1 — un humano, una identidad — desbarata las identidades sintéticas y los duplicados en la entrada; el préstamo en sí, una promesa de devolver, no tiene evento que autenticar. Los valores, fondos y bonos tokenizados — la propia obra de BNP Paribas: la verificación del titular y la conservación son reales pero ya las garantizan los tokens de acceso restringido; ROCKR añade el teorema 3 — el borrado sin pérdida de los activos, que el RGPD (Reglamento General de Protección de Datos) hace valioso — y nada que no puedan obtener de otro modo en los teoremas 1 y 4.

Fuera de alcance — los teoremas no se aplican, y no los forzamos

Dinero contra dinero: divisas, liquidación interbancaria y de tesorería, intereses, dividendos. Las dos piernas son dinero; no hay derecho que demostrar. Es todo el dominio de Pontes, de Qivalis y del dinero de banco central tokenizado — por eso lo llamamos pierna monetaria y lo dejamos a los bancos. El efectivo: el anonimato es su principio; el teorema 1 es lo contrario. Los seguros y las garantías: dinero contra una promesa condicional; el siniestro se instruye, no se cruza. Los bienes entregados a domicilio y los contenidos en streaming o descargados: ningún momento autenticable en que una persona verificada reciba un derecho conservado. Los flujos de institución a institución sin titular humano: compensación, neteo, operaciones intragrupo; nada en nuestra arquitectura está construido para ello, y no lo reivindicamos.

Dos reservas de honestidad. Incluso en los casos de alcance pleno, el banco sólo obtiene la ganancia si su pierna monetaria se liquida atómicamente contra la pierna del derecho de entrada de ROCKR — esa unión es una promesa de diseño, no todavía una demostración. Y la proporción importa: en número de transacciones, los teoremas alcanzan una minoría de lo que un banco procesa; en valor del fraude en la cartera de particulares, la mayoría. Defendemos la segunda afirmación, no la primera: los teoremas alcanzan la parte de la cartera donde vive la responsabilidad del Reglamento de Servicios de Pago europeo — no «las transacciones del banco».

ROCKR Preuves — denominación completa: Association pour la vérification formelle des infrastructures numériques de confiance («Asociación para la verificación formal de las infraestructuras digitales de confianza») — es una asociación de la ley francesa de 1901, constituida el 11 de agosto de 2026 en Grand-Brassac, Francia, por sus miembros fundadores.

Realizar trabajos de verificación formal sobre las infraestructuras digitales de confianza — protocolos de identidad, de liquidación y de autenticación de actividades reales; solicitar y gestionar financiación pública de investigación; contratar con científicos y laboratorios; publicar la totalidad de los resultados en acceso abierto.

Nuestras pruebas se producen con la asistencia de una IA, a partir de un corpus de diseño publicado: el asistente redacta definiciones y pruebas, el diseñador decide cada cuestión que la redacción hace surgir, y el núcleo Lean es el único árbitro. Cada paso y cada decisión quedan registrados. Que la ingeniería de prueba asistida por IA pueda llevar un sistema crítico para la seguridad del modelo a una implementación verificada, a escala de producción, no se ha demostrado, hasta donde sabemos, todavía; responder a esa pregunta — bajo revisión adversa, a la vista de todos — forma parte del objeto de la asociación tanto como los cuatro teoremas.

Los cuatro teoremas proceden de un sistema real: la arquitectura ROCKR–ROCKRCOIN, un protocolo de liquidación de código abierto, fundado en la identidad verificada, al servicio de la economía de la experiencia vivida. La investigación misma es genérica — sus resultados están llamados a servir mucho más allá del sistema que planteó las preguntas.

El desarrollo se financia exclusivamente con programas públicos de investigación — nunca con capital riesgo — para preservar la independencia, la transparencia y la libre disponibilidad de los resultados.

El vehículo francés y europeo del programa de prueba: financiación pública francesa y europea, cooperación con científicos y laboratorios, publicación en acceso abierto.

El gemelo británico lleva el mismo programa ante la comunidad y los financiadores del Reino Unido. La cooperación entre los dos vehículos está inscrita en el propio objeto de la asociación — no dejada a la costumbre. rockrprooflabs.org

La plataforma que pone la participación verificada al servicio de la economía de la experiencia vivida — conciertos, clases, encuentros: todo lo que reúne a personas reales en un lugar real.

El protocolo de liquidación de código abierto fundado en la identidad verificada — la fuente de los cuatro teoremas. Libro blanco.

Investigadores, laboratorios, financiadores y revisores adversos son bienvenidos. Las preguntas difíciles mejoran el trabajo — y la respuesta más valiosa de todas es la de un revisor que se enfrenta a las definiciones y a los enunciados de los teoremas del Modelo Cero: cada objeción es una línea que cambiar y una recompilación.

Toda persona que sigue los proyectos estudiados es bienvenida a seguir también nuestros intercambios: la transparencia es nuestro método de trabajo, no un riesgo que dominar.

En 1965 Roger Penrose demostró que cuando una estrella masiva colapsa, debe formar una singularidad — un punto donde la gravedad se vuelve infinita y las leyes de la física sencillamente dejan de funcionar. El trabajo le valió el Premio Nobel de Física de 2020, y dejó una pregunta que marcó el resto de su carrera: ¿qué clase de teoría podría describir la realidad allí donde fallan nuestras mejores ecuaciones? Su respuesta, perseguida durante décadas, fue geométrica — bajo el espacio y el tiempo hay estructura, y entenderla exigiría algo más que cómputo.

Kurt Gödel demostró que todo sistema matemático suficientemente rico contiene verdades que no pueden probarse siguiendo las reglas del propio sistema. Y sin embargo los matemáticos humanos pueden salirse de las reglas y sencillamente ver que esos enunciados son verdaderos. Penrose extrajo una conclusión audaz: la comprensión humana no es, en el fondo, seguir reglas — no es un cómputo.

El mecanismo físico que propone para ello se sitúa en el borde especulativo de la física, está discutido, y él mismo lo dice. Lo que importa para esta historia es la puerta que abre: si las mentes pueden captar verdades a las que ningún algoritmo llega, ¿dónde viven esas verdades?

La identidad de Euler — e^iπ + 1 = 0 — no puede ser reinterpretada por un demagogo ni retorcida para justificar una guerra. Su significado está contenido por entero en sí misma: sellado contra la malinterpretación. Platón sostenía que tales verdades — y quizá la belleza, quizá el bien — existen con independencia de nosotros: la mente no las inventa, las descubre.

Penrose toma esa visión en serio hasta el fondo de la geometría del universo. La extensión moral es una hipótesis, no un resultado — pero el núcleo matemático es un hecho llano: algunas verdades no pueden secuestrarse.

Democracia, capitalismo, socialismo, religión, ciencia: ninguno es intrínsecamente bueno ni malo. Están hechos de lenguaje, y el lenguaje es poroso — un régimen puede encarcelar disidentes en nombre de «proteger la democracia», y no existe constante fundamental del universo que desenmascare el abuso. Cuando intentamos llevar un absoluto — justicia, equidad, sentido — a las instituciones, algo se pierde en la traducción: el ideal llega como un «-ismo», un recipiente que santos y tiranos pueden recoger por igual.

Ningún sistema nos salvará por el mero hecho de existir. Todo sistema necesita operadores vigilantes y éticos — y ciudadanos con la disposición a buscar lo que es verdad. Como enseñó Platón, lo único que cualquiera puede hacer es inculcar la disposición a descubrir la verdad.

ROCKR existe para crear un entorno donde inculcar esa disposición — la disposición a descubrir lo que es verdad — sea posible de forma independiente, para cada individuo y cada comunidad. No podemos hacer que una ideología sea intrínsecamente buena; nadie puede. Lo que sí podemos hacer es dar dos pasos a la vez: sacar las promesas que soportan la carga de un sistema del lenguaje secuestrable y llevarlas a las matemáticas, el único medio donde la verdad sobrevive a la traducción — y sacar el propio sistema de las instituciones lejanas y llevarlo a los espacios vivos de la comunidad local. Los cuatro teoremas son el primer paso hecho realidad: las garantías en las que la gente debe confiar — personas reales, presencia real, borrado sin expropiación, una oferta que no puede mentir — enunciadas como matemáticas comprobables por máquina en lugar de como condiciones de servicio (LB 8.1, Antecedentes).

Y la filosofía fija el propósito además del método: una comunidad que selecciona sus propias experiencias en vivo — de todo tipo, de todo género, elegidas de abajo arriba — es un entorno donde la disposición a descubrir lo que es verdad puede crecer. Las subvenciones RUIPA abren ese entorno a todos; los teoremas hacen incorruptible la liquidez que lo sostiene.

No afirmamos que ROCKR sea intrínsecamente bueno; nada construido por personas lo es. Afirmamos que sus garantías están escritas en el único lenguaje que no puede secuestrarse — y que todo lo demás queda, como debe ser, en manos del individuo y de la comunidad.