Invariant Density in Proof Assistants: Application to Coq for Redundancy Elimination

This work demonstrates invariant-preserving redundancy elimination in algebraic axiomatizations inside Coq, using explicit proof objects. It targets proof engineering and library design rather than automation or foundational minimality. Version 2. This version expands the paper beyond a single illustrative case, adding multiple invariant-preserving examples (including group presentations via Tietze transformations) and strengthening the formal framework to be self-contained. Core claims and scope remain unchanged. This paper is part of a broader research program on invariant density across syntactic, semantic, and formal systems. The present work instantiates invariant density within proof assistants, demonstrating invariant-preserving redundancy elimination via explicit proof witnesses in Coq. Related papers in the suite develop geometric, syntactic, algebraic, and equational formulations of invariant density, each available as separate Zenodo records. 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.18404261 (bounded derivability, equational presentations)