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

246 theorems across fifteen 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,938 jobs, and a grep across all non-cache .lean files finds no sorry, no custom axioms and no native_decide. Those figures agree with the repository's own description.

A sixteenth module on optimal friction dosing, twenty-three further theorems, is committed on a local branch and not pushed, so the public repository and all current site copy describe the smaller version. The 246 figure goes stale the moment that branch lands.

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.