palindromic_prime_threehundredeightythree
plain-language theorem explainer
383 is asserted to be a prime number. Number theorists building libraries of concrete prime instances for arithmetic function work would cite this fact. The proof executes as a direct computational check via the native_decide tactic.
Claim. The natural number $383$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is defined locally as a transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results include foundational 'is' structures from OptionAEmpiricalProgram, SimplicialLedger, GameTheory, and RamanujanBridge modules that enforce collision-free or algebraic properties, plus the basic Prime alias.
proof idea
The proof is a one-line term-mode wrapper that applies the native_decide tactic to evaluate the primality predicate on 383.
why it matters
The declaration supplies a verified palindromic prime example inside the arithmetic functions module. It does not feed any parent theorems, as the used_by count is zero. It touches number theory foundations but does not engage the Recognition Science forcing chain, J-uniqueness, or phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.