balanced_prime_five
plain-language theorem explainer
The declaration verifies that 5 is a balanced prime by confirming primality of 5, 3 and 7 together with the arithmetic mean relation. Number theorists examining prime instances within Recognition Science arithmetic footholds would cite this concrete case. The proof is a direct computational check via native decision procedures on the finite conjunction.
Claim. $5$ is prime, $3$ is prime, $7$ is prime, and $(3 + 7)/2 = 5$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related maps. Prime is the transparent alias for Nat.Prime. The upstream balanced definition states that a ledger is balanced precisely when its event list satisfies the balanced_list predicate.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the finite conjunction of primality predicates and the arithmetic equality.
why it matters
This supplies an explicit base-case instance of a balanced prime inside the arithmetic-functions layer. It supports the number-theory footholds that feed the forcing chain (T0-T8) and Recognition Composition Law by furnishing concrete prime data. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.