prime_threethousandfiveeleven
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 in Recognition Science
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.
scope and limits
- Does not prove any multiplicative or arithmetic-function properties of 3511.
- Does not connect the primality statement to Recognition Science forcing chains or constants.
- Does not supply a manual or analytic proof, only computational verification.
- Does not address Wieferich congruence conditions beyond the primality claim.
formal statement (Lean)
2382theorem prime_threethousandfiveeleven : Prime 3511 := by native_decide
proof body
Term-mode proof.
2383
2384-- Note: primeCounting for values > 1000 requires careful verification
2385-- Leaving larger primeCounting values for future sessions
2386
2387/-! ### Primes in the 500s -/
2388
2389/-- 503 is prime. -/