🔧 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.
The canonical version with full reference list is in the permanent archives below:



Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.19687156


Internet Archive: https://archive.org/details/rei-aios-paper-128-1776810422866


Harvard Dataverse:...