divisors_card_thirty
plain-language theorem explainer
The theorem records that the positive integer 30 possesses exactly eight divisors. Number theorists applying divisor counts inside arithmetic-function wrappers for Möbius inversion or Dirichlet series in the Recognition Science setting would cite this fact. The proof is a one-line native decision procedure that evaluates the divisor set and its cardinality directly.
Claim. The set of positive divisors of 30 has cardinality 8: $|{d ∈ ℕ⁺ : d | 30}| = 8$.
background
The declaration sits inside the module supplying lightweight wrappers around Mathlib arithmetic functions, with emphasis on the Möbius function μ as the initial interface. The module keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic definitions stabilize. Upstream structures supply phi-tier nuclear densities, J-cost calibration, and spectral emergence of gauge groups, yet this divisor count functions as an independent computational anchor.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic. This tactic reduces the equality to a kernel-level computation of the divisor set of 30 and its cardinality, discharging the goal without further lemmas.
why it matters
The result supplies a concrete numerical foothold inside the arithmetic-functions layer that supports later Möbius-based inversion steps in the Recognition Science number-theory development. It aligns with the module's role as a staging area for Dirichlet tools that may eventually interface with the phi-ladder and forcing chain. No downstream uses are recorded, so its integration into larger T5–T8 derivations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.