Quantitative edges of a positive and negative block spike

Abstract

A rank-one diagonal spike in a Hermitian block matrix admits two-sided spectral-edge estimates. For a unit v, Hermitian S with Sv = 0, L >= 1 and L >= ‖K X S‖, every t >= 96L has an error at most 891L^4/t^3 at each edge, and 1782L^4/t^3 in their sum.

Definition 1.1 (Top spectral edge).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (M:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\mathrm{edgeMax}\left(M\right)=\mathrm{sSup}\left(\mathrm{spectrum}\left(\mathbb{R},M\right)\right)$$

Formalization. D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.edgeMax (✓ std3).

Source. Repository-derived.

Commentary.

The real supremum of the real spectrum. Hermitian matrices on nonempty finite types have a nonempty compact real spectrum.

Definition 1.2 (Bottom spectral edge).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (M:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\mathrm{edgeMin}\left(M\right)=\mathrm{sInf}\left(\mathrm{spectrum}\left(\mathbb{R},M\right)\right)$$

Formalization. D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.edgeMin (✓ std3).

Source. Repository-derived.

Commentary.

The real infimum of the real spectrum, using the same real-spectrum convention as the top edge.

Definition 1.3 (Hermitian block pencil).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (X:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (D:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),K\left(X,D\right)=\mathrm{Matrix}.\mathrm{fromBlocks}\left(D,X,\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right),-D\right)$$

Formalization. D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.K (✓ std3).

Source. Repository-derived.

Commentary.

K X D is Matrix.fromBlocks D X (Matrix.conjTranspose X) (-D); it is Hermitian when D is Hermitian.

Lemma 1.4 (Upper spectral shift).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (M:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{IsHermitian}\left(M\right))\Rightarrow (\forall (c:\mathbb{R}),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(c\cdot 1-M\right))\iff (\forall (x:\mathbb{R}),(x\in \mathrm{spectrum}\left(\mathbb{R},M\right))\Rightarrow (x\le c)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.upper_shift_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

A scalar upper spectral bound is exactly positivity of the scalar shift minus the Hermitian matrix.

Lemma 1.5 (Action of a rank-one matrix).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (v:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),\forall (z:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right),\mathrm{star}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right)\right)\right)\right)\left(z\right)=⟨v,z{⟩}_{\mathbb{C}}\cdot v$$

Proof. Machine-checked in Lean as D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.outer_action (✓ std3). ∎

Source. Repository-derived.

Commentary.

Matrix.vecMulVec and WithLp.ofLp are the actual matrix and vector carriers. The scalar is the complex inner product.

Lemma 1.6 (Hermitian rank-one matrix).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (v:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right),\mathrm{star}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.outer_hermitian (✓ std3). ∎

Source. Repository-derived.

Commentary.

The conjugate transpose of the rank-one matrix equals the matrix itself.

Definition 1.7 (First edge-sum coefficient).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (X:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (v:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),defect1\left(X,v\right)={\Vert \mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)\right)\left(v\right)\Vert }^2-{\Vert \mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(X\right)\left(v\right)\Vert }^2$$

Formalization. D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.defect1 (✓ std3).

Source. Repository-derived.

Commentary.

The first coefficient measures the squared norm difference between the adjoint action and the original action.

Definition 1.8 (Second edge-sum coefficient).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],\forall (X:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (S:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (v:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),defect2\left(X,S,v\right)=\mathrm{Complex}.\mathrm{re}\left(⟨\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(X\right)\left(v\right),\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(S\right)\left(\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(X\right)\left(v\right)\right){⟩}_{\mathbb{C}}\right)-\mathrm{Complex}.\mathrm{re}\left(⟨\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)\right)\left(v\right),\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(S\right)\left(\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)\right)\left(v\right)\right){⟩}_{\mathbb{C}}\right)$$

Formalization. D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.defect2 (✓ std3).

Source. Repository-derived.

Commentary.

The second coefficient is the difference of the real S-pairings, with the original action first and the adjoint action second.

Theorem 1.9 (Two-sided positive-edge enclosure).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],[\mathrm{Nonempty}\left(\iota \right)],\forall (X:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (S:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (v:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),\forall (t:\mathbb{R}),\forall (L:\mathbb{R}),(\Vert v\Vert =1)\Rightarrow ((\mathrm{Matrix}.\mathrm{IsHermitian}\left(S\right))\Rightarrow ((\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(S\right)\left(v\right)=0)\Rightarrow ((1\le L)\Rightarrow ((\Vert K\left(X,S\right)\Vert \le L)\Rightarrow ((96\cdot L\le t)\Rightarrow (\left|\mathrm{edgeMax}\left(K\left(X,t\cdot \mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right),\mathrm{star}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right)\right)\right)+S\right)\right)-(t+\frac{{\Vert \mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)\right)\left(v\right)\Vert }^2-\frac{{\Vert ⟨v,\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(X\right)\left(v\right){⟩}_{\mathbb{C}}\Vert }^2}{2}}{t}-\frac{\mathrm{Complex}.\mathrm{re}\left(⟨\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)\right)\left(v\right),\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(S\right)\left(\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)\right)\left(v\right)\right){⟩}_{\mathbb{C}}\right)}{t^2})\right|\le \frac{891\cdot L^4}{t^3}))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.positive_spike_enclosure (✓ std3). ∎

Source. Repository-derived.

Commentary.

The normalized test vector is formed from e + εr₁ + ε²r₂ at ε = 1/t. Its Rayleigh quotient supplies the lower edge bound; the complement gap and residual-energy estimate supply the upper bound. Both estimates hold at every finite t >= 96L.

Theorem 1.10 (Two-sided edge-sum enclosure).

$$\forall (\iota :Type),[\mathrm{Fintype}\left(\iota \right)],[\mathrm{DecidableEq}\left(\iota \right)],[\mathrm{Nonempty}\left(\iota \right)],\forall (X:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (S:\mathrm{Matrix}\left(\iota ,\iota ,\mathbb{C}\right)),\forall (v:\mathrm{EuclideanSpace}\left(\mathbb{C},\iota \right)),\forall (t:\mathbb{R}),\forall (L:\mathbb{R}),(\Vert v\Vert =1)\Rightarrow ((\mathrm{Matrix}.\mathrm{IsHermitian}\left(S\right))\Rightarrow ((\mathrm{Matrix}.\mathrm{toEuclideanCLM}\left(S\right)\left(v\right)=0)\Rightarrow ((1\le L)\Rightarrow ((\Vert K\left(X,S\right)\Vert \le L)\Rightarrow ((96\cdot L\le t)\Rightarrow (\left|\mathrm{edgeMax}\left(K\left(X,t\cdot \mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right),\mathrm{star}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right)\right)\right)+S\right)\right)+\mathrm{edgeMin}\left(K\left(X,t\cdot \mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right),\mathrm{star}\left(\mathrm{WithLp}.\mathrm{ofLp}\left(v\right)\right)\right)+S\right)\right)-(\frac{defect1\left(X,v\right)}{t}+\frac{defect2\left(X,S,v\right)}{t^2})\right|\le \frac{1782\cdot L^4}{t^3}))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.edge_sum_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Unitary block reflection transfers the positive-edge estimate to the negative edge. Their leading ±t terms cancel. The sum has the corrected coefficient ‖X* v‖² - ‖X v‖² at order 1/t and the difference of the S-pairings at order 1/t².

References

• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.K
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.defect1
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.defect2
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.edgeMax
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.edgeMin
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.edge_sum_bound
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.outer_action
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.outer_hermitian
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.positive_spike_enclosure
• Truth anchor: D5/S3/Quantum/BlockNorm/SpikeEdgeEstimate.upper_shift_iff
• Dependency: D5/S3/Weil/GroundMode/ResidualDrivenProjectiveEnergy