dAlembert_locally_bounded
plain-language theorem explainer
Continuous real-valued functions are locally bounded on every closed bounded interval. This lemma serves as step H2 in the bootstrap for Aczél's classification of continuous d'Alembert solutions. The proof applies the extreme value theorem to |H| on the compact interval [-R, R] via IsCompact.exists_isMaxOn.
Claim. Let $H:ℝ→ℝ$ be continuous. Then for every $R>0$ there exists $M∈ℝ$ such that $|H(t)|≤M$ whenever $|t|≤R$.
background
The module establishes that every continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^∞$, yielding the classification $H(t)=1$, $H(t)=cosh(λt)$, or $H(t)=cos(λt)$. The function $H$ is the shifted cost arising from the Recognition Composition Law: upstream CostAlgebra defines $H(x)=J(x)+1=½(x+x^{-1})$, which satisfies the multiplicative form $H(xy)+H(x/y)=2H(x)H(y)$; FunctionalEquation reparametrizes it to the additive d'Alembert equation used here.
proof idea
Term-mode proof that directly invokes the extreme value theorem. It calls IsCompact.exists_isMaxOn on the compact set Icc (-R) R (using Set.nonempty_Icc and h_cont.abs.continuousOn), obtains a maximizer x of |H|, and sets M=|H x| to bound |H t| for all |t|≤R by the attained-maximum property.
why it matters
This is H2 in the integration-bootstrap strategy of the Aczél theorem, supplying local boundedness that enables the representation formula Φ(t+δ)−Φ(t−δ) and the subsequent C^1 to C^∞ regularity ascent. It discharges the former H_AczelClassification hypothesis in the IndisputableMonolith codebase. Within Recognition Science it underpins the derivation of smooth solutions to the cost functional equation that feed the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.