sum_of_squares_onehundredthirtyseven
plain-language theorem explainer
The equality 137 equals 4 squared plus 11 squared is recorded for its alignment with the Recognition Science prediction for the inverse fine-structure constant. Researchers examining sum-of-two-squares decompositions in the alpha band would cite this identity when linking number theory to the framework constants. The verification is a direct native decision procedure that confirms the arithmetic without additional lemmas.
Claim. $137 = 4^{2} + 11^{2}$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. This declaration is an isolated numerical identity placed in the file because of its relevance to Recognition Science constants. Upstream results include the transparent alias for Nat.Prime and structural 'is' predicates from foundation modules that discharge as algebraic tautologies or hypothesis interfaces.
proof idea
The proof is a one-line wrapper that applies native_decide to verify the numerical equality.
why it matters
This identity supports the framework's alpha inverse band inside the interval (137.030, 137.039). It connects to the T5 J-uniqueness step and the constants in RS-native units. No downstream theorems are recorded yet, leaving it as a number-theoretic foothold in the primes module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.