pith. machine review for the scientific record. sign in
theorem proved term proof

jcost_log_zero_unique

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

Last generation error: xAI API error (429): The model is currently at capacity due to high demand. Please try again in a few minutes. For guaranteed processing and availability, please request Provisioned Throughput: https://docs.x.ai/developers/advanced-api-usage/provisioned-throughput

generate prose now

formal statement (Lean)

  86theorem jcost_log_zero_unique (t : ℝ) :
  87    Cost.Jcost (Real.exp t) = 0 ↔ t = 0 := by

proof body

Term-mode proof.

  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. -/

depends on (26)

Lean names referenced from this declaration's body.