Invariant Density and Bounded Derivability in Finite Equational Presentations

This paper introduces invariant density, a syntactic measure for finite equational presentations based on bounded derivability. The framework is explicitly bounded, decidable, and terminating for fixed parameters, but intentionally incomplete. It formalizes invariant sets, proves monotonicity properties, and shows how redundancy elimination increases invariant density without loss of bounded invariants. A reference implementation realizing the definitions and algorithms is archived separately on Zenodo and publicly available. 10.5281/zenodo.18441678 An appendix documenting a reference implementation snapshot is included for reproducibility. This work is part of a broader suite developing invariant density across syntactic, formal, and semantic contexts. The present paper focuses on bounded derivability in finite equational presentations. Complementary works in the suite address geometric formulations, general syntactic frameworks, algebraic semantics, and proof assistant realizations (including Coq), each archived separately on Zenodo: https://doi.org/10.5281/zenodo.18265909 (geometric formulation)https://doi.org/10.5281/zenodo.18301563 (syntactic framework)https://doi.org/10.5281/zenodo.18301522 (algebraic semantics)https://doi.org/10.5281/zenodo.18301480 (proof assistants)