balanced_prime_twohundredeleven
plain-language theorem explainer
211 is a balanced prime because it is the arithmetic mean of the primes 199 and 223. Number theorists cataloging prime constellations or balanced structures inside the Recognition Science arithmetic-functions layer would cite this explicit triple. The proof is a one-line native decision that evaluates the three primality predicates and the averaging equality by direct computation.
Claim. $211$, $199$, and $223$ are all prime, and $(199 + 223)/2 = 211$.
background
The module supplies thin wrappers around Mathlib arithmetic functions, beginning with the Möbius function, to support later Dirichlet inversion. Prime is the transparent alias for the standard predicate Nat.Prime on natural numbers. The balanced predicate imported from LedgerForcing states that a ledger is balanced precisely when its event list is balanced; the present theorem instantiates that predicate for the concrete prime 211 via the averaging condition.
proof idea
The proof is a one-line term wrapper that applies native_decide to the entire conjunction, letting the computational kernel verify primality of each integer and the exact arithmetic equality without invoking any named lemmas.
why it matters
The declaration supplies a concrete balanced-prime example inside the arithmetic-functions module, directly referencing the balanced ledger predicate from LedgerForcing. It sits among the lightweight Möbius footholds that precede deeper inversion work, yet currently has no downstream dependents. It therefore functions as an isolated verification point rather than a link in the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.