IntegerLedgerStateLogic

formal source

  24  PrimeLedgerAtom (toNat p)
  25
  26/-- A recovered positive integer ledger state. -/
  27def IntegerLedgerStateLogic (n : LogicNat) : Prop :=
  28  0 < n
  29
  30theorem primeLedgerAtomLogic_iff_prime (p : LogicNat) :
  31    PrimeLedgerAtomLogic p ↔ Nat.Prime (toNat p) :=
  32  primeLedgerAtom_iff_prime (toNat p)
  33
  34theorem prime_is_ledger_atom_logic {p : LogicNat} (hp : Nat.Prime (toNat p)) :
  35    PrimeLedgerAtomLogic p :=
  36  (primeLedgerAtomLogic_iff_prime p).mpr hp
  37
  38theorem ledger_atom_logic_is_prime {p : LogicNat} (h : PrimeLedgerAtomLogic p) :
  39    Nat.Prime (toNat p) :=
  40  (primeLedgerAtomLogic_iff_prime p).mp h
  41
  42theorem one_not_primeLedgerAtomLogic :
  43    ¬ PrimeLedgerAtomLogic (fromNat 1) := by
  44  intro h
  45  have hp : Nat.Prime (toNat (fromNat 1)) := ledger_atom_logic_is_prime h
  46  rw [toNat_fromNat] at hp
  47  exact Nat.not_prime_one hp
  48
  49theorem prime_logic_is_positive_ledger_state {p : LogicNat}
  50    (hp : Nat.Prime (toNat p)) : IntegerLedgerStateLogic p := by
  51  exact (toNat_lt LogicNat.zero p).mpr (by simpa [toNat_zero] using hp.pos)
  52
  53/-- Certificate tying recovered-prime atoms to the classical prime ledger. -/
  54structure PrimeLedgerLogicCert where
  55  atom_iff_prime : ∀ p : LogicNat, PrimeLedgerAtomLogic p ↔ Nat.Prime (toNat p)
  56  one_not_atom : ¬ PrimeLedgerAtomLogic (fromNat 1)
  57  prime_positive : ∀ {p : LogicNat}, Nat.Prime (toNat p) → IntegerLedgerStateLogic p