FarzullaProofs: Lean 4 Formalisations of Definitions and Elementary Algebra

Version 3.0.0 supersedes version 2.0.0 (10.5281/zenodo.21315611). Do not cite v2.0.0. It contained a retracted functional and depth claims that have since been withdrawn. Both are described below. 1. Retraction. The AxiomOfConsent module formalises 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. 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, a units identity rather than a comparative static. The theorems remain valid statements about that formula — Lean did not fail. What is withdrawn is the mapping from those theorems to claims about coordination, and with it the previous “12/12 match” claim. 2. Withdrawn depth claims. Version 2.0.0 advertised “246 machine-checked theorems” and assigned the label gold-formal-core to nearly every module. An adversarial triage that read the proofs rather than the statements found that the large majority 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, and the tool that checked them compared status strings across files rather than assessing depth. The tier vocabulary has been withdrawn. Nine modules have been moved to archive/ and are no longer built or claimed: CBDCPrivacy, AsymptoticProtection, AutonomousRedteam, AMLParadox, MonographQualia, ConsciousnessNominalisation, QuantumOscillatory, and the Probability and Relations files of Common/. Each defined an elementary arithmetic operation and proved standard facts about it under domain vocabulary that never entered a single statement. See archive/README.md for the per-module account. What this library is. A formalisation of the definitions and elementary algebra of the accompanying papers, checked against Mathlib. Lean checks that the proofs follow from the stated definitions. It does not establish that the definitions are faithful renderings of the constructs in the papers, and for the shallower modules they plainly are not. Zero sorry is not the same as no unproven assumptions: several modules rest on modelling assumptions that Lean neither verifies nor can verify, tracked in ASSUMPTIONS_LEDGER.md. The library is unreviewed in the peer-review sense, and should be cited as a reproducibility-and-coherence artifact rather than as independent evidence for any substantive claim in the papers. Scope (v3.0.0): 10 modules, 190 theorems, zero sorry, no axioms beyond propext / Classical.choice / Quot.sound (Lean 4 v4.27.0, Mathlib pinned to v4.27.0). Build clean, 7917 jobs. Repository: github.com/dissensus-ai/lean-formalizations (archived here at commit 8e113333bf461b0396ba44267f64320ef9f974bb).