Lean 4 formalisations accompanying research papers by Murad Farzulla.
This repository was audited in August 2026. Two defects were found, and both are corrected
here. Anyone who encountered an earlier version of this repository, the Zenodo deposit
10.5281/zenodo.21315611 (v2.0.0, 11 July 2026), or the release v4.27.0 should read this
section, because those copies state things this one withdraws.
1. The AxiomOfConsent module formalises a functional that has since been retracted.
The module's central definition is friction σ α ε = σ(1+ε)/(1+α). That closed form was
retracted on 30 July 2026. It is not the first-order expansion of expected delegation
regret about the origin under any data-generating process, and no affine reparameterisation
makes it one. Specifically: there is no first-order term in ε — the expansion has a
Θ(√ε) cusp at 0⁺ with infinite right-derivative and a discontinuity at exactly ε = 0,
and its sign is belief-model-dependent. The α effect is not identified by the design, since
E[G](α) = E[G](−α) is an exact distributional identity. The σ result is degree-1
homogeneity, which is a units identity rather than a comparative static.
The theorems in that module remain valid statements about that formula. Lean did not fail.
What was wrong was the mapping from those theorems to claims about the world, and the
mapping is what has been withdrawn. Affected declarations are marked in
FarzullaProofs/AxiomOfConsent/ and in that module's PaperMap.md.
2. The previous depth tiering and theorem count implied substance the library does not have.
Earlier versions of this file advertised "269 machine-checked theorems" and assigned the
label gold-formal-core to 15 of 16 modules. An adversarial triage that read the proofs
rather than the statements found that the large majority of those theorems unfold a
definition and close by linarith, ring or simp; roughly two thirds have proof bodies
of two lines or fewer, and the longest proof in the library is 19 lines. The tier labels
were self-assigned — twelve modules were promoted to gold on a single day — and the
verification tool that "checked" them compares status strings across four files. It
verifies that labels agree with each other. It has never verified depth.
Nine modules have been moved to archive/ and are no longer built or
claimed. The tier vocabulary has been withdrawn and replaced with a plain description of
what each module proves.
It is a formalisation of the definitions and elementary algebra of the accompanying papers, machine-checked against Mathlib. That is a real but modest thing, and it is worth being exact about its two boundaries:
- 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.
- Zero
sorryis not the same as no unproven assumptions. Several modules rest on modelling assumptions that Lean neither verifies nor can verify; these are tracked inASSUMPTIONS_LEDGER.mdand restated at point of use.
The library is unreviewed in the peer-review sense. It should be cited as a reproducibility-and-coherence artifact, not as independent evidence for any paper's substantive claims.
Current scope: 10 modules, 190 theorems, zero sorry, zero axioms beyond
propext / Classical.choice / Quot.sound (Lean 4 v4.27.0, Mathlib pinned to v4.27.0).
| Module | Paper | Status | What the Lean proves | Thms |
|---|---|---|---|---|
AgonismEndogenisation |
Optimal friction dose (note in preparation) | definitional-algebra-assumption-carried | Minimisation of a scaled parabola, and an argmin-invariance result. Carries two stated modelling assumptions. | 23 |
AxiomOfConsent |
The Axiom of Consent (arXiv:2601.06692) | retracted-functional | Monotonicity and bounds for σ(1+ε)/(1+α). Functional retracted — see above. |
28 |
ROM |
The Replicator-Optimization Mechanism (arXiv:2601.06363) | definitional-algebra | Row-stochastic mass conservation, simplex invariance, skew-symmetry of an RPS payoff matrix, monotonicity of L/(1+F). |
25 |
IdentityThesis |
Identity is Irreducibly Relational | definitional-algebra | Set-theoretic encodings (von Neumann vs Zermelo), complex-arithmetic facts, and an equivalence that holds by definition. | 22 |
Common |
shared infrastructure | (untracked) | Transfer/adversarial skeletons and optimisation/dynamics utilities. Several instantiate tautologically. | 20 |
ConsensualSovereignty |
Consensual Sovereignty | definitional-algebra | Bounds on a stakes-weighted mean. | 19 |
RegimeTenure |
When Suppression Fails (ROM legitimacy carve) | definitional-algebra | Comparative statics of C₀/b. The first-passage identity itself is proved by hand in the paper and is not formalised. |
16 |
GenreMimicry |
Genre Mimicry | definitional-algebra | Monotonicity of d/t and p/(1−p). |
14 |
SemanticVision |
Semantic Vision | definitional-algebra | Jaccard index bounds and symmetry on Finset. |
12 |
ROMEthics |
ROM ethics bridge | definitional-algebra | b − w·h, and its image under L/(1+F). One theorem depends on the retracted friction functional and is marked. |
11 |
Nine further modules are archived and excluded from all of the above:
CBDCPrivacy, AsymptoticProtection, AutonomousRedteam, AMLParadox, MonographQualia,
ConsciousnessNominalisation, QuantumOscillatory, Common/Probability,
Common/Relations. See archive/README.md for what each one actually
contained and why it was pulled.
The whole module formalises the retracted functional. Within it, these declarations were previously presented as verified results about coordination and are withdrawn as such:
| Declaration | Was presented as | Disposition |
|---|---|---|
friction_strict_anti_alignment |
F strictly decreasing in alignment | Withdrawn. The alignment effect dies on identification, not on sign. |
friction_strict_mono_entropy |
F strictly increasing in entropy | Withdrawn. Non-monotone under every belief model tested. |
friction_at_perfect_alignment |
F(σ,1,0) = σ/2 | Withdrawn with the σ/2 baseline. The real floor is the quantization floor, alignment-dependent, and exactly zero at ρ = −1/3. |
friction_ge_half_stake |
Global lower bound F ≥ σ/2 | Withdrawn, same reason. |
friction_unbounded |
F diverges as α → −1⁺ | Withdrawn. Downstream of the retracted signed denominator. |
friction_strict_mono_stake, friction_stake_linear |
F increasing/linear in stakes | Units identity, not a comparative static. Also subject to an unresolved raw-vs-dimensionless normalisation question. |
friction_zero_of_stake_zero, stake_zero_of_friction_zero, friction_eq_zero_iff, friction_pos |
zero-friction iff zero-stakes | Statement retained, proof retired. The result survives on a quantization/deadband argument that is not the one formalised here. |
The quadratic variant friction_quad* is a formal variant only. Its original empirical
motivation was withdrawn earlier as a sign-blind DGP artifact; that is a separate and older
retraction, and should not be mistaken for this one.
rps_not_potential states that rps_payoff 0 1 ≠ rps_payoff 1 0, which after simp
is -1 ≠ 1. It is an asymmetry witness for one payoff matrix. The library defines no
potential function and no potential game, so the declaration name overstates what is
proved and should be read as the arithmetic fact it is. The same applies to
skew_symmetric_nonzero_not_potential.
curl https://elan.lean-lang.org/install.sh -sSf | sh # if elan is not installed
lake exe cache get # pre-built Mathlib oleans
lake buildArchived modules are outside the FarzullaProofs library target and are not built.
tools/verify_papermap_refs.py # mapping -> declaration existence
tools/verify_claims_consistency.py --report reports/paper_verification_report.md
make verifyBoth tools check consistency of metadata: that declarations named in a PaperMap.md
exist, and that status strings agree across files. Neither assesses whether a proof does
any work. A PASS from make verify means the bookkeeping is coherent. It is not an audit.
@software{farzulla2026leanformalizations,
author = {Farzulla, Murad},
title = {{FarzullaProofs}: Lean 4 Formalisations of Definitions and Elementary Algebra},
year = {2026},
version = {3.0.0},
url = {https://github.com/dissensus-ai/lean-formalizations},
note = {Lean 4 v4.27.0. Supersedes v2.0.0, which contained a retracted functional
and withdrawn depth claims.}
}Do not cite v2.0.0 (10.5281/zenodo.21315611). It is superseded for the reasons in
Read this first.