Operator-valued scattering for the one-dimensional wave equation with memory

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Let a medium $M$ consist of positive real numbers $R$, $T$, and $\gamma$, and a function $a:\mathbb R_x\times\mathbb R_t\to\mathbb C$ with the following properties: $a(x,t)=0$ whenever $|x|>R$ or $|t|>T$; for every $t$, the map $x\mapsto a(x,t)$ is strongly measurable; for every $x$, the map $t\mapsto a(x,t)$ is smooth; and for every derivative order $k$ there is a finite nonnegative bound, independent of $x$ and $t$, for $|\partial_t^ka(x,t)|$.

Put $\mathbb C_+=\{z:\operatorname{Im}z>0\}$. Represent a scalar frequency signal by a function $f:\mathbb C\to\mathbb C$ that vanishes outside $\mathbb C_+$. For $\alpha\in\mathbb R$, define

$$E_\alpha(h)=\sup_{\sigma>0}e^{-2\sigma\alpha} \int_{\mathbb R}|h(\lambda+i\sigma)|^2\,d\lambda,$$

and let $\mathcal H_\alpha$ be the holomorphic signals with $E_\alpha(h)<\infty$. Say that $f\in(z+i)^{-1}\mathcal H_\alpha$ when $(z+i)f(z)\in\mathcal H_\alpha$, and that $h\in z^{-1}\mathcal H_\beta$ when $zh(z)\in\mathcal H_\beta$.

For every real $R_1>R$, there exist complex-linear maps $T,R_+$ on frequency signals and complex-linear maps $\mathcal T,\mathcal R_+$ on time signals, all chosen before $\alpha$, with the following properties.

1. For each $L\in\{T,R_+\}$ and each $\alpha\in\mathbb R$, there is a finite constant $C_{L,\alpha}\ge0$ such that every $f\in(z+i)^{-1}\mathcal H_\alpha$ satisfies $Lf\in z^{-1}\mathcal H_{\alpha+2R_1}$ and

$$E_{\alpha+2R_1}(zLf)\le C_{L,\alpha}E_\alpha((z+i)f).$$

2. For each such $\alpha$ and $f$, there exists a frequency field $v(x,z)$, holomorphic in $z\in\mathbb C_+$ and locally in $z^{-1}\mathcal H_\beta$ in $x$ for some weight $\beta$, that solves weakly

$$\left(D_x^2-z^2+A_M(x)\right)v=0, \qquad (A_M(x)v)(z)=\frac1{2\pi}\int_{\mathbb R} \widehat a(x,z_{\mathrm{re}}-\lambda) \frac{\lambda+i\operatorname{Im}z}{\lambda+i\operatorname{Im}z+i\gamma} v(x,\lambda+i\operatorname{Im}z)\,d\lambda,$$

where $D_x=-i\partial_x$ and $\widehat a(x,\nu)=\int e^{i\nu t}a(x,t)\,dt$. The convolution is absolutely Bochner integrable on every upper-half-plane slice, and

$$v(x,z)= \begin{cases} f(z)e^{izx}+(R_+f)(z)e^{-izx},&x<-R,\\ (Tf)(z)e^{izx},&x>R. \end{cases}$$

Any other weak frequency field satisfying the same equation and exterior identities agrees with $v$ almost everywhere in $x$ for every $z\in\mathbb C_+$.

3. A time datum $g:\mathbb R\to\mathbb C$ is admissible when it is smooth, compactly supported with topological support contained in $(R,\infty)$, and its Fourier–Laplace integral $\widehat g(z)=\int_{\mathbb R}e^{izt}g(t)\,dt$ is absolutely integrable for every $z\in\mathbb C_+$. For every admissible $g$, both $\mathcal Tg$ and $\mathcal R_+g$ have such transforms and

$$\widehat{\mathcal Tg}(z)=T(\widehat g)(z),\qquad \widehat{\mathcal R_+g}(z)=R_+(\widehat g)(z) \quad(z\in\mathbb C_+).$$

4. For every admissible $g$, there is an energy field $u$ with value in $C_tH_x^1$, time derivative in $C_tL_x^2$, and named weak time and space derivatives, satisfying the causal memory equation

$$D_t^2u-a(x,t)\int_{-\infty}^{t}e^{-\gamma(t-s)}D_tu(s,x)\,ds-D_x^2u=0$$

in the weak spacetime sense, with $u(t,x)=g(t-x)$ for every $t<0$. It has the exterior representation

$$u(t,x)= \begin{cases} g(t-x)+(\mathcal R_+g)(t+x),&x<-R,\\ (\mathcal Tg)(t-x),&x>R, \end{cases}$$

for all $t$, and it is unique among causal energy solutions modulo almost-everywhere equality of the value and both weak derivatives on every time slice.

The statement identifies a single frequency scattering pair and its time-domain realization, simultaneously for every Hardy weight and every exterior cutoff $R_1>R$.

Formalization Note The total integral operators are always accompanied by explicit measurability and integrability conditions. Frequency functions use canonical zero extension away from $\mathbb C_+$, and Sobolev solutions are compared by their natural almost-everywhere equivalence rather than by arbitrary pointwise representatives.

Why this node was retired

The posted statement is

noncomputable section

namespace ScatteringMain

open ScatteringInterfaces

theorem operatorValuedScattering (M : Medium) :
    OperatorValuedScatteringProblem M := by sorry

end ScatteringMain

FrequencyLocal requires one exponential Hardy weight β to control every spatial radius ρ, incompatible with the prescribed incoming wave even in the free medium.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Replace ∃β ∀ρ>0 by ∀ρ>0 ∃β(ρ) in the local weighted Hardy condition, retaining a finite bound for that fixed spatial window. Recheck all downstream mapping and scattering conclusions against the original source.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.

import Definitions.Def_frame_2026_scattering_interfaces

noncomputable section

namespace ScatteringMain

open ScatteringInterfaces

theorem operatorValuedScattering (M : Medium) :
    OperatorValuedScatteringProblem M := by sorry

end ScatteringMain