Reading Eight Erdős Problems Together

Verification and sources

The starting point is the sparse perturbation construction accompanying Erdős Problem #251 in this repository, especially its short paper and ResidueFeedbackCore.lean. The latter already proves residue-dependent selection and an abstract infinite sum endpoint. An operator-supplied review supplied the form of Lemma 3.4, the sharp exponential support constants, and the linear/superlinear factorial contrast. Those ingredients are credited to that review, not presented as discoveries of this paper. The extensions developed here are the exact capacity criterion on arbitrary strict integer divisibility chains, the factorial support classification and its integer-exponent comparison, the common-divisor formulation, and the derivative dimension and rationality thresholds proved above.

The derivative theorem combines residue feedback from #251 with the treatment of factorial carries in #68. Identity (J) interprets a carry as multiplication by a polynomial vanishing at the evaluation point. This produces the independent higher derivative instead of assuming its availability. The moving coordinates in (T) make the full-dimensional critical construction possible; the counting obstruction proves its measure is zero. Conversely, division by the same vanishing polynomial preserves integer factorial coefficients and eventual divisibility. The complementary tail formula then proves rational-derivative rigidity at precisely the same threshold. These are explicit transfers between representations, not evidence for a general improvement in automated discovery. The other programmes motivated comparison of rank, arithmetic and analytic obstructions; their endpoints are not premises here.

Hurwitz functions and interpolation by vanishing polynomials are classical. Waldschmidt’s survey [42] describes growth and multipoint derivative questions. Here we fix a polynomial bound on the integer Taylor coefficients and study the dimension and interior of a finite real derivative image, as well as rationality of finitely many derivatives under eventual coefficient divisibility. This last hypothesis is restrictive: it is not an unrestricted rational-value theorem for Hurwitz functions. For the classical scalar dimension formula, see Wegmann [43], who credits Šalát. Our additional task is to separate a joint derivative image after several carry constructions have been added. Neither the definition of a Hurwitz function nor the mass-distribution argument is new. The precise dimension formula and the two sharp thresholds are proved here; historical priority remains unestablished.

Airey, Mance and Vandehey already use digit sets eventually divisible by every fixed integer while retaining asymptotically full digit entropy [41]. Their theorem concerns normality and Hausdorff dimension for chosen Cantor bases. Here a fixed divisibility chain and arbitrary summable allowances are given, and the conclusion distinguishes interval filling from nullity and meagreness. These are elementary arguments in the classical theory of Cantor series and achievement sets; historical novelty of the exact classification is not established. Classical interval covering is background, rather than a contribution claimed here. A literature comparison and the reproducible checks are recorded in the accompanying research record. The work was developed with AI assistance and mathematical cross-checking by separate agent passes; that does not constitute independent expert review.

The formal module CongruenceInterpolation.lean uses the existing feedback module and states the common-divisor obstruction for a real carry recurrence. The analytic identification of that recurrence with the Cantor series, and the capacity and support classifications, are the ordinary proofs above. The module FeedbackContinuation.lean reuses the existing interval-feedback endpoint and proves eventual individual and cumulative divisibility from nested cofinal moduli; choosing the moduli and continuation intervals remains part of the ordinary proof. See the research record for the exact build status and source revision. No claim about any of the eight Erdős programmes changes; in particular factorial denominators $n!$ here are not $n!-1$ from #68.

The accompanying module FactorialJet.lean checks the finite factorial-carry identity and its first weighted version, including endpoint terms, and preservation of divisibility. It does not formalise Theorems 2.1 and 2.2, their limits or dimension proof. The exact-arithmetic script jets.py checks the formulas at specified finite degrees, both quotient formulas, and independently checks the uniform tail majorant in (T). These finite degree tests are not the proof for every $d$.

The capacity criterion already covers non-power and oscillating allowances.