j_dalembert

formal source

 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.
 144
 145The completed zeta function ξ(s) = ξ(1-s) has this same symmetry.
 146Defining Ξ(t) := ξ(1/2 + it), RH is equivalent to:
 147"all zeros of Ξ are real."
 148
 149The RS structural prediction:
 150Since d'Alembert solutions have zeros on lines,
 151and the ledger's cost structure is governed by d'Alembert,
 152the zeros of Ξ should be confined to the real line. -/
 153
 154/-- J is symmetric under inversion: the RS "functional equation." -/
 155theorem j_functional_equation {x : ℝ} (hx : 0 < x) :