dAlembert_status
plain-language theorem explainer
The dAlembert_status entry registers the d'Alembert functional equation as a standard mathematical fact whose continuous solutions satisfying the given initial conditions are the hyperbolic cosine. Researchers deriving the J-cost function or invoking the recognition composition law in the forcing chain would reference this classification. The entry is realized as a direct string assignment that tags the fact for the module's axiom registry table.
Claim. The continuous solutions $H:ℝ→ℝ$ to the functional equation $H(t+u)+H(t-u)=2H(t)H(u)$ with initial conditions $H(0)=1$ and $H''(0)=1$ are given by $H(t)=cosh(t)$.
background
The Meta.Axioms module maintains a registry that partitions claims into physical postulates, well-known mathematical facts, and open problems. This entry is listed under mathematical facts and points to Aczél (1966) for the d'Alembert equation. The local setting draws on the Cost and Status abbreviations from RSNative.Core together with the recognition composition law that forces the J-function to take the cosh form.
proof idea
The declaration is a one-line definition that returns the string classifying the equation as a mathematical fact. No lemmas are applied and no tactics are used.
why it matters
The entry populates the axiom registry table in the module documentation, specifically marking the d'Alembert result as a standard fact from Aczél (1966). It supports the T5 J-uniqueness step in the unified forcing chain by justifying the cosh realization of J under the recognition composition law. The declaration has zero downstream uses in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.