LeanDFumt: An Open-Source Eight-Valued Logic Library for Lean 4

Abstract

Self-contained, Mathlib-free Lean 4 library implementing the Rei-AIOS D-FUMT8 eight-valued logic {TRUE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF}. 29 zero-sorry theorems via decide / native_decide on the finite type. Three classical-logic bridges (toBool, toTernary, asProp with Decidable instance). Builds in ~5 seconds on a fresh clone — two orders of magnitude faster than Mathlib-dependent projects. Apache-2.0 licensed at github.com/fc0web/lean-d-fumt8 (v1.0.0). Library-only strategy (purely additive, no kernel changes, full Mathlib compatibility). Completes the proof-theoretic anchor for D-FUMT8, complementing the Schnorr-randomness ceiling (Paper 69) and the QuTiP quantum-operational floor (Papers 75–76). To our knowledge, this is the first publicly released eight-valued-logic library for Lean 4.