prime_fivehundredninetynine
plain-language theorem explainer
The declaration asserts that 599 is a prime number. Number theorists working with arithmetic functions such as the Möbius function would cite this fact when verifying squarefreeness or inversion formulas for specific inputs. The proof is a one-line term that invokes the native_decide tactic to resolve the primality predicate computationally.
Claim. $599$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local conventions treat primes as base cases for these functions, where μ(p) = -1 for any prime p. The Prime predicate is drawn from the sibling Basic module to encode the standard definition of primality.
proof idea
The proof is a term-mode one-liner that applies native_decide to discharge the statement that 599 satisfies the Prime predicate.
why it matters
This supplies a concrete prime instance inside the arithmetic functions file, enabling direct use in Möbius calculations and related number theory within the Recognition Science framework. It supports the broader development of Dirichlet algebra tools, though it does not tie directly to forcing chains or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.