Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A392096 Divisor-Pair Sigma Bounds

Abstract

Hoft’s consecutive divisor-pair condition forces a strict abundancy interval.

Definition 1.1 (Consecutive gap-separated divisor pairs).

Formalization. D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.DivisorPairs (✓ std3).

Source. Repository-derived.

Commentary.

For natural D and q, DivisorPairs is a structure with fields D_pos, count, count_ge_two, lower, upper, lower_zero, upper_last, divisors_eq, within, and gap_succ. The first three fields make D positive and provide at least two pairs. The next four give the two natural-valued enumerating maps, start lower at one, and end upper at q.

The divisors_eq field says that Nat.divisors(q) is exactly the union of the images of lower and upper over range(count). The within field says lower(i)<upper(i)<Dlower(i). The gap_succ field says Dupper(i)<lower(i+1) between successive pairs. The expression count-1 uses truncated natural subtraction.

This is the divisor characterization stated by the OEIS A392096 entry. The positivity field is automatic at the Member scale D=2^(m+1), but is explicit so the general structure records every order argument used below.

Definition 1.2 (Membership in the divisor-form version of A392096).

Formalization. D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.Member (✓ std3).

Source. Repository-derived.

Commentary.

A natural n is a Member exactly when natural m and q exist with m at least one, q odd, n=2^m*q, and nonempty divisor-pair data at D=2^(m+1). The conjunction is right-associated exactly as in the Lean definition.

OEIS A392096 attributes this divisor characterization to Hartmut F. W. Hoft. The entry asserts that it is equivalent to the symmetric-representation width pattern 1,2,1,0,…,0,1,2,1. This module formalizes only the displayed divisor predicate. The asserted equivalence is ASSUMED-UNVERIFIED and is not formalized here.

Theorem 1.3 (Least-prime bound and square exclusion).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.divisor_pairs_minFac_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For odd q with DivisorPairs data at scale D, the least prime factor minFac(q) is strictly below D and its square does not divide q. The least prime occupies the first upper position, while its square would have to occur after it and would violate the next separation gap.

Theorem 1.4 (Every divisor pair has least-prime ratio).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.divisor_pairs_upper_pair_shape (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every index below count, the upper divisor is minFac(q) times the paired lower divisor. The proof uses divisor location, least-prime coprimality, and the separation gaps; it is a public prerequisite of the telescoping estimate and the final theorem.

Theorem 1.5 (The divisor gaps telescope strictly).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.divisor_pairs_gap_telescoping (✓ std3). ∎

Source. Repository-derived.

Commentary.

For odd q with DivisorPairs data, summing the successive gaps gives (D*minFac(q)-1)S < DminFac(q)*r, where S is the sum of the lower entries over range(count) and r is the last lower entry. This repository-derived estimate is used directly by the final upper sigma bound.

Theorem 1.6 (Lower coefficient comparison).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.lower_coefficient_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For natural D and p with p<D, the product Dp is at most (D-1)(p+1). This named coefficient estimate is a direct public prerequisite of the final strict lower sigma bound.

Theorem 1.7 (Upper coefficient comparison).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.upper_coefficient_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For natural D and p with D at least four and p at least three, three times (D-1)(p+1) is at most four times (Dp-1). This named coefficient estimate is a direct public prerequisite of the final strict upper sigma bound.

Theorem 1.8 (Division-free natural sigma bounds).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.a392096_sigma_bounds_nat (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n satisfying Member, twice n is strictly below ArithmeticFunction.sigma(1,n), and three times that divisor sum is strictly below eight times n. This is the division-free natural-number companion to the source-form rational bound.

The proof lets p be minFac(q). Divisor location and the gap conditions force p<D, exclude p^2 dividing q, and identify every upper(i) as plower(i). Summing the successive gaps gives (Dp-1)S<Dp*r, where S is the sum of all lower entries and r is the last one. This estimate and S>r yield the two strict bounds after sigma multiplicativity.

Theorem 1.9 (Strict sigma bounds for every divisor-form member).

Proof. Machine-checked in Lean as D5/S3/Factorization/SymmetricSigmaRepeatedPatternAbundancy.a392096_sigma_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n satisfying Member, the conclusion over the rationals is written in the source’s own form: 2n<sigma(n)<8n/3. It follows from the division-free natural theorem by casting both inequalities and dividing the upper inequality by three.

This is a repository-derived conditional theorem. Its hypothesis is the divisor-form Member criterion transcribed from the OEIS A392096 comment by Hartmut F. W. Hoft dated 2025-12-30; the comment’s symmetric-representation width-pattern equivalence is only scope-matched context, is ASSUMED-UNVERIFIED, and is not formalized. No claim is made for a number unless the divisor-form Member predicate has been supplied.

References