Bode-Width Criterion

Abstract

Finite mirror-paired widths produce the same critical-line, area, and curvature defect.

Theorem 1.1 (Finite width, displacement, and damping defects coincide).

$$\begin{gathered} \forall I:Type,\mathrm{Fintype}\left(I\right),delta:I\to \mathbb{R}, \\ \forall i\in I,0\le \mathrm{delta}\left(i\right)\wedge \mathrm{delta}\left(i\right)\le \frac{1}{2}\Rightarrow \\ \mathrm{let}C:=\forall i\in I,\frac{1}{2}+\mathrm{delta}\left(i\right)=\frac{1}{2}\wedge \frac{1}{2}-\mathrm{delta}\left(i\right)=\frac{1}{2}, \\ \mathrm{let}W(y):=\sum _{i\in I}\max (\mathrm{delta}\left(i\right)-\left|y-\frac{1}{2}\right|,0), \\ \mathrm{let}A:={\int }_0^{\infty }W\left(y\right)dy, \\ \mathrm{let}S:=\sum _{i\in I}{\frac{1}{2}+\mathrm{delta}\left(i\right)-\frac{1}{2}}^2+{\frac{1}{2}-\mathrm{delta}\left(i\right)-\frac{1}{2}}^2, \\ \mathrm{let}R(tau):=\sum _{i\in I}2\cdot \cosh \left(tau\cdot \mathrm{delta}\left(i\right)\right)-1, \\ C\iff \forall y\in \mathbb{R},y>0\Rightarrow W\left(y\right)=0\wedge \forall y\in \mathbb{R},y>0\Rightarrow W\left(y\right)=0\iff A=0\wedge A=\frac{1}{2}\cdot S\wedge A=\frac{1}{2}\cdot \mathrm{deriv}\left(\mathrm{deriv}\left(R\right),0\right) \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Scattering/BodeWidthCriterion.bode_width_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source finite window is encoded by nonnegative mirror-pair widths delta bounded by one half. Each pair contributes the displayed triangular pulse. Its integral is delta squared, while the two mirrored real-part displacements contribute twice delta squared. Twice differentiating the finite cosh partition gives the same sum.

References

• Truth anchor: D5/S3/Weil/Scattering/BodeWidthCriterion.bode_width_criterion