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 (Monotonicity in the layer depth).
Lean statement: D5/S3/Arith/GoldenResource/EightStepAbundancy.denominator_mono
Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/EightStepAbundancy.denominator_mono (✓ std3). ∎
Citation. Xiaolong Wu (2019). A New Type of Abundant Numbers. DOI: 10.48550/arXiv.1906.05796.
Commentary.
For every natural p and depths a<=b, B(p,a)<=B(p,b). This is finite-sum monotonicity on nested ranges and supplies the denominator comparison in an actual prime-layer exchange.
Theorem 1.3 (Positive prime-layer denominator).
Lean statement: D5/S3/Arith/GoldenResource/EightStepAbundancy.denominator_pos
Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/EightStepAbundancy.denominator_pos (✓ std3). ∎
Citation. Xiaolong Wu (2019). A New Type of Abundant Numbers. DOI: 10.48550/arXiv.1906.05796.
Commentary.
For every prime p and positive depth k, B(p,k)>0. The first layer equals p and every later layer adds a nonnegative natural power.
Theorem 1.4 (The exact multiplicative gain).
Lean statement: D5/S3/Arith/GoldenResource/EightStepAbundancy.layer_ratio_identity
Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/EightStepAbundancy.layer_ratio_identity (✓ std3). ∎
Citation. Xiaolong Wu (2019). A New Type of Abundant Numbers. DOI: 10.48550/arXiv.1906.05796.
Commentary.
For every prime p and positive depth k, (1-p^(-(k+1)))/(1-p^(-k))=1+1/B(p,k), interpreted in the reals. The finite geometric sum gives this identity and hence the exact gain used in actual one-layer abundancy comparisons.
Theorem 1.5 (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.6 (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.denominator_mono - Truth anchor:
D5/S3/Arith/GoldenResource/EightStepAbundancy.denominator_pos - 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 - Truth anchor:
D5/S3/Arith/GoldenResource/EightStepAbundancy.layer_ratio_identity - Dependency: D5/S3/Arith/GoldenLocalThreshold
- Dependency: D5/S3/Arith/GoldenResourceObjectiveFactorization