balanced_prime_onehundredseventythree
plain-language theorem explainer
173 is prime and equals the average of the primes 167 and 179. Number theorists checking specific prime triples inside the Recognition Science arithmetic layer would cite this verification. The proof reduces to a single native decision step that evaluates primality and the averaging equality directly.
Claim. $173$ is prime, $167$ is prime, $179$ is prime, and $(167 + 179)/2 = 173$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A balanced prime is defined here as a prime that is the arithmetic mean of two other primes. The local abbreviation Prime stands for the standard natural-number primality predicate Nat.Prime. Upstream results include the balanced predicate on ledgers, which requires an event list to satisfy a balance condition, and several structure or class declarations that discharge hypotheses via algebraic or empirical checks.
proof idea
The proof is a one-line wrapper that applies native_decide to the full conjunction of three primality statements and the averaging equality.
why it matters
This supplies a concrete numerical check inside the primes arithmetic module. It supports preparatory number-theoretic scaffolding but feeds no listed parent theorems. The declaration aligns with framework emphasis on explicit small-integer verifications that can later interface with constants such as the alpha band or phi-ladder mass formulas, though no direct connection is made here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.