sum_of_squares_onehundrednine
plain-language theorem explainer
The natural number 109 equals 3 squared plus 10 squared. Number theorists verifying small Diophantine representations or sum-of-squares identities might cite the equality. The proof reduces directly to a single native decision step in the Lean kernel.
Claim. $109 = 3^2 + 10^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. This theorem records a basic numerical identity inside the same file. No upstream lemmas are referenced.
proof idea
One-line wrapper that applies native_decide to confirm the equality by direct computation.
why it matters
The identity supplies a verified numerical fact within the NumberTheory.Primes.ArithmeticFunctions module but does not connect to Möbius inversion, Dirichlet algebra, or Recognition Science landmarks such as the forcing chain or phi-ladder. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.