IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom

   1import Mathlib
   2import IndisputableMonolith.Foundation.ArithmeticFromLogic
   3import IndisputableMonolith.NumberTheory.PrimeLedgerAtom
   4
   5/-!
   6  LogicPrimeLedgerAtom.lean
   7
   8  Logic-native prime ledger atoms.
   9
  10  The first recovered-number adapter for the RH / prime-ledger stack:
  11  primality is stated on `LogicNat` and transported through the recovery
  12  equivalence `LogicNat.toNat`.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace NumberTheory
  17namespace LogicPrimeLedgerAtom
  18
  19open Foundation.ArithmeticFromLogic
  20open Foundation.ArithmeticFromLogic.LogicNat
  21
  22/-- A prime ledger atom over recovered naturals. -/
  23def PrimeLedgerAtomLogic (p : LogicNat) : Prop :=
  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
  58  transports_classical : ∀ p : LogicNat, PrimeLedgerAtomLogic p ↔ PrimeLedgerAtom (toNat p)
  59
  60def primeLedgerLogicCert : PrimeLedgerLogicCert where
  61  atom_iff_prime := primeLedgerAtomLogic_iff_prime
  62  one_not_atom := one_not_primeLedgerAtomLogic
  63  prime_positive := prime_logic_is_positive_ledger_state
  64  transports_classical := fun _ => Iff.rfl
  65
  66end LogicPrimeLedgerAtom
  67end NumberTheory
  68end IndisputableMonolith
  69