Parity Weyl Interval

Abstract

The affine even and odd channels determine a coordinate-independent resolvent interval and its positive spectral completions.

Theorem 1.1 (Parity Weyl interval).

$$\forall Even\in Type,Odd\in Type,Source\in Type,evenBase\in Even\to \mathrm{Real}\left(\right),evenBoundary\in Even\to \mathrm{Real}\left(\right),oddBase\in Odd\to \mathrm{Real}\left(\right),oddBoundary\in Odd\to \mathrm{Real}\left(\right),referenceBudget\in \mathrm{Real}\left(\right),source\in Source,spectralReading\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to Source,resolventMoment\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to \mathrm{Real}\left(\right),\left(\left(\forall e\in Even,0\le \mathrm{apply}\left(evenBoundary,e\right)\right)\wedge \left(\left(\forall o\in Odd,0\le \mathrm{apply}\left(oddBoundary,o\right)\right)\wedge \left(\left(\forall e\in Even,\mathrm{apply}\left(evenBoundary,e\right)=0\Rightarrow 0\le \mathrm{apply}\left(evenBase,e\right)\right)\wedge \left(\left(\forall o\in Odd,\mathrm{apply}\left(oddBoundary,o\right)=0\Rightarrow 0\le \mathrm{apply}\left(oddBase,o\right)\right)\wedge \left(\left(\exists e\in Even,\mathrm{apply}\left(evenBoundary,e\right)\ne 0\right)\wedge \left(\left(\exists o\in Odd,\mathrm{apply}\left(oddBoundary,o\right)\ne 0\right)\wedge \left(\mathrm{BddAbove}\left(\left\{\exists e\in Even,\mathrm{apply}\left(evenBoundary,e\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{neg}\left(\mathrm{apply}\left(evenBase,e\right)\right),\mathrm{apply}\left(evenBoundary,e\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\}\right)\wedge \mathrm{BddBelow}\left(\left\{\exists o\in Odd,\mathrm{apply}\left(oddBoundary,o\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{apply}\left(oddBase,o\right),\mathrm{apply}\left(oddBoundary,o\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\}\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}evenRatios=\left\{\exists e\in Even,\mathrm{apply}\left(evenBoundary,e\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{neg}\left(\mathrm{apply}\left(evenBase,e\right)\right),\mathrm{apply}\left(evenBoundary,e\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\},\mathrm{let}oddRatios=\left\{\exists o\in Odd,\mathrm{apply}\left(oddBoundary,o\right)\ne 0\wedge q=\mathrm{div}\left(\mathrm{apply}\left(oddBase,o\right),\mathrm{apply}\left(oddBoundary,o\right)\right)\mid q\in \mathrm{Real}\left(\right)\right\},\mathrm{let}lower=\mathrm{add}\left(referenceBudget,\mathrm{sSup}\left(evenRatios\right)\right),\mathrm{let}upper=\mathrm{add}\left(referenceBudget,\mathrm{sInf}\left(oddRatios\right)\right),\mathrm{let}admissible=R:\mathrm{Real}\left(\right)\mapsto 0\le R\wedge \left(\left(\forall e\in Even,0\le \mathrm{add}\left(\mathrm{apply}\left(evenBase,e\right),\mathrm{mul}\left(\mathrm{sub}\left(R,referenceBudget\right),\mathrm{apply}\left(evenBoundary,e\right)\right)\right)\right)\wedge \left(\forall o\in Odd,0\le \mathrm{sub}\left(\mathrm{apply}\left(oddBase,o\right),\mathrm{mul}\left(\mathrm{sub}\left(R,referenceBudget\right),\mathrm{apply}\left(oddBoundary,o\right)\right)\right)\right)\right),\mathrm{let}shiftedAdmissible=delta:\mathrm{Real}\left(\right)\mapsto R:\mathrm{Real}\left(\right)\mapsto 0\le R\wedge \left(\left(\forall e\in Even,0\le \mathrm{add}\left(\mathrm{add}\left(\mathrm{apply}\left(evenBase,e\right),\mathrm{mul}\left(delta,\mathrm{apply}\left(evenBoundary,e\right)\right)\right),\mathrm{mul}\left(\mathrm{sub}\left(R,\mathrm{add}\left(referenceBudget,delta\right)\right),\mathrm{apply}\left(evenBoundary,e\right)\right)\right)\right)\wedge \left(\forall o\in Odd,0\le \mathrm{sub}\left(\mathrm{sub}\left(\mathrm{apply}\left(oddBase,o\right),\mathrm{mul}\left(delta,\mathrm{apply}\left(oddBoundary,o\right)\right)\right),\mathrm{mul}\left(\mathrm{sub}\left(R,\mathrm{add}\left(referenceBudget,delta\right)\right),\mathrm{apply}\left(oddBoundary,o\right)\right)\right)\right)\right),\mathrm{let}completion=R:\mathrm{Real}\left(\right)\mapsto \exists nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{map}\left((x:\mathrm{Real}\left(\right)\mapsto \mathrm{neg}\left(x\right)),nu\right)=nu\wedge \left(\mathrm{apply}\left(spectralReading,nu\right)=source\wedge \mathrm{apply}\left(resolventMoment,nu\right)=R\right),\left(\forall R\in \mathrm{Real}\left(\right),\mathrm{apply}\left(admissible,R\right)\iff R\in \mathrm{Icc}\left(\max \left(0,lower\right),upper\right)\right)\wedge \left(\left(lower>upper\Rightarrow \left(\neg \left(\exists R\in \mathrm{Real}\left(\right),\mathrm{apply}\left(admissible,R\right)\right)\right)\right)\wedge \left(\left(\forall delta\in \mathrm{Real}\left(\right),\left\{\mathrm{applyTwo}\left(shiftedAdmissible,delta,R\right)\mid R\in \mathrm{Real}\left(\right)\right\}=\left\{\mathrm{apply}\left(admissible,R\right)\mid R\in \mathrm{Real}\left(\right)\right\}\right)\wedge \left(\left(\left(\forall R\in \mathrm{Real}\left(\right),\mathrm{apply}\left(admissible,R\right)\Rightarrow \mathrm{apply}\left(completion,R\right)\right)\wedge \left(\forall nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{map}\left((x:\mathrm{Real}\left(\right)\mapsto \mathrm{neg}\left(x\right)),nu\right)=nu\Rightarrow \left(\mathrm{apply}\left(spectralReading,nu\right)=source\Rightarrow \mathrm{apply}\left(admissible,\mathrm{apply}\left(resolventMoment,nu\right)\right)\right)\right)\right)\Rightarrow \left(\forall R\in \mathrm{Real}\left(\right),R\in \mathrm{Icc}\left(\max \left(0,lower\right),upper\right)\iff \mathrm{apply}\left(completion,R\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/ParityWeylInterval.parity_weyl_interval (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof treats zero boundary channels by the two kernel hypotheses. For nonzero channels, conditional-completeness bounds turn affine positivity into the lower and upper Rayleigh endpoint inequalities. Direct ring identities prove invariance under recentering.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/ParityWeylInterval.parity_weyl_interval