sum_of_squares_eightynine
plain-language theorem explainer
89 equals five squared plus eight squared. Researchers verifying sum-of-two-squares decompositions for primes congruent to one modulo four would cite this identity. The proof is a direct term-mode computation that evaluates both sides via native_decide.
Claim. $89 = 5^2 + 8^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This declaration provides a standalone numerical identity rather than a functional property of arithmetic functions. No upstream lemmas are invoked.
proof idea
The proof is a one-line term that applies native_decide to evaluate the equality directly.
why it matters
It supplies a verified instance of a sum-of-two-squares decomposition for the prime 89. No parent theorems or downstream uses are recorded. The result sits in the arithmetic foundations without reference to the forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.