IndisputableMonolith.NumberTheory.Primes.Basic

   1import Mathlib
   2
   3/-!
   4Basic prime-number footholds for the `reality` repo.
   5
   6Design goals:
   7- Reuse Mathlib’s `Nat.Prime` and existing number theory library (don’t reinvent).
   8- Keep this namespace **axiom-free** and **sorry-free** so it can live in the main monolith.
   9- Provide small “sanity theorems” that confirm the module is wired correctly.
  10- Grow upward into analytic number theory only after the algebraic layer is stable.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace NumberTheory
  15namespace Primes
  16
  17open scoped BigOperators
  18
  19/-! ### Sanity checks (compile-time smoke) -/
  20
  21theorem prime_two : Nat.Prime 2 := by
  22  decide
  23
  24theorem prime_three : Nat.Prime 3 := by
  25  decide
  26
  27theorem not_prime_zero : ¬ Nat.Prime 0 := by
  28  decide
  29
  30theorem not_prime_one : ¬ Nat.Prime 1 := by
  31  decide
  32
  33/-! ### Local aliases (optional convenience) -/
  34
  35/-- Repo-local alias for Mathlib’s `Nat.Prime` (kept transparent). -/
  36abbrev Prime (n : ℕ) : Prop := Nat.Prime n
  37
  38@[simp] theorem prime_iff (n : ℕ) : Prime n ↔ Nat.Prime n := Iff.rfl
  39
  40end Primes
  41end NumberTheory
  42end IndisputableMonolith
  43