prime_twohundredeleven
plain-language theorem explainer
The declaration asserts that 211 is a prime natural number. Number theorists building arithmetic functions or Möbius-based inversions inside the Recognition Science framework would cite this fact when verifying small primes for later Dirichlet constructions. The proof reduces the claim to a single native_decide tactic that executes a decidable primality check.
Claim. $211$ is prime, i.e., it satisfies the predicate of having no positive divisors other than $1$ and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related maps. The Prime abbreviation used here is the transparent alias for Nat.Prime supplied by the sibling Basic module. Upstream results include structural consistency statements from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma, and MockThetaPhantom that maintain framework coherence across foundation and game-theory layers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality predicate by direct computational enumeration of possible factors.
why it matters
This primality fact supplies a concrete base case for arithmetic-function development in the NumberTheory layer. It supports the module's stated goal of stabilizing basic interfaces before layering Dirichlet algebra and inversion. No downstream uses are recorded yet, so the declaration functions as a primitive building block rather than a derived result inside the T0-T8 forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.