sum_of_squares_ninetyseven
plain-language theorem explainer
The declaration asserts the numerical identity 97 = 4² + 9². Number theorists working on sums of two squares for primes of the form 4k+1 may cite this concrete case. The proof is a direct computational verification that applies native_decide to the equality.
Claim. $97 = 4^2 + 9^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ (ArithmeticFunction.moebius). μ(n) vanishes on non-squarefree inputs and equals (-1)^k on squarefree n with k distinct prime factors. The local setting keeps statements minimal so that Dirichlet convolution and inversion can be added once the basic interfaces stabilize. This theorem supplies an isolated numerical fact inside the primes section without invoking those functions.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the arithmetic equality by direct computation.
why it matters
The identity supplies a basic numerical check inside the NumberTheory.Primes.ArithmeticFunctions module. It sits among Möbius-related definitions but has no downstream uses or parent theorems in the supplied graph. No direct link to Recognition Science landmarks such as the phi-ladder or RCL appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.