j_zero_at_fixed_point

formal source

 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`)
 191
 1922. d'Alembert solutions have zeros confined to lines
 193   (THEOREM: `cosh_no_real_zeros` + analytic continuation)
 194
 1953. The ζ functional equation ξ(s) = ξ(1-s) IS the RS reciprocal
 196   symmetry J(x) = J(1/x) applied to the number-theoretic ledger
 197   (MODEL: structural identification)
 198
 1994. σ = 0 conservation forces the zero line to be Re(s) = 1/2
 200   (PREDICTION: the critical line IS the ledger balance condition)
 201
 202THE GAP: Step 3 is a model identification, not a theorem.
 203The specific condition that would close it: proving that the