divisors_card_ten
plain-language theorem explainer
The positive divisors of 10 number exactly four. Researchers working with arithmetic functions in the Recognition Science primes module would cite this for verifying small-cardinality cases in divisor counts. The proof is a one-line native_decide term that evaluates the finite divisors set at compile time.
Claim. The cardinality of the set of positive divisors of $10$ equals $4$.
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Statements remain minimal to support later Dirichlet algebra and inversion layers. This theorem draws on basic natural-number divisor enumeration; upstream structures include J-cost calibration from PhiForcingDerived and spectral emergence from Q₃, though the present result uses only finite-set cardinality.
proof idea
The proof is a one-line term that applies native_decide to compute the divisors of 10 and their cardinality directly.
why it matters
This supplies a verified small-case fact inside the primes arithmetic-functions layer. It supports discrete counting steps that appear in Recognition Science number-theoretic footholds, consistent with the module's Möbius emphasis. No downstream uses are recorded and no open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.