Pith. sign in
module module moderate

IndisputableMonolith.Foundation.DAlembert.Stability

show as:
view Lean formalization →

The module defines the d'Alembert defect measuring deviation from the exact functional equation H(t+u) + H(t-u) = 2 H(t) H(u). Researchers tracing approximate solutions through the T5 cost uniqueness step would cite it when quantifying stability around d'Alembert solutions. The module collects the central definition together with symmetry properties and bound declarations.

claimFor a map $H:\mathbb{R}\to\mathbb{R}$, the defect at $(t,u)$ is $\Delta_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$. The module develops hypotheses and bounds for maps whose defect remains small.

background

Recognition Science derives the J-function from the Recognition Composition Law at T5. The upstream Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. This module adapts the classical d'Alembert equation to the cost setting by introducing the defect that vanishes precisely when H satisfies the equation exactly.

The local theoretical setting is the Foundation layer, where quantitative control of deviations from the functional equation is prepared before error estimates are applied to uniqueness arguments.

proof idea

This is a definition module, no proofs. It states the defect, records its basic algebraic properties through sibling declarations, and declares the hypotheses and bound objects needed for later stability work.

why it matters in Recognition Science

The module supplies the defect measure required for stability control inside the T5 J-uniqueness argument of the forcing chain. It operationalizes Definition 7.1 so that approximate solutions can be bounded before the uniqueness step is closed.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (24)