inversion_fixed_point

formal source

 157  Cost.Jcost_symm hx
 158
 159/-- The fixed point of x ↔ 1/x is x = 1. This is the RS "critical point." -/
 160theorem inversion_fixed_point (x : ℝ) (hx : 0 < x) :
 161    x = x⁻¹ ↔ x = 1 := by
 162  constructor
 163  · intro h
 164    have hne : x ≠ 0 := ne_of_gt hx
 165    have : x * x = 1 := by
 166      calc x * x = x * x⁻¹ := by rw [← h]
 167        _ = 1 := mul_inv_cancel₀ hne
 168    have hx_sq : x ^ 2 = 1 := by rwa [sq]
 169    nlinarith [sq_nonneg (x - 1)]
 170  · intro h; rw [h]; simp
 171
 172/-- J has its unique zero at the fixed point x = 1. -/
 173theorem j_zero_at_fixed_point : Cost.Jcost 1 = 0 := Cost.Jcost_unit0
 174
 175/-- J is strictly positive away from the fixed point. -/
 176theorem j_positive_off_fixed_point (x : ℝ) (hx : 0 < x) (hne : x ≠ 1) :
 177    0 < Cost.Jcost x :=
 178  Cost.Jcost_pos_of_ne_one x hx hne
 179
 180/-! ## The RS Prediction of the Riemann Hypothesis
 181
 182**HYPOTHESIS (not theorem)**
 183
 184The Riemann Hypothesis states that all non-trivial zeros of the
 185Riemann zeta function have real part 1/2.
 186
 187RS predicts this from the following chain:
 188
 1891. The recognition ledger's multiplicative structure is governed by
 190   the d'Alembert equation (THEOREM: `rs_cost_satisfies_dalembert`)