divisors_card_onehundredtwenty_gt
plain-language theorem explainer
The declaration proves that every positive integer n less than 120 has strictly fewer divisors than 120 itself. Researchers studying highly composite numbers or bounds on the divisor function would cite this result as a concrete verification. The proof reduces the universal statement to 119 finite cases via interval_cases and resolves each by native_decide computation.
Claim. For all natural numbers $n$ satisfying $0 < n < 120$, the number of positive divisors of $n$ is strictly less than the number of positive divisors of 120.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to divisor counts. The divisor cardinality function counts the positive divisors of a natural number. The supplied doc-comment states that 120 is highly composite, meaning it has more divisors than any smaller positive integer. The local theoretical setting is arithmetic functions in the primes and squarefree context, with no deeper Dirichlet inversion developed here. Upstream structures such as the phi-ladder lattice hypothesis and empirical program collision-freeness provide broader number-theoretic scaffolding but are not invoked in this computational check.
proof idea
The proof introduces the variables n, hn, hlt and applies interval_cases n to split the range 1 to 119 into individual cases. Each case is discharged by native_decide, which evaluates the divisor cardinalities by direct computation.
why it matters
The result supplies a concrete bound confirming the highly composite character of 120 within the arithmetic functions module. It supports the module's role in providing footholds for Möbius and divisor tools that may feed into phi-ladder lattice constructions or Ramanujan bridge structures, though no downstream uses are recorded. In the Recognition framework it aligns with integer arithmetic properties appearing in the forcing chain T0-T8 and the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.