mod6_eightynine_prime
plain-language theorem explainer
89 is a prime congruent to 5 modulo 6. Number theorists checking explicit residue-class properties of small primes would cite this instance. The proof is a one-line wrapper that invokes native_decide to evaluate the conjunction computationally.
Claim. $89$ is prime and $89 ≡ 5 mod 6$.
background
The declaration lives in the ArithmeticFunctions module, whose module documentation describes lightweight wrappers around Mathlib arithmetic functions that begin with the Möbius function μ and keep statements minimal until Dirichlet inversion stabilizes. The sole upstream result is the transparent alias Prime n := Nat.Prime n, which imports the standard primality predicate without additional hypotheses.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of primality and the modular equality.
why it matters
The result supplies an explicit modular fact about the prime 89 inside the NumberTheory layer. It aligns with Recognition Science interest in primes congruent to 5 mod 6, a class that includes constants near the fine-structure inverse such as 137. No downstream theorems yet reference it, so its precise role in larger forcing-chain or RCL calculations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.