divisors_card_twelve_gt
plain-language theorem explainer
The declaration establishes that every positive integer n below 12 has strictly fewer divisors than 12 itself. Number theorists examining highly composite numbers or the growth of the divisor function would cite this fact when ordering small integers by divisor count. The proof exhausts the eleven possible values of n through case splitting followed by decision procedures.
Claim. For every positive integer $n$ satisfying $0 < n < 12$, the divisor function satisfies $d(n) < d(12)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its basic properties such as vanishing on non-squarefree arguments. The local setting keeps statements elementary so that Dirichlet inversion can be added later without heavy infrastructure. This particular result supplies the concrete divisor-count comparison needed to recognize 12 as highly composite.
proof idea
The proof introduces n together with the positivity and upper-bound hypotheses. It then invokes interval_cases to split into the eleven concrete subgoals n = 1 through n = 11, each of which is discharged by native_decide.
why it matters
The result supplies the base verification that 12 is highly composite, directly preceding the module's claim for 60. It therefore anchors the arithmetic-function scaffolding used throughout the Recognition Science development of number-theoretic constants and ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.