`j_positive_off_fixed_point`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.PrimeLedgerStructure
domain: NumberTheory
line: 176 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.PrimeLedgerStructure on GitHub at line 176.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 204completed zeta function Ξ(t) = ξ(1/2 + it) satisfies a
 205d'Alembert-type constraint from the Euler product structure.
 206

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.