SatisfiesDAlembert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.