Maximum Length of a Two-Dense Divisor Block

Abstract

The largest two-dense divisor block has ruler-scaled maximum odd count.

Both statistics use the complete increasing list of positive divisors and its actual maximal splitBy blocks. An adjacent pair a,b stays joined exactly when b is at most twice a. Equality and singleton blocks are retained. The theorem includes every positive natural n.

Definition 1.1 (Odd counts in the actual blocks).

$$\forall n:\mathbb{N},\mathrm{oddBlockCounts}(n)=\mathrm{map}((B\mapsto \mathrm{length}(\mathrm{filter}((d\mapsto \mathrm{decide}(\mathrm{Odd}(d))),B))),\mathrm{splitBy}((ab\mapsto \mathrm{decide}(b\le 2\cdot a)),\mathrm{map}(\mathrm{fst},\mathrm{divisorsAntidiagonalList}(n))))$$

Formalization. D5/S3/Factorization/TwoDenseDivisorBlockMaximum.oddBlockCounts (✓ std3).

Source. Repository-derived.

Commentary.

Count odd entries in each block of the same partition used by the existing row function. At n=0 Mathlib’s divisor list is empty.

Theorem 1.2 (The maximum identity).

$$\forall n:\mathbb{N},0<n⟹\sup (\mathrm{toFinset}(\mathrm{row}(n)),\mathrm{id})=(\mathrm{factorization}(n,2)+1)\cdot \sup (\mathrm{toFinset}(\mathrm{oddBlockCounts}(n)),\mathrm{id})$$

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

Resolves. Problems/oeis-a400194-two-dense-divisor-block-maximum (proved) by D5/S3/Factorization/TwoDenseDivisorBlockMaximum.result.

Citation. Omar E. Pol (2026). OEIS A400194, maximum length of a two-dense divisor block. URL: https://oeis.org/A400194.

Commentary.

Sortedness and the strict separating boundaries show that divisor-list endpoints whose ratio is at most two have the same block membership. Every complete dyadic chain of an odd divisor therefore remains inside one actual block. The map from an odd member and an exponent between zero and factorization(n,2) to their dyadic product bijects onto that block. Odd-component recovery, cancellation and injectivity of powers of two prove injectivity. Distinct divisor entries turn the bijection into the local block-length identity. Taking suprema over the same block family gives the conjectured maximum formula. The zero default of the natural supremum is harmless; every positive n has divisor one.

References

• Truth anchor: D5/S3/Factorization/TwoDenseDivisorBlockMaximum.oddBlockCounts
• Truth anchor: D5/S3/Factorization/TwoDenseDivisorBlockMaximum.result
• Dependency: D5/S3/Factorization/TwoDenseDivisorBlocksPalindrome