sum_of_squares_five
plain-language theorem explainer
The natural number 5 equals the sum of two integer squares 1² + 2². Number theorists examining small cases of sums-of-squares representations would reference this identity. The verification is a direct computational check performed by the native decision procedure.
Claim. $5 = 1^2 + 2^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and related objects such as bigOmega. Local conventions treat these as standard number-theoretic tools without deeper Dirichlet inversion at this stage. The present declaration stands apart from the Möbius siblings and carries no upstream dependencies.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to confirm the equality by direct computation.
why it matters
The declaration supplies a basic arithmetic fact inside the arithmetic-functions module. It supports the lightweight style described in the module documentation but feeds no downstream results. No direct link to the Recognition Science forcing chain or phi-ladder appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.