theorem
proved
term proof
j_positive_off_fixed_point
show as:
view Lean formalization →
formal statement (Lean)
176theorem j_positive_off_fixed_point (x : ℝ) (hx : 0 < x) (hne : x ≠ 1) :
177 0 < Cost.Jcost x :=
proof body
Term-mode proof.
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
204completed zeta function Ξ(t) = ξ(1/2 + it) satisfies a
205d'Alembert-type constraint from the Euler product structure.
206
207FALSIFIER: Discovery of a non-trivial zero with Re(s) ≠ 1/2. -/
208
209/-! ### Note on a Lean statement of RH
210
211A faithful Lean statement of the Riemann Hypothesis requires the
212Riemann zeta function `ζ : ℂ → ℂ` and its non-trivial zeros to be
213available in the ambient library. As of this writing, mathlib's
214zeta development is partial; in particular a clean `RH` predicate
215that quantifies over non-trivial zeros and asserts
216`Re ρ = 1/2` is not yet stockpiled here.
217
218Rather than introduce a vacuous placeholder `Prop` that obscures
219the gap, we deliberately omit a Lean-level RH statement from this
220module. The structural theorems below (`structural_parallel_certificate`
221and friends) are the genuine machine-checked content of the
222companion paper; the bridge to `ζ` is the open analytic question
223documented in that paper. -/
224
225/-- The structural parallel: the number of properties shared between
226 J-cost and the ζ functional equation. Each is a separately proved fact. -/