IndisputableMonolith.NumberTheory.PrimeLedgerAtom

   1import Mathlib
   2
   3/-!
   4# Prime Ledger Atoms
   5
   6This module grounds the arithmetic ledger used by the RH bridge.
   7
   8The content is deliberately classical and small: primes are exactly the
   9irreducible postings of the multiplicative positive-integer ledger.  The RS
  10work starts after this point, when the prime postings are weighted into the
  11Euler ledger.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NumberTheory
  16
  17/-- A prime ledger atom is a prime integer together with the irreducibility
  18property appropriate to the multiplicative ledger. -/
  19structure PrimeLedgerAtom (p : ℕ) : Prop where
  20  prime : Nat.Prime p
  21  irreduciblePosting : ∀ a b : ℕ, p = a * b → a = 1 ∨ b = 1
  22
  23/-- Positive integers are the states of the multiplicative integer ledger. -/
  24def IntegerLedgerState (n : ℕ) : Prop := 0 < n
  25
  26/-- A prime number is an irreducible posting of the integer ledger. -/
  27theorem prime_is_ledger_atom {p : ℕ} (hp : Nat.Prime p) : PrimeLedgerAtom p where
  28  prime := hp
  29  irreduciblePosting := by
  30    intro a b hab
  31    have ha_dvd : a ∣ p := ⟨b, by rw [hab]⟩
  32    have ha := hp.eq_one_or_self_of_dvd a ha_dvd
  33    rcases ha with ha | ha
  34    · exact Or.inl ha
  35    · right
  36      have hb_eq : p = p * b := by
  37        simpa [ha] using hab
  38      have hb : p * b = p * 1 := by
  39        simpa using hb_eq.symm
  40      exact Nat.mul_left_cancel hp.pos hb
  41
  42/-- Ledger atoms are prime numbers. -/
  43theorem ledger_atom_is_prime {p : ℕ} (h : PrimeLedgerAtom p) : Nat.Prime p :=
  44  h.prime
  45
  46/-- Prime-ledger atom iff ordinary primality. -/
  47theorem primeLedgerAtom_iff_prime (p : ℕ) :
  48    PrimeLedgerAtom p ↔ Nat.Prime p :=
  49  ⟨ledger_atom_is_prime, prime_is_ledger_atom⟩
  50
  51/-- The unit is not a prime ledger atom. -/
  52theorem one_not_primeLedgerAtom : ¬ PrimeLedgerAtom 1 := by
  53  intro h
  54  exact Nat.not_prime_one h.prime
  55
  56/-- Every prime is a positive ledger state. -/
  57theorem prime_is_positive_ledger_state {p : ℕ} (hp : Nat.Prime p) :
  58    IntegerLedgerState p := hp.pos
  59
  60/-- Certificate for the arithmetic base of the prime ledger. -/
  61structure PrimeLedgerCert where
  62  atom_iff_prime : ∀ p : ℕ, PrimeLedgerAtom p ↔ Nat.Prime p
  63  one_not_atom : ¬ PrimeLedgerAtom 1
  64  prime_positive : ∀ {p : ℕ}, Nat.Prime p → IntegerLedgerState p
  65
  66/-- The prime ledger certificate. -/
  67def primeLedgerCert : PrimeLedgerCert where
  68  atom_iff_prime := primeLedgerAtom_iff_prime
  69  one_not_atom := one_not_primeLedgerAtom
  70  prime_positive := prime_is_positive_ledger_state
  71
  72end NumberTheory
  73end IndisputableMonolith
  74