jcost_log_zero_unique

formal source

  83
  84/-- The J-cost G(t) = cosh(t) - 1 has its unique real zero at t = 0.
  85    In log coordinates, t = 0 means x = e⁰ = 1: the RS balance point. -/
  86theorem jcost_log_zero_unique (t : ℝ) :
  87    Cost.Jcost (Real.exp t) = 0 ↔ t = 0 := by
  88  rw [show Cost.Jcost (Real.exp t) = Cost.Jlog t from rfl]
  89  exact Cost.Jlog_eq_zero_iff t
  90
  91/-! ## Multiplicative Structure and Primes
  92
  93In the RS ledger, multiplication is the composition of transactions.
  94Primes are irreducible: they cannot be further decomposed. The
  95unique factorization theorem says every transaction has a unique
  96decomposition into irreducible parts. -/
  97
  98/-- A prime is an irreducible ledger transaction: it cannot be
  99    written as a product of two smaller transactions. -/
 100theorem primes_are_irreducible (p : ℕ) (hp : Nat.Prime p) :
 101    ∀ a b : ℕ, a * b = p → a = 1 ∨ b = 1 := by
 102  intro a b hab
 103  have := hp.eq_one_or_self_of_dvd a ⟨b, hab.symm⟩
 104  rcases this with ha | ha
 105  · left; exact ha
 106  · right; subst ha
 107    have h1 : 0 < a := Nat.pos_of_ne_zero hp.ne_zero
 108    have h2 : a * b = a * 1 := by omega
 109    exact (Nat.mul_left_cancel (Nat.pos_of_ne_zero hp.ne_zero) h2)
 110
 111/-- Every natural number > 1 has at least one prime factor.
 112    The ledger cannot avoid primes. -/
 113theorem has_prime_factor (n : ℕ) (hn : 1 < n) :
 114    ∃ p : ℕ, Nat.Prime p ∧ p ∣ n :=
 115  Nat.exists_prime_and_dvd (by omega)
 116