Finite Weyl Budget Bounds

Abstract

Finite parity pencils converge monotonically to the full generalized Rayleigh budget interval.

Theorem 1.1 (Finite Hermitian pencils bound and approximate the full budget interval).

$$\forall EvenTest\in Type,OddTest\in Type,evenDim\in \mathrm{Nat}\left(\right)\to \mathrm{Nat}\left(\right),oddDim\in \mathrm{Nat}\left(\right)\to \mathrm{Nat}\left(\right),evenBase\in \mathrm{DependentMap}\left(N:\mathrm{Nat}\left(\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(\mathrm{apply}\left(evenDim,N\right)\right),\mathrm{Fin}\left(\mathrm{apply}\left(evenDim,N\right)\right),\mathrm{Complex}\left(\right)\right)\right),oddBase\in \mathrm{DependentMap}\left(N:\mathrm{Nat}\left(\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(\mathrm{apply}\left(oddDim,N\right)\right),\mathrm{Fin}\left(\mathrm{apply}\left(oddDim,N\right)\right),\mathrm{Complex}\left(\right)\right)\right),evenBoundary\in \mathrm{DependentMap}\left(N:\mathrm{Nat}\left(\right),\mathrm{Fin}\left(\mathrm{apply}\left(evenDim,N\right)\right)\to \mathrm{Complex}\left(\right)\right),oddBoundary\in \mathrm{DependentMap}\left(N:\mathrm{Nat}\left(\right),\mathrm{Fin}\left(\mathrm{apply}\left(oddDim,N\right)\right)\to \mathrm{Complex}\left(\right)\right),fullEvenBase\in EvenTest\to \mathrm{Real}\left(\right),fullEvenBoundary\in EvenTest\to \mathrm{Complex}\left(\right),fullOddBase\in OddTest\to \mathrm{Real}\left(\right),fullOddBoundary\in OddTest\to \mathrm{Complex}\left(\right),referenceBudget\in \mathrm{Real}\left(\right),\mathrm{let}finiteEvenQuotients=N:\mathrm{Nat}\left(\right)\mapsto \left\{\exists x\in \mathrm{Fin}\left(\mathrm{apply}\left(evenDim,N\right)\right)\to \mathrm{Complex}\left(\right),\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(evenBoundary,N\right)\right),x\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{neg}\left(\mathrm{Re}\left(\mathrm{dot}\left(\mathrm{star}\left(x\right),\mathrm{mulVec}\left(\mathrm{apply}\left(evenBase,N\right),x\right)\right)\right)\right),\mathrm{normSq}\left(\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(evenBoundary,N\right)\right),x\right)\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\},\mathrm{let}finiteOddQuotients=N:\mathrm{Nat}\left(\right)\mapsto \left\{\exists x\in \mathrm{Fin}\left(\mathrm{apply}\left(oddDim,N\right)\right)\to \mathrm{Complex}\left(\right),\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(oddBoundary,N\right)\right),x\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{Re}\left(\mathrm{dot}\left(\mathrm{star}\left(x\right),\mathrm{mulVec}\left(\mathrm{apply}\left(oddBase,N\right),x\right)\right)\right),\mathrm{normSq}\left(\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(oddBoundary,N\right)\right),x\right)\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\},\mathrm{let}fullEvenQuotients=\left\{\exists x\in EvenTest,\mathrm{apply}\left(fullEvenBoundary,x\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{neg}\left(\mathrm{apply}\left(fullEvenBase,x\right)\right),\mathrm{normSq}\left(\mathrm{apply}\left(fullEvenBoundary,x\right)\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\},\mathrm{let}fullOddQuotients=\left\{\exists x\in OddTest,\mathrm{apply}\left(fullOddBoundary,x\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{apply}\left(fullOddBase,x\right),\mathrm{normSq}\left(\mathrm{apply}\left(fullOddBoundary,x\right)\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\},\mathrm{let}finiteLower=N:\mathrm{Nat}\left(\right)\mapsto \mathrm{add}\left(referenceBudget,\mathrm{sSup}\left(\mathrm{apply}\left(finiteEvenQuotients,N\right)\right)\right),\mathrm{let}finiteUpper=N:\mathrm{Nat}\left(\right)\mapsto \mathrm{add}\left(referenceBudget,\mathrm{sInf}\left(\mathrm{apply}\left(finiteOddQuotients,N\right)\right)\right),\mathrm{let}fullLower=\mathrm{add}\left(referenceBudget,\mathrm{sSup}\left(fullEvenQuotients\right)\right),\mathrm{let}fullUpper=\mathrm{add}\left(referenceBudget,\mathrm{sInf}\left(fullOddQuotients\right)\right),\mathrm{let}evenPencil=N:\mathrm{Nat}\left(\right),R:\mathrm{Real}\left(\right)\mapsto \mathrm{add}\left(\mathrm{apply}\left(evenBase,N\right),\mathrm{smul}\left(\mathrm{ofReal}\left(\mathrm{sub}\left(R,referenceBudget\right)\right),\mathrm{vecMulVec}\left(\mathrm{apply}\left(evenBoundary,N\right),\mathrm{star}\left(\mathrm{apply}\left(evenBoundary,N\right)\right)\right)\right)\right),\mathrm{let}oddPencil=N:\mathrm{Nat}\left(\right),R:\mathrm{Real}\left(\right)\mapsto \mathrm{sub}\left(\mathrm{apply}\left(oddBase,N\right),\mathrm{smul}\left(\mathrm{ofReal}\left(\mathrm{sub}\left(R,referenceBudget\right)\right),\mathrm{vecMulVec}\left(\mathrm{apply}\left(oddBoundary,N\right),\mathrm{star}\left(\mathrm{apply}\left(oddBoundary,N\right)\right)\right)\right)\right),\mathrm{let}feasible=N:\mathrm{Nat}\left(\right),R:\mathrm{Real}\left(\right)\mapsto \mathrm{PosSemidef}\left(\mathrm{applyTwo}\left(evenPencil,N,R\right)\right)\wedge \mathrm{PosSemidef}\left(\mathrm{applyTwo}\left(oddPencil,N,R\right)\right),\left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{IsHermitian}\left(\mathrm{apply}\left(evenBase,N\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{IsHermitian}\left(\mathrm{apply}\left(oddBase,N\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),x\in \mathrm{Fin}\left(\mathrm{apply}\left(evenDim,N\right)\right)\to \mathrm{Complex}\left(\right),\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(evenBoundary,N\right)\right),x\right)=0\Rightarrow 0\le \mathrm{Re}\left(\mathrm{dot}\left(\mathrm{star}\left(x\right),\mathrm{mulVec}\left(\mathrm{apply}\left(evenBase,N\right),x\right)\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),x\in \mathrm{Fin}\left(\mathrm{apply}\left(oddDim,N\right)\right)\to \mathrm{Complex}\left(\right),\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(oddBoundary,N\right)\right),x\right)=0\Rightarrow 0\le \mathrm{Re}\left(\mathrm{dot}\left(\mathrm{star}\left(x\right),\mathrm{mulVec}\left(\mathrm{apply}\left(oddBase,N\right),x\right)\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\exists x\in \mathrm{Fin}\left(\mathrm{apply}\left(evenDim,N\right)\right)\to \mathrm{Complex}\left(\right),\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(evenBoundary,N\right)\right),x\right)\ne 0\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\exists x\in \mathrm{Fin}\left(\mathrm{apply}\left(oddDim,N\right)\right)\to \mathrm{Complex}\left(\right),\mathrm{dot}\left(\mathrm{star}\left(\mathrm{apply}\left(oddBoundary,N\right)\right),x\right)\ne 0\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{BddAbove}\left(\mathrm{apply}\left(finiteEvenQuotients,N\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{BddBelow}\left(\mathrm{apply}\left(finiteOddQuotients,N\right)\right)\right)\wedge \left(\left(\exists x\in EvenTest,\mathrm{apply}\left(fullEvenBoundary,x\right)\ne 0\right)\wedge \left(\left(\exists x\in OddTest,\mathrm{apply}\left(fullOddBoundary,x\right)\ne 0\right)\wedge \left(\mathrm{BddAbove}\left(fullEvenQuotients\right)\wedge \left(\mathrm{BddBelow}\left(fullOddQuotients\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{Subset}\left(\mathrm{apply}\left(finiteEvenQuotients,N\right),\mathrm{apply}\left(finiteEvenQuotients,\mathrm{add}\left(N,1\right)\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{Subset}\left(\mathrm{apply}\left(finiteOddQuotients,N\right),\mathrm{apply}\left(finiteOddQuotients,\mathrm{add}\left(N,1\right)\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{Subset}\left(\mathrm{apply}\left(finiteEvenQuotients,N\right),fullEvenQuotients\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{Subset}\left(\mathrm{apply}\left(finiteOddQuotients,N\right),fullOddQuotients\right)\right)\wedge \left(\left(\forall q\in \mathrm{Real}\left(\right),epsilon\in \mathrm{Real}\left(\right),\left(\mathrm{Mem}\left(q,fullEvenQuotients\right)\wedge 0<epsilon\right)\Rightarrow \left(\exists N\in \mathrm{Nat}\left(\right),qN\in \mathrm{Real}\left(\right),\mathrm{Mem}\left(qN,\mathrm{apply}\left(finiteEvenQuotients,N\right)\right)\wedge \mathrm{sub}\left(q,epsilon\right)<qN\right)\right)\wedge \left(\forall q\in \mathrm{Real}\left(\right),epsilon\in \mathrm{Real}\left(\right),\left(\mathrm{Mem}\left(q,fullOddQuotients\right)\wedge 0<epsilon\right)\Rightarrow \left(\exists N\in \mathrm{Nat}\left(\right),qN\in \mathrm{Real}\left(\right),\mathrm{Mem}\left(qN,\mathrm{apply}\left(finiteOddQuotients,N\right)\right)\wedge qN<\mathrm{add}\left(q,epsilon\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\left(\forall N\in \mathrm{Nat}\left(\right),R\in \mathrm{Real}\left(\right),\mathrm{IsHermitian}\left(\mathrm{applyTwo}\left(evenPencil,N,R\right)\right)\wedge \mathrm{IsHermitian}\left(\mathrm{applyTwo}\left(oddPencil,N,R\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),R\in \mathrm{Real}\left(\right),\mathrm{Iff}\left(\mathrm{PosSemidef}\left(\mathrm{applyTwo}\left(evenPencil,N,R\right)\right),\mathrm{apply}\left(finiteLower,N\right)\le R\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),R\in \mathrm{Real}\left(\right),\mathrm{Iff}\left(\mathrm{PosSemidef}\left(\mathrm{applyTwo}\left(oddPencil,N,R\right)\right),R\le \mathrm{apply}\left(finiteUpper,N\right)\right)\right)\wedge \left(\mathrm{Monotone}\left(finiteLower\right)\wedge \left(\mathrm{Antitone}\left(finiteUpper\right)\wedge \left(\mathrm{Tendsto}\left(finiteLower,atTop,\mathrm{nhds}\left(fullLower\right)\right)\wedge \left(\mathrm{Tendsto}\left(finiteUpper,atTop,\mathrm{nhds}\left(fullUpper\right)\right)\wedge \left(\left(\forall N\in \mathrm{Nat}\left(\right),R\in \mathrm{Real}\left(\right),\mathrm{Iff}\left(\mathrm{applyTwo}\left(feasible,N,R\right),\mathrm{MemIcc}\left(R,\mathrm{apply}\left(finiteLower,N\right),\mathrm{apply}\left(finiteUpper,N\right)\right)\right)\right)\wedge \left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{apply}\left(finiteUpper,N\right)<\mathrm{apply}\left(finiteLower,N\right)\Rightarrow \left(\left(\forall R\in \mathrm{Real}\left(\right),\mathrm{PosSemidef}\left(\mathrm{applyTwo}\left(evenPencil,N,R\right)\right)\Rightarrow \mathrm{apply}\left(finiteLower,N\right)\le R\right)\wedge \left(\left(\forall R\in \mathrm{Real}\left(\right),\mathrm{PosSemidef}\left(\mathrm{applyTwo}\left(oddPencil,N,R\right)\right)\Rightarrow R\le \mathrm{apply}\left(finiteUpper,N\right)\right)\wedge \mathrm{Not}\left(\exists R\in \mathrm{Real}\left(\right),\mathrm{applyTwo}\left(feasible,N,R\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/FiniteWeylBudgetBounds.finite_weyl_budget_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement constructs both finite quotient families, their endpoints, the two rank-one pencils, and finite feasibility directly from the matrix and boundary data.

Kernel positivity handles zero boundary pairings. Nested finite quotient sets and one-sided approximation of every full quotient express the Galerkin density hypothesis without assuming endpoint convergence.

Each finite pencil is positive semidefinite exactly on its corresponding budget ray. The lower endpoints increase, the upper endpoints decrease, both converge to the full interval, and a crossed finite interval supplies incompatible lower and upper requirements.

References

• Truth anchor: D5/S3/Weil/Budget/FiniteWeylBudgetBounds.finite_weyl_budget_bounds
• Dependency: D5/S3/Weil/Budget/OddTestBudgetUpperBound