rs_cost_satisfies_dalembert
plain-language theorem explainer
The RS cost function lifted via H(t) = Jcost(exp t) + 1 satisfies the d'Alembert functional equation for all real t and u. Number theorists modeling ledger conservation and the Riemann Hypothesis prediction in Recognition Science cite this result. The proof substitutes the explicit cosh form of Jcost and verifies the addition formula by direct algebraic reduction.
Claim. Let $H(t) = J(e^t) + 1$, where $J$ is the RS cost function. Then $H$ satisfies $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$.
background
In the PrimeLedgerStructure module, natural numbers are modeled as transactions on a discrete multiplicative ledger, with primes as the irreducible entries. The d'Alembert structure is the property that a real function H obeys the functional equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t,u. Upstream, the lemma Jcost_exp_cosh states that Jcost(exp t) = cosh t - 1, which directly identifies the lifted RS cost with the hyperbolic cosine.
proof idea
The term proof introduces t and u, simplifies via the Jcost_exp_cosh lemma to obtain cosh t, rewrites using the addition and subtraction formulas for cosh, and finishes by ring normalization.
why it matters
This theorem proves the d'Alembert zero structure for the RS cost function, a required step in the module's ledger-based approach to the zeta functional equation. It is invoked by j_positive_off_fixed_point and structural_parallel_certificate to establish symmetry and positivity properties that parallel the completed zeta function. In the Recognition Science framework it supports the proved claim that d'Alembert structure forces zeros onto lines, as listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.