divisors_card_threehundredsixty
plain-language theorem explainer
The declaration asserts that the positive integer 360 possesses exactly 24 divisors. Number theorists computing sums over divisors or preparing Möbius inversion steps would reference this cardinality for concrete checks. The proof is a one-line native_decide term that evaluates the divisor set directly inside the Lean kernel.
Claim. The set of positive divisors of 360 has cardinality 24: $d(360) = 24$, where $d(n)$ denotes the divisor function.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Statements remain minimal to support later Dirichlet inversion once interfaces stabilize. Upstream structures include nuclear density tiers scaled by φ-powers, J-cost calibration on the positive reals, and spectral emergence of gauge groups with 24 chiral fermions, though none enter this specific computation.
proof idea
The proof is a one-line term wrapper that applies native_decide to compute the divisors of 360 and confirm the cardinality equals 24.
why it matters
This supplies a verified numerical anchor inside the arithmetic functions module that can support divisor-sum arguments in the Recognition framework. It sits alongside Möbius footholds used for inversion in the forcing chain from T0 to T8, though no downstream theorems currently cite it. The result closes a basic computational slot without touching the J-uniqueness or phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.