SatisfiesDAlembert
The declaration defines the d'Alembert functional equation as the property that a map H from reals to reals obeys H(t+u) + H(t-u) = 2 H(t) H(u) for all real t and u. Number theorists and Recognition Science researchers working on the J-cost to zeta parallel in PrimeLedgerStructure cite it when linking ledger irreducibility to functional equations. The definition is a direct predicate encoding the additive form of the equation with no proof obligations.
claimA function $H : {R} {to} {R}$ satisfies the d'Alembert functional equation when $H(t+u) + H(t-u) = 2 H(t) H(u)$ holds for all real numbers $t$ and $u$.
background
The PrimeLedgerStructure module treats natural numbers as multiplicative ledger transactions, with primes as the irreducible entries whose unique factorization supplies the balance sheet. The d'Alembert equation is introduced here to force zeros of solutions onto lines, providing the structural parallel between J-cost symmetry and the zeta functional equation. Upstream, the shifted cost H(x) = J(x) + 1 from CostAlgebra converts the Recognition Composition Law into the standard d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y); the log substitution then yields the additive version defined in this module. The FourthGate upstream version augments the predicate with the normalization H(0) = 1, while this module isolates the core equation alone.
proof idea
This is a direct definition of the predicate. It encodes the standard d'Alembert functional equation without the normalization H(0) = 1 present in the FourthGate version.
why it matters in Recognition Science
The definition supplies the core property invoked by the d'Alembert classification theorem, the unit-calibration corollary that forces H = cosh, and the result that d'Alembert structure plus calibration yields G = cosh - 1, all in FourthGate. It anchors the ledger-conservation argument that predicts the Riemann Hypothesis from the J-cost to zeta correspondence. The module doc flags the open gap: whether the Euler product imposes d'Alembert-type constraints on the completed zeta function.
scope and limits
- Does not enforce the normalization H(0) = 1.
- Does not assume smoothness or differentiability of H.
- Does not derive the explicit solution form cosh.
- Does not address prime factorization or ledger transactions directly.
formal statement (Lean)
56def SatisfiesDAlembert (H : ℝ → ℝ) : Prop :=
proof body
Definition body.
57 ∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u
58
59/-- cosh satisfies the d'Alembert equation. -/