FarzullaProofs — Lean 4 formalisations

Anyone refereeing or extending the Axiom of Consent friction functional, the Replicator-Optimization Mechanism, or the regime-tenure law can go from an equation in a PDF to the checked Lean statement in one step, and read off which side conditions the result needs. Each module ships a PaperMap linking manuscript theorem identifiers to Lean declarations. The ROM modules also ship as arXiv ancillary files with arXiv:2601.06363.

For readers who do not use Lean, the assumptions ledger is probably the more reusable artefact: an explicit inventory of the side conditions and modelling assumptions each result is conditional on, including, in one module, a statement of where the model leaves its own valid domain. The proofs are elementary and readable, so the repository also works as a worked example of formalising an applied paper's algebra with Mathlib.

What is in the repository

190 theorems across ten paper modules plus a shared Common library, on Lean 4 v4.27.0 with Mathlib at the matching revision. The build was checked by running it rather than by reading the README: lake build returns exit 0 on 7,917 jobs, and a grep across all non-cache .lean files finds no sorry, no custom axioms and no native_decide.

The earlier figure on this page was 246 theorems across fifteen modules, with the caveat that it would go stale the moment the unpushed optimal-friction-dosing branch landed. That branch landed on 25 August 2026, in the same push as an audit that cut rather than added: nine modules moved to archive/, where they are neither built nor claimed. The counts moved down, not up.

What the count does not tell you is depth, and the honest figure there is much smaller. Roughly two thirds of the proofs in the library have bodies of two lines or fewer, and the longest proof is nineteen lines. Treat the theorem count as a statement about coverage, not about difficulty.

Depth is uneven, and the headline count flattens that

Roughly six modules formalise named propositions from the manuscripts. The rest formalise simplified algebraic stand-ins. The module named for the 33k-word consciousness monograph defines qualia distance as the absolute difference of two reals and proves non-negativity, self-distance zero and symmetry, which are the standard properties of absolute value. The CBDC privacy module models privacy composition as additive epsilon accounting closed by ring. Neither formalises the argument of the paper it is named after.

The Bronze, Silver and Gold tier labels advertised in the README no longer discriminate between these cases: the coverage file now marks every module as gold. The promotion commits flipped the label by adding a roughly forty-line file of four further elementary theorems, so the label moved and the depth did not.

Everything in the library is elementary algebra over the reals, Finset and the complex numbers. There is no measure theory, no topology and no continuous dynamics anywhere in it; results described as dynamics are discrete algebraic identities, not statements about differential equations or their convergence.

What machine-checking does and does not buy

Lean checks that the proofs follow from the stated definitions. It does not establish that the definitions are faithful renderings of the papers' constructs, and for the shallower modules they plainly are not. The library is unreviewed in the peer-review sense.

One concrete example of the gap: the regime-tenure first-passage identity is proved by hand in the paper and is not formalised at all. Only the comparative statics around it are machine-checked.