Machine-checked audit of an accumulation–release hypothesis: five findings that follow from a Lean 4 formalisation, with an open-licensed figure corpus for the Cambrian small-shelly record

Abstract. We formalise, in Lean 4 (core library only), the logical structure of a pair of manuscripts that argue for a global accumulation–release transition at the Ediacaran–Cambrian boundary, and a companion Airy/fold-scaling model of punctuated equilibrium. The formalisation is deliberately discrete and exponent-level: it does not prove the analytic theorems, but it decides, with the kernel, five structural claims that determine whether the empirical argument can succeed. Three of them weaken the argument as published: the rate-dependence prediction is an assumption wearing the costume of a theorem; criterion C3 fails on the authors’ own reported numbers; and C1–C4 are kinematic and cannot distinguish an internal topological release from an external trigger. The remaining two are positive constraints: the release magnitude is bounded by the number of Morse events, and the “topological protection” claim is conditional on a regularity hypothesis that is never tested empirically. We also ship an open-licensed figure-harvesting pipeline (CC-BY 4.0, per-figure sha256 and provenance) and document why PLOS alone cannot supply the same-clade pre/post comparison the theory requires.