liouville_eighthundredforty
plain-language theorem explainer
The Liouville function evaluates to 1 at 840 because its prime factorization 2^3 × 3 × 5 × 7 yields total exponent sum 6, which is even. Number theorists verifying explicit values of multiplicative functions for concrete integers would cite this instance. The result follows from a direct computational decision that evaluates the definition without manual expansion of factors.
Claim. $λ(840) = 1$, where $λ(n) = (-1)^{Ω(n)}$ and $Ω(840) = 6$ is even.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the Liouville function. The Liouville function is the completely multiplicative map sending each prime power p^k to (-1)^k, so that λ(n) = (-1)^Ω(n) with Ω the total number of prime factors counted with multiplicity. Upstream structures supply the Recognition Science setting: NucleosynthesisTiers.of organizes nuclear densities on φ-tiers, DAlembert.LedgerFactorization.of calibrates the J-cost map, PhiForcingDerived.of encodes J-cost convexity, and SpectralEmergence.of derives the gauge and generation content from the Q3 structure.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the prime factorization of 840 and the parity of Ω directly from the definition of liouville.
why it matters
This explicit evaluation supplies a concrete check inside the arithmetic-functions layer that supports verification of multiplicative identities. It sits downstream of the liouville definition in the same module and aligns with coprimality remarks on RS constants that follow in the file. No downstream theorems yet reference it, leaving open whether it will be invoked in larger Dirichlet-series or forcing-chain calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.