Eight-Step Abundancy Maximum
Abstract
The unique largest abundancy at eight prime factors counted with multiplicity is attained by 180180 and equals 224/55.
Definition 1.1 (Prime-layer denominator).
Formalization. D5/S3/Arith/GoldenResource/EightStepAbundancy.layerDenominator (✓ std3).
Citation. Xiaolong Wu (2019). A New Type of Abundant Numbers. DOI: 10.48550/arXiv.1906.05796.
Commentary.
D(p,k) denotes layerDenominator p k. It sums p to the powers one through k, with an empty sum at k = 0. For a prime p and a positive layer k, the multiplicative abundancy gain is 1 + 1/D(p,k).
Theorem 1.2 (The strict eighth-layer boundary).
Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/EightStepAbundancy.eight_step_layer_cutoff (✓ std3). ∎
Citation. Xiaolong Wu (2019). A New Type of Abundant Numbers. DOI: 10.48550/arXiv.1906.05796.
Commentary.
The eight events, in denominator order, are (2,1), (3,1), (5,1), (2,2), (7,1), (11,1), (3,2), and (13,1). Their denominators are 2, 3, 5, 6, 7, 11, 12, and 13.
The equivalence quantifies over every prime and every positive layer. Every excluded event has denominator at least 14. The proof first excludes all depths at least three by comparison with 2 + 4 + 8, then classifies the remaining prime bases.
Theorem 1.3 (The unique eight-step maximizer).
Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/EightStepAbundancy.eight_step_abundancy_optimum (✓ std3). ∎
Citation. Xiaolong Wu (2019). A New Type of Abundant Numbers. DOI: 10.48550/arXiv.1906.05796.
Commentary.
Here omega(n) is the sum of n’s prime exponents, equivalently Mathlib’s cardFactors n, and Z(n) is sigma(1,n)/n as a real number. The competitor ranges over every positive natural number with omega(n) = 8, without a bound on n or its prime factors.
The proof applies the existing local threshold theorem at the two prices log(15/14) and log(14/13). Equality at their midpoint forces equality of each exponent. The existing objective factorization then sums the local comparisons over the union of the two finite prime supports; the equal eight-step costs cancel.
The theorem includes the exact values, both eight-step counts, and 180180 = 2^2 * 3^2 * 5 * 7 * 11 * 13. The comparison with 5040 concerns abundancy at fixed step count. It does not assert a comparison for an objective penalizing integer size.
References
- Truth anchor:
D5/S3/Arith/GoldenResource/EightStepAbundancy.eight_step_abundancy_optimum - Truth anchor:
D5/S3/Arith/GoldenResource/EightStepAbundancy.eight_step_layer_cutoff - Truth anchor:
D5/S3/Arith/GoldenResource/EightStepAbundancy.layerDenominator - Dependency: D5/S3/Arith/GoldenResourceObjectiveFactorization