divisors_card_fortyfive
plain-language theorem explainer
The declaration asserts that the positive integer 45 has exactly six positive divisors. Number theorists or Recognition Science practitioners computing small cases of the divisor function ahead of Möbius inversion or phi-ladder mass formulas would cite this fact. The proof reduces to a single native decision tactic that evaluates the divisor set directly from the integer representation.
Claim. $d(45) = 6$, where $d(n)$ denotes the number of positive divisors of the natural number $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ and basic square-free checks before deeper Dirichlet algebra. Local conventions treat divisor cardinality as a primitive count on the positive integers, independent of the Recognition Science forcing chain. Upstream structures include phi-tier nuclear densities and J-cost ledger factorizations, yet this computation stands as an isolated numerical verification.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the set of divisors of 45 and confirm its cardinality equals 6.
why it matters
This basic arithmetic checkpoint supports Möbius footholds in the NumberTheory.Primes.ArithmeticFunctions module and aligns with the need for exact divisor counts when evaluating mass formulas on the phi-ladder. It fills a small computational slot with no listed parent theorems and touches no open questions in the T0-T8 chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.