R-Gen

An engineering firm does work, a qualified reviewer checks it, and the approval becomes part of the record. R-Gen models that sequence on chain.

A claim is the work. It records what was done, the definition and standard it is judged against, the quantity, the deadline, and any comments or value-proposition reference.

A validation is the reviewer’s judgement. It records quality, the evidence, and the credential that made the reviewer qualified to sign.

A K-Asset is the approved pair. It keeps the claim, the validation, the credential, the adjudication, and the provenance together as one asset.

That is the point: the engineering business can put its work, sign-off, and dispute record on chain, and the asset carries that history. The core does not price the work, pay it, or score it; those are extensions.

The model comes from Dan Robles’ CoEngineers and Ingenesist Project. The papers start with a problem: the value of engineering is invisible because almost nothing records the judgement about the work.

The papers are the only published suite that sets out this model end to end. There is no other coherent body of thought on how engineering work should be accounted for on a shared ledger. That is why I invested in CoEngineers in 2017 and why I have stayed with it.

A load calculation shows the problem. The calculation is the claim; a second engineer checks the assumptions and signs it; their credential makes the signature count. Today the calculation, the check, and the fee sit in different systems, so the record cannot say who checked it, against which version, or what happened in a dispute.

Each primitive is traceable to a paper quote and page, a Rholang implementation, a Lean theorem, and a suite or corpus row. The matrix is docs/src/reference/paper-to-code.md. The papers are third-party copyrighted reference material; the contracts, model, and book are original work.

Seven contracts cover the flow: root, identity, credentials, claim, value proposition, oracle, provenance. The claim holds the work, criteria, quantity and definition, comments, and value-proposition reference; validation creates the K-Asset; the oracle holds one credentialed adjudicator and executes through the subject’s private applyDecision capability.

Pareto here is a removal test: take a primitive out; if the rest can still express a claim, a validation, and a K-Asset, it was an extension, not core. That leaves seven contracts, with no cycles. The core mints and transfers nothing and has no R-Cash dependency. Pricing, payments, risk scoring, panels, governance, handles, metrics, and the client consume the core’s facts; the core does not call them.

A linear cell is state that a contract consumes, checks, and puts back exactly once. A second operation sees the new state and refuses, so two operations cannot both read the same state and both commit. Independent entities do not share a mutable cell. Identity creation and credential issuance are the only serialization points. Oracle cases receive the subject’s private applyDecision capability, so a decision cannot be applied to another K-Asset.

The Lean model proves the general result: no two events on one cell in any run expect the same version, and every arm’s decision comes from the cell it consumed. The proof is over the model, not the deployed Rholang.

A 32-pair matrix records the outcome for every pair of arms. Nineteen pairs are exclusive: whichever runs first, the second refuses. Twelve are ordered: one direction refuses, the other is the legal serialized order. One is independent. Every pair names the theorem that covers it, and a check script verifies the mapping.

On 4 November 2026, against Rholo node e2d073d, the seven-contract core installed on a fresh isolated devnet. Ten behavioural suites passed, from identity and credentials through claim, K-Asset, value, oracle, provenance, integration, a core vertical slice, and the race regression, with 291 passing assertions.

The Lean project builds 36 files without Mathlib. The audit covers 131 public theorems and reports only propext and Quot.sound; there is no sorry, admit, native_decide, or declared axiom. The flow manifest maps 66 arms: 35 proved-model, 0 proved-conformance, 31 owed. Proved-model means the theorem is about the model. Proved-conformance would tie a deployed arm to an emitted row and a passing suite; none is claimed. The model emits 21 corpus rows. The adversarial review records four P0 defects in the legacy 12-term prototype and their removal.