balanced_prime_onehundredfiftyseven
plain-language theorem explainer
157 is the arithmetic mean of the primes 151 and 163. Number theorists checking concrete balanced-prime instances inside the Recognition Science arithmetic layer would cite this result. The verification is a single native_decide term that evaluates the full conjunction of primality and averaging equality at compile time.
Claim. $157$, $151$, and $163$ are prime and satisfy $(151 + 163)/2 = 157$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent local alias for Nat.Prime. The balanced predicate from LedgerForcing asserts that a ledger is balanced precisely when its event list is balanced. This theorem supplies a numerical instance of the balanced-prime pattern without invoking Möbius or Dirichlet inversion.
proof idea
The proof is a term-mode native_decide that directly evaluates the conjunction of three Prime statements and the averaging equality.
why it matters
The declaration supplies a verified numerical foothold for balanced primes at 157. It sits in the arithmetic-functions module whose doc-comment emphasizes basic interfaces before deeper inversion work. No downstream theorems depend on it, leaving the link to ledger balancing or the eight-tick octave as an open extension point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.