structural_parallel_certificate
plain-language theorem explainer
The theorem assembles five properties of J-cost that parallel the functional equation of the Riemann zeta function: inversion symmetry, unique zero at the fixed point, strict positivity off that point, satisfaction of d'Alembert's equation after exponential change of variable, and the multiplicative composition identity. Number theorists exploring Recognition Science's ledger interpretation of primes cite this when mapping cost functions onto zeta-like behavior. It is proved by direct conjunction of five prior lemmas on J-cost symmetry, zero, d
Claim. The J-cost function on positive reals satisfies $J(x)=J(x^{-1})$, $J(1)=0$, $J(x)>0$ whenever $x>0$ and $x≠1$, the auxiliary function $H(t)=J(e^t)+1$ obeys d'Alembert's equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and the identity $J(xy)+J(x/y)=2J(x)+2J(y)+2J(x)J(y)$ holds for all $x,y>0$.
background
In the Recognition Science ledger model, natural numbers represent multiplicative transactions and primes are the irreducible ones. The J-cost function, defined via $J(x)=(x-1)^2/(2x)$, encodes the cost of such transactions. SatisfiesDAlembert is the functional equation ∀t,u. H(t+u)+H(t-u)=2Ht⋅Hu. Upstream lemmas establish J-cost symmetry under inversion, its vanishing at unity, positivity away from unity, and the d'Alembert identity J(xy)+J(x/y)=2J(x)+2J(y)+2J(x)J(y).
proof idea
The proof is a term-mode conjunction that directly invokes five lemmas: Jcost_symm for inversion symmetry, Jcost_unit0 for the zero at 1, Jcost_pos_of_ne_one for positivity off the fixed point, rs_cost_satisfies_dalembert for the d'Alembert property of the shifted exponential, and dalembert_identity for the multiplicative relation.
why it matters
This declaration supplies the MODEL of the structural parallel between J-cost and the zeta functional equation, as described in the module documentation. It feeds the downstream theorem j_positive_off_fixed_point. Within the framework it connects the T5 J-uniqueness and the d'Alembert forcing of zero confinement to the ledger view of primes, supporting the hypothesis that ledger conservation implies the Riemann Hypothesis. The module notes that the gap whether the Euler product imposes d'Alembert-type constraints remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.