balanced_prime_fiftythree
plain-language theorem explainer
53 qualifies as a balanced prime because 47 and 59 are both prime and average exactly to 53. Number theorists collecting concrete prime-triplet instances inside the Recognition Science arithmetic-functions module would cite this fact. The verification is a one-line native_decide invocation that evaluates the primality predicates and the arithmetic identity in a single step.
Claim. $47$, $53$, and $59$ are all prime and satisfy $(47 + 59)/2 = 53$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and keeping statements minimal until Dirichlet inversion layers are added. The local Prime abbreviation is the transparent alias for the standard natural-number primality predicate. Upstream ledger constructions define balanced as the property that an event list satisfies a balance condition, while the Ramanujan-bridge and mechanism-design structures supply supporting combinatorial scaffolding.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of three primality checks and the central arithmetic equality.
why it matters
The declaration supplies a verified concrete instance of a balanced prime at 53, filling a small slot in the number-theory scaffolding that supports the Recognition Science framework. It sits downstream of the basic Prime definition and the balanced ledger predicate, contributing to the arithmetic facts that may later interface with the phi-ladder or eight-tick octave. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.