Odd-Test Family Budget Upper Bound

Abstract

The admissible finite odd-test family bounds a negative rank-one pencil’s budget by its Rayleigh-infimum endpoint.

Theorem 1.1 (The odd-test family bounds the budget by its infimum endpoint).

$$\begin{array}{c}\forall n:\mathbb{N},\\ B:\mathrm{Matrix}(\mathrm{Fin}(n),\mathrm{Fin}(n),\mathbb{C}),\\ s:\mathrm{Fin}(n)\to \mathbb{C},\\ R0,R:\mathbb{R},\\ ((\exists o:\mathrm{Fin}(n)\to \mathbb{C},⟨s,o⟩\ne 0)\wedge \\ \mathrm{BddBelow}(\left\{\exists o:\mathrm{Fin}(n)\to \mathbb{C},⟨s,o⟩\ne 0\wedge q=\frac{\mathrm{Re}(⟨o,\mathrm{mulVec}(B,o)⟩)}{\mathrm{normSq}(⟨s,o⟩)}\mid q\in \mathbb{R}\right\})\wedge \\ (\forall o:\mathrm{Fin}(n)\to \mathbb{C},⟨s,o⟩\ne 0\Rightarrow 0\le \mathrm{Re}(⟨o,\mathrm{mulVec}(B,o)⟩)-(R-R0)\cdot \mathrm{normSq}(⟨s,o⟩)))\Rightarrow \\ R\le R0+\mathrm{sInf}(\left\{\exists o:\mathrm{Fin}(n)\to \mathbb{C},⟨s,o⟩\ne 0\wedge q=\frac{\mathrm{Re}(⟨o,\mathrm{mulVec}(B,o)⟩)}{\mathrm{normSq}(⟨s,o⟩)}\mid q\in \mathbb{R}\right\}).\end{array}$$

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

Source. Repository-derived.

Commentary.

The public odd-test quotient set contains the Rayleigh quotient of every finite complex test with nonzero boundary pairing. Its upper endpoint is the reference budget plus the real infimum of that entire set.

The family is explicitly nonempty and bounded below. Nonnegativity of the negative rank-one pencil is assumed for every admissible test; each nonzero boundary pairing has positive norm square, so division makes the shifted budget a lower bound of every quotient. The conditional infimum property then gives the endpoint bound.

The repository contains a generic parity endpoint construction, but no finite-matrix theorem exposing this negative rank-one pencil. The proof reuses the pinned norm-square, positive-division, and real infimum lemmas.

References

• Truth anchor: D5/S3/Weil/Budget/OddTestBudgetUpperBound.odd_test_budget_at_most_upper