palindromic_prime_three
plain-language theorem explainer
The declaration asserts that 3 is prime in the natural numbers. Researchers constructing arithmetic functions or prime-based objects in the Recognition Science number theory layer would cite this fact as a basic building block. The proof is a one-line term that applies native_decide to confirm the property directly.
Claim. $3$ is a prime number, i.e., it satisfies the standard primality predicate on the natural numbers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The local theoretical setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. The Prime predicate is a transparent alias for the standard primality condition on natural numbers.
proof idea
The proof is a one-line term that invokes native_decide to verify the primality of 3 by direct computation.
why it matters
This supplies a basic prime fact inside the arithmetic functions module. It supports any later prime-related constructions even though no downstream uses are currently recorded. The result sits alongside the Möbius footholds and remains independent of the core Recognition Science chain steps such as the J-uniqueness or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.