Assembly.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The unconditional eventual covering bound, using the actual prime-congruence and local affine Gaussian-position producers. Conditional intermediate interfaces retain their stated hypotheses and are not used as unproved assumptions here.

theorem OAI.SingleLatticeCovering.Assembly.eventual_single_lattice_covering line 19