prime_ninetyseven
plain-language theorem explainer
97 is asserted to be prime in the natural numbers. Number theorists applying arithmetic functions within the Recognition Science setup would reference this specific prime fact during Möbius calculations or factorization steps. The proof reduces to a single decision procedure invocation.
Claim. The natural number $97$ is prime.
background
The module supplies lightweight wrappers for Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard primality predicate on natural numbers. The vp definition extracts the exponent of a given prime in the factorization of a number.
proof idea
It is a one-line wrapper that invokes the decide tactic on the primality statement.
why it matters
The result populates the set of known primes available to the arithmetic functions layer. It aligns with the number theory prerequisites for the Recognition Science forcing chain, though no immediate parent theorem or downstream application is specified in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.