has_prime_factor

formal source

 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
 117/-! ## J-Cost on the Multiplicative Ledger
 118
 119Each ratio in the ledger carries J-cost. The total cost of a
 120transaction n is related to the costs of its prime factors
 121through the d'Alembert identity (the RCL). -/
 122
 123/-- The d'Alembert identity for J-cost:
 124    J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y) -/
 125theorem j_dalembert {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 126    Cost.Jcost (x * y) + Cost.Jcost (x / y) =
 127    2 * Cost.Jcost x + 2 * Cost.Jcost y + 2 * Cost.Jcost x * Cost.Jcost y :=
 128  Cost.dalembert_identity hx hy
 129
 130/-- J-cost submultiplicativity: the cost of a composite transaction
 131    is bounded by the costs of its factors. -/
 132theorem j_submult {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 133    Cost.Jcost (x * y) ≤
 134    2 * Cost.Jcost x + 2 * Cost.Jcost y + 2 * Cost.Jcost x * Cost.Jcost y :=
 135  Cost.Jcost_submult hx hy
 136
 137/-! ## The Reciprocal Symmetry and the Critical Line
 138
 139The RS cost function satisfies J(x) = J(1/x): reciprocal symmetry.
 140The ζ functional equation has the analogous reflection s ↔ 1-s.
 141
 142The critical line Re(s) = 1/2 is the fixed point of s ↔ 1-s,
 143just as x = 1 is the fixed point of x ↔ 1/x.