Running least common multiples: distinct values and multiplicities

Proof sources.

The evidence record fixes the source versions and individual statement associations. These are earlier checks; this revision makes no fresh formal-verification claim.

The general distinct-value assertion and its four word-and-torus arguments are stated as remarks with complete ordinary proofs in Section 5.1; they have no Lean proofs. The source record reports that the general and prime-power subseries arguments were found on 26 September 2026 and checked by a second AI agent, whose corrections were incorporated. It records no human review; the present revision does not constitute a new independent review. No separate literature search for the prime-power subseries theorem at $|P|\ge 3$ is recorded, and no priority claim is made for it. The subseries identities also have ordinary proofs. The program two_tail.py checks their finite instances in exact arithmetic.

For $\{2,3,5\}$ the separate theorem for the sum over distinct values has a Lean proof; its source record says that Comparator had not been run on it. The general affine-block calculation, decoding criterion and finite-set application are also remarks with ordinary proofs; the last additionally uses exact computation. Their formal coverage is restricted to the $\{2,3,5\}$ case with one block and the interval of Section 2. The linear-flow and Smith-factor results likewise have the ordinary proofs printed here; no additional formal coverage is inferred for them.

The two-prime deduction is credited to Fan [17]. Its formal proof assumes the cited Hecke–Mahler value theorem, as specified in Section 14; its algebraic identities are unconditional. The weighted-triangle and shift identities, denominator formula, scaled dichotomy, uniqueness argument, residue limit, strip decomposition and recoding also have written proofs here. Their individual formal associations are retained, without a blanket assertion that every result in the record is formalised. Kernel acceptance uses the standard axioms allowed by the linked checks and is not an independent review of the paper-to-statement correspondence.

The twelve-block enclosure, denominator bound and eight mixed-radix digits have finite exact proofs. The two large exclusions have saved witnesses and exact checkers, and the larger scan has a saved run. None of these finite computations proves the residue inequalities beyond every starting index. No Comparator replay is claimed for the general or subseries arguments.

Artefact and data availability.

The links in the source inventory and to the integer-arithmetic checker open a fixed revision of the repository. The witnesses and exact checkers for the two large numerical exclusions and the saved larger scan are in the large-computation directory. The programs for sums over distinct values recompute the constants of Theorem 1.1 and the certificates of Remark 5.8 in exact rational arithmetic, with two independent computations of the tail intervals, and store their outputs; a fast test checks them against the stored outputs. The same directory checks the finite illustrations of Section 5.1 and the block identity for $\{2,3,5,7\}$.

Funding and competing interests.

This work received no external funding. The author declares no competing interests.

Authorship and review.

Will Cook directed the work. AI agents did most of the research and drafting. Cook has not independently verified every mathematical claim, and these manuscripts have not had independent human mathematical review.

Acknowledgements.

Steve Fan’s forum post of 26 June 2026 supplied the two-prime factorisation and its Hecke–Mahler reduction before this manuscript; it also records the elementary running-LCM identity for finite prime sets [17]. The transcendence input is due to Yann Bugeaud and Michel Laurent and to the earlier work of Loxton and van der Poorten cited by them. The problem numbering and its status as of 28 July 2026 are taken from the Erdős Problems catalogue maintained by Thomas Bloom [4].