sum_of_squares_twentynine
plain-language theorem explainer
29 equals 2 squared plus 5 squared. Number theorists checking small-case representations of primes congruent to 1 mod 4 may reference this identity during enumeration or verification steps. The proof is a direct computational check via native decision procedures.
Claim. $29 = 2^2 + 5^2$
background
The declaration appears in a module that supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The module setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces are stable. No upstream lemmas are invoked.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the numerical equality by direct evaluation.
why it matters
The identity supplies an explicit small-case fact inside the NumberTheory.Primes section. It sits alongside Möbius and big-Omega definitions but carries no recorded downstream uses. It supports the framework's pattern of verified computational checks for concrete integers without advancing the main forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.