bibkey: mian2026lcm10000 authors: “Ibrahim Mian; Shayaan Siddique” year: 2026 title: “Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of Z Has lcm Exceeding 10000” doi: null url: https://arxiv.org/abs/2607.25628v1 claim: “Every finite covering of Z by distinct odd moduli greater than one has least common multiple greater than 10000.” strata_touched:

• D5/S3/Arith/Congruence/TwoOddPrimeUncoveredDensity license: Apache-2.0 triage: anchor

Kernel-checked finite lcm exclusion

Locator: arXiv:2607.25628v1, published 28 July 2026. The paper and source repository were read 16 September 2026. The source is ibrahimmian36/centurion at commit b513de2f7b9526e85ea6d760d4415a977f9a2c6b; the repository is Apache-2.0. The downloaded arXiv PDF SHA-256 is 8c1273d20e56449ed7a0d8276893eacf2db1c2ee65f24eb5f456e223474db24f and the source archive SHA-256 is ed6bc4c35a4071ef729325841b736c59e718cc96efa36763dc93668cfd703a00.

The source theorem odd_covering_lcm_gt_10000 has the exact hypotheses n : ι → ℕ, a : ι → ℤ, [Fintype ι], 1 < n i, Odd (n i), Function.Injective n, and ∀ x : ℤ, ∃ i, (n i : ℤ) ∣ (x - a i). It concludes 10000 < Finset.univ.lcm n. The transported theorem Erdos7.FC.fc_odd_strictCoveringSystem_lcm_gt_10000 targets the official StrictCoveringSystem ℤ formulation.

The proof is kernel-checked Lean 4.30.0 code. It combines the density implication 2N ≤ σ₁(N), the odd abundancy floor at 945, 23 finite CRT capacity certificates below 10000, and a kernel-checked enumeration of all odd non-deficient candidates. The first candidates not excluded by that finite certificate are 10395, 12285, and 17325. The source reports 63 published theorems with axiom closure exactly [propext, Classical.choice, Quot.sound], with no sorryAx, native-decide axiom, or solver in the trusted base. This repository records the published result as a citation-only boundary; it does not add a duplicate Lean wrapper. The upstream GitHub Lean Action CI run 33831024928 completed successfully for the pinned source commit.

The result strengthens the finite search boundary for Erdős #7 but leaves all lcm values at least 10395 and the unrestricted problem open. Its capacity certificate method is independent of the sparse-tail block estimates in the problem dossier.