divisors_card_eight
plain-language theorem explainer
The statement asserts that the positive integer 8 has exactly four positive divisors. Number theorists handling divisor counts or Möbius inversion steps in Recognition Science would cite this when working with powers of two. The proof is a direct computational verification via native decision procedures.
Claim. $d(8)=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 μ. Local conventions treat statements as footholds for later Dirichlet inversion once basic interfaces stabilize. Upstream structures include J-cost calibration and spectral emergence, where factors of 8 appear in counting 24 chiral fermion flavors and |Aut(Q₃)|=48.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the cardinality of the divisor set of 8 directly.
why it matters
This fact supplies a concrete arithmetic anchor for Möbius footholds in the NumberTheory layer. It aligns with the eight-tick octave (T7) in the forcing chain, where 2^3 enters dimensional and generational counts. No downstream theorems are recorded yet, so the declaration functions as basic scaffolding for future prime-power and ladder applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.