sum_of_squares_seventeen
plain-language theorem explainer
17 equals 1 squared plus 4 squared. Researchers classifying primes congruent to 1 mod 4 as sums of two squares cite this explicit identity as a base case. The proof is a one-line wrapper that applies the native_decide tactic to evaluate the numerical equality directly.
Claim. $17 = 1^2 + 4^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and squarefree checks. This theorem records a concrete numerical identity for the prime 17, placed in the file for organizational convenience despite lacking direct dependence on the Möbius machinery. No upstream results or sibling definitions are referenced.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to confirm the equality by direct computation.
why it matters
It supplies a verified base case for sums of two squares representations within the number theory component. No parent theorems or downstream uses appear in the dependency graph, and the declaration does not engage the Recognition Science forcing chain, phi-ladder, or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.