palindromic_prime_onehundredthirtyone
plain-language theorem explainer
The declaration establishes that 131 is a prime natural number. Researchers working with arithmetic functions in the Recognition Science framework would cite this when verifying base cases for Möbius inversions or prime-specific computations. The proof reduces to a single native_decide invocation that computationally confirms the primality predicate.
Claim. The natural number 131 is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function. The local setting keeps statements minimal until deeper Dirichlet algebra is added. Prime is the transparent alias for the standard primality predicate on natural numbers. Upstream results supply structural verifications such as collision-free classes and algebraic tautologies drawn from foundation, simplicial ledger, game theory, and Ramanujan bridge modules.
proof idea
The proof is a one-line term that applies native_decide to confirm 131 satisfies the primality definition.
why it matters
This supplies an explicit prime fact inside the arithmetic functions module. It serves as a base case for potential Möbius applications to prime sums, consistent with the module's role as a foothold for number theory. No downstream theorems depend on it, and it does not engage the forcing chain, phi-ladder, or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.