Centered reduced residue progression maximum

Let n be even and squarefree with at least three distinct prime factors. Let p be its greatest prime factor and put d=n/p. Under d<2p, determine the longest positive-step arithmetic progression in the fixed centered reduced residue system from -n/2+1 through n/2.

The unnumbered conjecture on printed page 14 of the cited paper states that the maximum length is floor(p-2p/d). The formal target expresses the maximum as an IsGreatest statement, so it requires an attaining progression and a bound for every positive step, together with the exact rational-floor equality.

The conjecture gives a closed formula for a maximum over all starts and all positive steps in a source-fixed representative system. Its hypotheses couple the distinct prime factors of a squarefree modulus to the geometry of the centered interval.

The cited paper presents the statement as a conjecture. The checked repository and pinned Mathlib contain prime-factor, squarefree, modular, gcd, and floor components, but no theorem with this centered progression maximum. The project handoff at issue 7333 records the arithmetic route and releases it unclaimed; issue 8677 identifies this exact source statement. These locators establish the project provenance and do not support a priority claim.

Write n=dp=2ep. Squarefreeness and maximality give odd e>=3, prime p>=5, and gcd(d,p)=1. A progression of the predicted length is obtained with step d and start p(2-e)+d; endpoint inequalities follow from the nonzero remainder of 2p modulo d, and prime-divisor analysis proves every term is a unit modulo n.

For an arbitrary positive step, if some prime factor of d is absent from the step, a complete residue sweep supplies the upper bound. If the step is a multiple t*d with t>=2, the centered interval diameter supplies it. For step d, the unique centered multiple of p in the starting residue class cannot be crossed; its two endpoint margins give the same bound. The positive remainder then converts the natural quotient to floor(p-2p/d).

An even squarefree modulus in the stated domain with an admissible progression longer than the formula, or with no progression attaining it, would refute the maximum statement. A mismatch between the rational floor and the natural quotient expression would refute the second conjunct.

The Lean module is D5/S3/ArithUnits/CenteredReducedResidueProgressions.lean. Its result theorem derives the complete factorization facts from the source hypotheses, constructs the lower progression, proves the three exhaustive upper cases, and proves the rational-floor identity without additional public assumptions. The canonical freeze records module identity e61fb1dce201b59f0aa8d8428428c8d232a37885503018230857905b33a8123b and result statement identity ed91b7bf43b9864cca5816d00ba09b81ed5b209556c21e13b8f0c7ec5744df16.

theorem; resolution kind proved for every modulus satisfying the literal source domain. The calibration n=30 is an instance of the theorem, not a premise. The result theorem node carries the typed Proved claim for this problem slug.

Literature completeness outside the cited paper and the bounded searches is unverified. No exhaustive novelty or publication-priority claim is made. The source reading and project handoff locators are attributed evidence.