prime_nineteen
plain-language theorem explainer
19 satisfies the primality condition in the natural numbers. Number theorists assembling primorial products or Möbius inversions inside the Recognition framework cite this fact as a base case. The verification reduces to a single native decision procedure that checks the predicate directly.
Claim. $19$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream structures supply J-cost minimization, spectral emergence of gauge content and generations, and nuclear density tiers, placing these arithmetic facts inside the Recognition Science setting.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the primality statement.
why it matters
This supplies a verified small prime for primorial constructions that follow in the same file. It supports the arithmetic-function layer needed for Dirichlet inversion and Möbius footholds, which in turn feed number-theoretic tools used by the forcing chain and complexity structures. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.