liouville_six
plain-language theorem explainer
The declaration verifies that the Liouville function evaluates to 1 at 6. Number theorists checking multiplicative arithmetic functions cite this as a basic instance. The proof is a direct native computation from the definition λ(n) = (-1)^Ω(n).
Claim. $λ(6) = 1$, where $λ(n) = (-1)^{Ω(n)}$ and $Ω(n)$ counts all prime factors of $n$ with multiplicity.
background
The Liouville function is defined directly as λ(n) = (-1)^Ω(n) for n > 0 (and 0 at n = 0), with Ω(n) the total number of prime factors counted with multiplicity. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to λ. The upstream definition states: 'The Liouville function λ(n) = (-1)^Ω(n). Note: We define this directly since Mathlib may not have a prebuilt version.'
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the definition at the concrete input 6.
why it matters
This supplies a concrete evaluation inside the arithmetic functions module. It supports basic verifications in the number-theoretic layer of the Recognition Science framework but does not link to the forcing chain (T0-T8), the Recognition Composition Law, or physical constants such as α^{-1}. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.