pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.Stability

show as:
view Lean formalization →

This module introduces the d'Alembert defect to measure deviation from the exact d'Alembert functional equation for maps H from reals to reals. Researchers tracing the T5 J-uniqueness argument in the Recognition Science forcing chain would cite these definitions when bounding approximate solutions. The module is a collection of definitions and elementary lemmas with no central theorem.

claimFor a function $H : ℝ → ℝ$, the d'Alembert defect at $(t,u)$ is defined by $Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$. When $Δ_H ≡ 0$, $H$ satisfies the exact d'Alembert equation; when $|Δ_H| ≤ ε$, $H$ is an approximate solution.

background

The module belongs to the Foundation layer and imports Cost together with Cost.FunctionalEquation. The latter supplies lemmas supporting the T5 cost uniqueness proof. Its central object is the defect $Δ_H$ that quantifies departure from the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$, which appears in the Recognition Composition Law context.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The defect definition supplies the starting point for the sibling StabilityHypotheses, StabilityBounds and StabilityEstimate declarations. These feed the T5 J-uniqueness argument in Cost.FunctionalEquation and thereby support the forcing chain from T5 through T8. It corresponds to Definition 7.1 in the paper.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (24)