divisors_card_six
plain-language theorem explainer
The declaration records that the positive integer 6 has exactly four divisors. Number theorists using arithmetic functions for Möbius inversion or squarefree checks inside the Recognition Science number-theory layer would cite this concrete fact. The proof is a one-line term that invokes native_decide to evaluate the finite divisor set directly.
Claim. $|d(6)| = 4$, where $d(n)$ denotes the number of positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem supplies a basic instance of the divisor-counting function applied to the integer 6. Upstream results include the J-cost structure from PhiForcingDerived and the ledger-factorization structure from DAlembert, which together embed such arithmetic facts into the Recognition Science derivation of physical quantities.
proof idea
The proof is a term-mode application of native_decide that reduces the equality to a decidable computation on the explicit finite set of divisors of 6.
why it matters
The result supplies a concrete arithmetic fact inside the NumberTheory.Primes.ArithmeticFunctions module that establishes Möbius footholds for the framework. It supports calculations that appear in spectral-emergence structures and simplicial-ledger constructions, aligning with the need for precise divisor counts when applying the Recognition Composition Law or phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.