prime_fourhundredninetynine
plain-language theorem explainer
The declaration asserts that the integer 499 is prime. Number theorists building arithmetic function libraries or verifying small primes would cite this fact for foundational checks. The proof reduces to a single native_decide application that evaluates the primality predicate by direct computation.
Claim. $499$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The local setting keeps statements minimal to support later Dirichlet algebra and inversion layers. Upstream results include the active edge count A from IntegrationGap, defined as the φ-power balance identity at D=3, and the primality predicate Prime from the Basic primes module.
proof idea
This is a one-line term proof that applies the native_decide tactic to settle the primality claim computationally.
why it matters
The result supplies a concrete primality instance inside the primes arithmetic functions module. It has no listed downstream applications. The declaration fills a basic number-theoretic slot but does not engage the Recognition Science forcing chain, RCL identity, or phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.