balanced_prime_twohundredfiftyseven
plain-language theorem explainer
257 is a balanced prime with 251 and 263 both prime and averaging exactly to 257, identified as Fermat prime F_3. Researchers examining prime distributions or arithmetic function applications in discrete structures would reference this specific case. The verification reduces to a direct computational check via native decision procedures on the primality predicates and the arithmetic equality.
Claim. $257$, $251$, and $263$ are prime, and their arithmetic mean satisfies $(251 + 263)/2 = 257$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem records a concrete balanced-prime instance centered at the Fermat prime 257. The local setting keeps statements minimal before layering Dirichlet algebra or inversion formulas.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of the three primality statements and the equality.
why it matters
The declaration supplies a verified example of a balanced prime at the Fermat number F_3 within the number-theory layer. It sits alongside Möbius and big-Omega definitions but carries no listed downstream uses. The fact touches the eight-tick octave structure through the exponent 8 in 2^8 + 1 without explicit linkage to the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.