Safe Complement Gap and Finite Negative Index

Abstract

A concentration-controlled spectral complement has a strict Weil gap and finite negative index.

Theorem 1.1 (Safe-complement gap).

$$\forall Z\in \mathrm{ZeroData}\left(\right),L\in \mathrm{Real}\left(\right),a\in \mathrm{Real}\left(\right),eta\in \mathrm{Real}\left(\right),Q\in \mathrm{Function}\left(\mathrm{WeilTestFunction}\left(\right),\mathrm{Prop}\left(\right)\right),f\in \mathrm{WeilTestFunction}\left(\right),\left(\mathrm{apply}\left(Q,f\right)\wedge \left(\mathrm{tsupport}\left(f\right)\subseteq \mathrm{Icc}\left(\mathrm{neg}\left(L\right),L\right)\wedge \left(\mathrm{SymmetricConvergent}\left(Z,\mathrm{convolutionSquare}\left(f\right)\right)\wedge \left(\mathrm{ArchimedeanConvergent}\left(\mathrm{convolutionSquare}\left(f\right)\right)\wedge \left(\mathrm{Integrable}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{mul}\left(\mathrm{fixedScaleMultiplier}\left(L,xi\right),\mathrm{normSq}\left(\mathrm{fourierLaplace}\left(f,xi\right)\right)\right)\right)\right)\wedge \left(\mathrm{MeasurableSet}\left(\mathrm{setOf}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{fixedScaleMultiplier}\left(L,xi\right)<a\right)\right)\right)\wedge \left(\mathrm{BddBelow}\left(\mathrm{image}\left(\mathrm{fixedScaleMultiplier}\left(L\right),\mathrm{setOf}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{fixedScaleMultiplier}\left(L,xi\right)<a\right)\right)\right)\right)\wedge \left(0<a\wedge \left(0<eta\wedge \left(eta<\mathrm{div}\left(a,\mathrm{add}\left(a,\max \left(0,\mathrm{neg}\left(\mathrm{sInf}\left(\mathrm{image}\left(\mathrm{fixedScaleMultiplier}\left(L\right),\mathrm{setOf}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{fixedScaleMultiplier}\left(L,xi\right)<a\right)\right)\right)\right)\right)\right)\right)\right)\wedge \left(\left(\forall g\in \mathrm{WeilTestFunction}\left(\right),\mathrm{apply}\left(Q,g\right)\Rightarrow \mathrm{mul}\left(\mathrm{div}\left(1,\mathrm{mul}\left(2,\mathrm{pi}\left(\right)\right)\right),\mathrm{integralOn}\left(\mathrm{setOf}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{fixedScaleMultiplier}\left(L,xi\right)<a\right)\right),\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{normSq}\left(\mathrm{fourierLaplace}\left(g,xi\right)\right)\right)\right)\right)\le \mathrm{mul}\left(eta,l2Mass\left(g\right)\right)\right)\wedge \left(\forall g\in \mathrm{WeilTestFunction}\left(\right),\mathrm{apply}\left(Q,g\right)\Rightarrow \mathrm{integral}\left(\mathrm{Real}\left(\right),\mathrm{lambda}\left(\mathrm{typed}\left(x,\mathrm{Real}\left(\right)\right),\mathrm{mul}\left(\cosh \left(\mathrm{div}\left(x,2\right)\right),\mathrm{apply}\left(g,x\right)\right)\right)\right)=0\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(0<\mathrm{sub}\left(a,\mathrm{mul}\left(\mathrm{add}\left(a,\max \left(0,\mathrm{neg}\left(\mathrm{sInf}\left(\mathrm{image}\left(\mathrm{fixedScaleMultiplier}\left(L\right),\mathrm{setOf}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{fixedScaleMultiplier}\left(L,xi\right)<a\right)\right)\right)\right)\right)\right)\right),eta\right)\right)\wedge \mathrm{mul}\left(\mathrm{sub}\left(a,\mathrm{mul}\left(\mathrm{add}\left(a,\max \left(0,\mathrm{neg}\left(\mathrm{sInf}\left(\mathrm{image}\left(\mathrm{fixedScaleMultiplier}\left(L\right),\mathrm{setOf}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{fixedScaleMultiplier}\left(L,xi\right)<a\right)\right)\right)\right)\right)\right)\right),eta\right)\right),l2Mass\left(f\right)\right)\le \mathrm{realPart}\left(\mathrm{zeroSum}\left(Z,\mathrm{convolutionSquare}\left(f\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/SafeComplementFiniteIndex.safe_complement_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the canonical Weil-test carrier, concentration in the dangerous multiplier band and pole orthogonality give the displayed positive gap for the frozen zero-side quadratic form.

Theorem 1.2 (Finite negative-index bound).

$$\forall H\in Type,energy\in \mathrm{Function}\left(H,\mathrm{Real}\left(\right)\right),P\in \mathrm{Submodule}\left(\mathrm{Real}\left(\right),H\right),Q\in \mathrm{Submodule}\left(\mathrm{Real}\left(\right),H\right),delta\in \mathrm{Real}\left(\right),\left(\mathrm{NormedAddCommGroup}\left(H\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathrm{Real}\left(\right),H\right)\wedge \left(\mathrm{FiniteDimensional}\left(\mathrm{Real}\left(\right),P\right)\wedge \left(\mathrm{IsCompl}\left(P,Q\right)\wedge \left(0<delta\wedge \left(\forall q\in H,q\in Q\Rightarrow \mathrm{mul}\left(delta,\mathrm{pow}\left(\mathrm{norm}\left(q\right),2\right)\right)\le \mathrm{apply}\left(energy,q\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{negativeIndex}\left(energy\right)\le \mathrm{withTop}\left(\mathrm{finrank}\left(\mathrm{Real}\left(\right),P\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/SafeComplementFiniteIndex.finite_negative_index_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

A strictly positive complementary subspace prevents a negative subspace from having dimension larger than the retained summand.

References

• Truth anchor: D5/S3/Weil/ZetaBridge/SafeComplementFiniteIndex.finite_negative_index_bound
• Truth anchor: D5/S3/Weil/ZetaBridge/SafeComplementFiniteIndex.safe_complement_gap
• Dependency: D5/S3/Weil/ZetaBridge/FixedScaleWeilQuadraticForm
• Dependency: D5/S3/Weil/ZetaGamma/ArchimedeanJumpDecomposition
• Dependency: D5/S3/Weil/ZetaLinear/ExactStickyReduction