isolated_prime_fiftythree
plain-language theorem explainer
53 is prime while its immediate neighbors 51 and 55 are composite, establishing 53 as an isolated prime. Number theorists working on small-scale prime isolation or gap facts inside the Recognition monolith would cite this concrete instance. The proof reduces to a single native_decide call that settles the three primality claims by direct computation.
Claim. $53$ is prime, while $51$ and $55$ are composite.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repository-local transparent alias for the standard predicate Nat.Prime on natural numbers. The supplied doc-comment identifies 53 as isolated because 51 factors as 3 times 17 and 55 factors as 5 times 11.
proof idea
One-line wrapper that applies the native_decide tactic to discharge the conjunction by exhaustive computational verification of the three primality statements.
why it matters
The theorem supplies a concrete numerical anchor inside the NumberTheory.Primes.ArithmeticFunctions section. No downstream uses are recorded, so it functions as a verified fact available for later arithmetic-function or prime-distribution arguments in the monolith. It aligns with the framework's pattern of recording small, decidable number-theoretic landmarks without invoking the Möbius inversion machinery developed elsewhere in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.