prime_threethousandfiveeleven
plain-language theorem explainer
3511 is prime and is the second known Wieferich prime. Number theorists verifying specific primes or building prime-counting tables would reference the fact. The proof is a one-line computational check that applies native decision procedures to the primality predicate.
Claim. $3511$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting is a collection of basic number-theoretic facts that can later support Dirichlet inversion or prime-counting arguments. Upstream material includes the definition of future states in TimeEmergence and the collision-free property in OptionAEmpiricalProgram, both of which appear among the declaration’s direct dependencies.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the primality predicate on the concrete integer 3511.
why it matters
The declaration records a verified prime that can feed primeCounting or related arithmetic functions inside the same module. It supplies a concrete datum for any later empirical or computational checks that rely on an explicit list of primes, consistent with the module’s role as a foothold for Möbius-based arguments. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.