mod6_five_prime
plain-language theorem explainer
The declaration asserts that 5 is prime and congruent to 5 modulo 6. Number theorists checking small-prime residues for modular arithmetic would cite this fact. The proof is a direct one-line native_decide application that evaluates the conjunction in the kernel.
Claim. $5$ is prime and $5$ satisfies $5 ≡ 5$ (mod 6).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and keeping statements minimal before Dirichlet inversion layers. Prime is the transparent alias for Nat.Prime. The upstream result is the Basic module abbrev that reexports the standard primality predicate without added structure.
proof idea
One-line wrapper that applies native_decide to the conjunction.
why it matters
The fact supplies a modular residue check on the prime 5 inside the primes arithmetic-functions file. It supports Recognition Science modular properties of small primes that appear in constant derivations such as the alpha band. No downstream uses are recorded, so the declaration functions as a basic verified checkpoint rather than a core lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.