First Lean 4 Formalization of the Davenport Constant D(Z_n) and D(Z2 x Z2): native_decide Certificates with EGZ Bridge (Rei-AIOS Paper 128)

This article is a re-publication of Rei-AIOS Paper 128 for the dev.to community. Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.19687156 Internet Archive: https://archive.org/details/rei-aios-paper-128-1776810422866 Harvard Dataverse: https://doi.org/10.7910/DVN/KC56RY GitHub source (