IntegerLedgerState

formal source

  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