Weil Rayleigh Enclosure Mode Capture
Abstract
Two-sided Rayleigh enclosure and codimension-one coercivity capture the ground eigendirection without requiring a small operator residual.
D is a real linear operator domain, iota:D->H is its embedding into a real Hilbert space and A:D->H is a symmetric operator action on that domain. The theorem is therefore compatible with an unbounded Friedrichs realization rather than replacing it by a bounded matrix. The arithmetic application must separately establish the real-invariant domain bridge for the canonical Weil form.
Theorem 1.1 (A certified Rayleigh interval captures the ground line).
Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/WeilRayleighEnclosureModeCapture.rayleigh_enclosure_mode_capture (✓ std3). ∎
Source. Repository-derived.
Commentary.
Write alpha=<k,u> and v=u-alphak. Symmetry and the eigenvalue equation give the exact identity q(v)=lambda||v||^2 +alpha^2*(q(k)-lambda). Cauchy-Schwarz gives alpha^2<=1. The coercive lower bound on k-perp then yields (T-M)||v||^2<=M-ell. This replaces the usual residual/gap quantity by three values directly exposed by a Schur or LDL certificate: a ground lower bound ell, a candidate upper bound M and a complementary threshold T. No claim about an unbounded-scale Xi limit is made by this theorem itself.