j_positive_off_fixed_point
J-cost is strictly positive for every positive real except the fixed point at one. Researchers formalizing the recognition ledger's multiplicative bounds cite this when establishing cost positivity away from equilibrium. The proof is a direct one-line application of the underlying J-cost positivity lemma.
claimFor every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
In Recognition Science the J-cost function quantifies deviation from the multiplicative fixed point in the discrete ledger. The PrimeLedgerStructure module treats natural numbers as transactions, with primes as irreducible entries, and shows that the cost function obeys the d'Alembert equation whose solutions have zeros confined to lines. The present theorem supplies the elementary positivity fact needed before the structural identification between J-cost symmetry and the zeta functional equation can be stated.
proof idea
The proof is a one-line wrapper that applies the lemma Cost.Jcost_pos_of_ne_one directly to the hypotheses 0 < x and x ≠ 1.
why it matters in Recognition Science
The result is a prerequisite for the d'Alembert satisfaction theorems that underwrite the RS prediction of the Riemann Hypothesis (critical line as ledger balance). It closes the basic positivity step in the chain from T5 J-uniqueness through the reciprocal symmetry J(x) = J(1/x) to the structural parallel with the completed zeta function.
scope and limits
- Does not claim positivity at the fixed point x = 1.
- Does not address negative reals or complex arguments.
- Does not quantify the growth rate of J-cost away from unity.
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. -/