divisors_card_sixty
plain-language theorem explainer
The declaration establishes that 60 possesses exactly twelve positive divisors. Number theorists consulting the arithmetic-functions layer of Recognition Science would cite it for rapid cardinality checks on small integers during Möbius or divisor-sum calculations. Its proof reduces to a single native decision procedure that enumerates the divisor set and compares its size directly.
Claim. The cardinality of the set of positive divisors of 60 equals 12: $|{d ∈ ℕ : d | 60}| = 12$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The present theorem is a basic cardinality statement for the divisor set of a fixed natural number. Upstream structures include nuclear-density tiers in φ-powers and J-cost calibration, yet this fact depends only on direct evaluation of the divisor predicate rather than those constructions.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the equality from the definition of the divisor set.
why it matters
It supplies a verified numerical anchor inside the arithmetic-functions module, consistent with the module's stated goal of keeping statements lightweight before deeper Dirichlet algebra is added. No parent theorem in the supplied used-by list exists, and the result touches none of the forcing-chain steps T5–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.