The sharp product and its two positive spectral rays

Abstract

Sharp product equality on labelled K2m determines the entire native spectrum.

Every natural m at least three is allowed. The vertices are Fin (2+m), with two labelled hubs and m labelled leaves. Every one of the 2m hub-to-leaf conductances varies independently over strictly positive reals. The matrix is the original ordinary unnormalized wLap, lambda2 is the original mean-zero Rayleigh infimum, and totalRes is the original harmonic-current resistance summed over every unordered distinct vertex pair, including nonadjacent pairs. No total-conductance or symmetry assumption is imposed on competitors. Nonedge values are arbitrary.

Definition 1.1 (The complete native eigenvalue multiplicities).

$$\forall m\in \mathrm{Nat},\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},\forall t\in \mathrm{Real},(\mathrm{FullSpectrum}\left(m,w,t\right))\iff (lete:=\mathrm{eigenvalues}\left(\mathrm{wLap}\left(K2m\left(m\right),w\right)\right)in(\mathrm{card}\left(\mathrm{filter}\left((\lambda i\mapsto e\left(i\right)=0),\mathrm{univ}\left(\mathrm{Fin}\left(2+m\right)\right)\right)\right)=1)\wedge ((\mathrm{card}\left(\mathrm{filter}\left((\lambda i\mapsto e\left(i\right)=t),\mathrm{univ}\left(\mathrm{Fin}\left(2+m\right)\right)\right)\right)=m)\wedge ((\mathrm{card}\left(\mathrm{filter}\left((\lambda i\mapsto e\left(i\right)=(m)\cdot (t)),\mathrm{univ}\left(\mathrm{Fin}\left(2+m\right)\right)\right)\right)=1)\wedge (\forall i\in \mathrm{Fin}\left(2+m\right),(e\left(i\right)=0)\vee ((e\left(i\right)=t)\vee (e\left(i\right)=(m)\cdot (t)))))))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.FullSpectrum (✓ std3).

Source. Repository-derived.

Commentary.

The eigenvalues are those returned by Matrix.IsHermitian.eigenvalues for the actual matrix wLap (K2m m) w. FullSpectrum requires exactly one zero eigenvalue, exactly m entries equal to t, exactly one entry equal to m*t, and every entry equal to one of those three values. It imposes no ascending-index convention and introduces no surrogate matrix or assumed spectral list. When m is at least three and t is positive, the three values are distinct. The generic Hermitian spectral theorem makes this indexed enumeration the full spectrum with multiplicity.

Definition 1.2 (One common sign across every leaf).

$$\forall m\in \mathrm{Nat},\forall t\in \mathrm{Real},\forall epsilon\in \mathrm{Real},\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\mathrm{Ray}\left(m,t,epsilon,w\right))\iff (\mathrm{EdgeRestriction}\left(m,(\frac{t}{2})\cdot (1+(epsilon)\cdot (\mathrm{splitRatio}\left(m\right))),(\frac{t}{2})\cdot (1-(epsilon)\cdot (\mathrm{splitRatio}\left(m\right))),w\right))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.Ray (✓ std3).

Source. Repository-derived.

Commentary.

For a real scale t and sign epsilon, Ray fixes each first-hub conductance to t/2*(1+epsilonsqrt((m-2)/(m+2))) and each second-hub conductance to t/2(1-epsilon*sqrt((m-2)/(m+2))). The same epsilon is used for all leaves. The theorem restricts t to positive values and epsilon to +1 or -1. The definition compares only labelled edges.

Definition 1.3 (The whole sharp-product endpoint).

$$\forall m\in \mathrm{Nat},(\mathrm{SharpProductClaim}\left(m\right))\iff ((\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (0<w\left(e\right)))\Rightarrow ((lambda2\left(K2m\left(m\right),w\right))\cdot (\mathrm{totalRes}\left(K2m\left(m\right),w\right))\le \mathrm{sharpConstant}\left(m\right)))\wedge ((\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (0<w\left(e\right)))\Rightarrow (((lambda2\left(K2m\left(m\right),w\right))\cdot (\mathrm{totalRes}\left(K2m\left(m\right),w\right))=\mathrm{sharpConstant}\left(m\right))\iff (\exists t\in \mathrm{Real},\exists epsilon\in \mathrm{Real},(0<t)\wedge (((epsilon=1)\vee (epsilon=-(1)))\wedge (\mathrm{Ray}\left(m,t,epsilon,w\right))))))\wedge ((\forall t\in \mathrm{Real},\forall epsilon\in \mathrm{Real},(0<t)\Rightarrow (((epsilon=1)\vee (epsilon=-(1)))\Rightarrow ((\exists w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},\mathrm{Ray}\left(m,t,epsilon,w\right))\wedge (\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\mathrm{Ray}\left(m,t,epsilon,w\right))\Rightarrow ((\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (0<w\left(e\right)))\wedge ((lambda2\left(K2m\left(m\right),w\right)=t)\wedge ((\mathrm{totalRes}\left(K2m\left(m\right),w\right)=\frac{\mathrm{sharpConstant}\left(m\right)}{t})\wedge (\mathrm{FullSpectrum}\left(m,w,t\right)))))))))\wedge ((\neg (\exists t\in \mathrm{Real},\exists s\in \mathrm{Real},\exists w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(0<t)\wedge ((0<s)\wedge ((\mathrm{Ray}\left(m,t,1,w\right))\wedge (\mathrm{Ray}\left(m,s,-(1),w\right))))))\wedge ((\forall t\in \mathrm{Real},\forall epsilon\in \mathrm{Real},\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\mathrm{Ray}\left(m,t,epsilon,w\right))\Rightarrow (\mathrm{Ray}\left(m,t,-(epsilon),\mathrm{exchangeWeights}\left(m,w\right)\right)))\wedge (\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},\forall wprime\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (w\left(e\right)=wprime\left(e\right)))\Rightarrow ((lambda2\left(K2m\left(m\right),w\right)=lambda2\left(K2m\left(m\right),wprime\right))\wedge (\mathrm{totalRes}\left(K2m\left(m\right),w\right)=\mathrm{totalRes}\left(K2m\left(m\right),wprime\right)))))))))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.SharpProductClaim (✓ std3).

Source. Repository-derived.

Commentary.

The conjunction contains the universal product bound C_m=(m+2)(m+1/m); equality if and only if a positive scale and one common sign give the edge restriction; existence and positivity of both rays at every positive scale; lambda2=t, totalRes=C_m/t and the full native spectrum on every such restriction; disjointness of the two labelled rays even when their positive scales differ; interchange of the rays under hub exchange; and invariance of lambda2 and totalRes under arbitrary changes on nonedges. Applying the equality characterization and the universal ray conclusion gives the complete spectrum at every equality case.

Theorem 1.4 (The sharp bound, all equality restrictions and their full spectra).

$$\forall m\in \mathrm{Nat},(3\le m)\Rightarrow ((\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (0<w\left(e\right)))\Rightarrow ((lambda2\left(K2m\left(m\right),w\right))\cdot (\mathrm{totalRes}\left(K2m\left(m\right),w\right))\le \mathrm{sharpConstant}\left(m\right)))\wedge ((\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (0<w\left(e\right)))\Rightarrow (((lambda2\left(K2m\left(m\right),w\right))\cdot (\mathrm{totalRes}\left(K2m\left(m\right),w\right))=\mathrm{sharpConstant}\left(m\right))\iff (\exists t\in \mathrm{Real},\exists epsilon\in \mathrm{Real},(0<t)\wedge (((epsilon=1)\vee (epsilon=-(1)))\wedge (\mathrm{Ray}\left(m,t,epsilon,w\right))))))\wedge ((\forall t\in \mathrm{Real},\forall epsilon\in \mathrm{Real},(0<t)\Rightarrow (((epsilon=1)\vee (epsilon=-(1)))\Rightarrow ((\exists w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},\mathrm{Ray}\left(m,t,epsilon,w\right))\wedge (\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\mathrm{Ray}\left(m,t,epsilon,w\right))\Rightarrow ((\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (0<w\left(e\right)))\wedge ((lambda2\left(K2m\left(m\right),w\right)=t)\wedge ((\mathrm{totalRes}\left(K2m\left(m\right),w\right)=\frac{\mathrm{sharpConstant}\left(m\right)}{t})\wedge (\mathrm{FullSpectrum}\left(m,w,t\right)))))))))\wedge ((\neg (\exists t\in \mathrm{Real},\exists s\in \mathrm{Real},\exists w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(0<t)\wedge ((0<s)\wedge ((\mathrm{Ray}\left(m,t,1,w\right))\wedge (\mathrm{Ray}\left(m,s,-(1),w\right))))))\wedge ((\forall t\in \mathrm{Real},\forall epsilon\in \mathrm{Real},\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\mathrm{Ray}\left(m,t,epsilon,w\right))\Rightarrow (\mathrm{Ray}\left(m,t,-(epsilon),\mathrm{exchangeWeights}\left(m,w\right)\right)))\wedge (\forall w\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},\forall wprime\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right)\to \mathrm{Real},(\forall e\in Sym2\left(\mathrm{Fin}\left(2+m\right)\right),(e\in \mathrm{edgeSet}\left(K2m\left(m\right)\right))\Rightarrow (w\left(e\right)=wprime\left(e\right)))\Rightarrow ((lambda2\left(K2m\left(m\right),w\right)=lambda2\left(K2m\left(m\right),wprime\right))\wedge (\mathrm{totalRes}\left(K2m\left(m\right),w\right)=\mathrm{totalRes}\left(K2m\left(m\right),wprime\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product bound, trace equality, positive spectral lower bound, harmonic reciprocal-eigenvalue formula, zero multiplicity, equality parameters, quadratic parameter roots and extremal lambda2/resistance values are direct applications of the original frozen optimizer suppliers. The additional argument proves reciprocal equality rigidity: for the m+1 positive native eigenvalues r_i, put q_i=r_i/t-1. Trace equality gives sum q_i=m-1. Each difference q_i/(1+q_i)-q_i/m is nonnegative, and product equality makes their sum zero. Hence each q_i is either zero or m-1; a positive total forces exactly one nonzero term. Consequently exactly one native eigenvalue is m*t and exactly m are t. This relation is used for every positive point on either equality ray. The construction remains on the original native matrix and harmonic resistance carriers throughout. These are repository-derived consequences of the selected K2m theory; no literature novelty or external open-problem resolution is asserted.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.FullSpectrum
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.Ray
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.SharpProductClaim
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mSharpSpectrum.result
• Dependency: D5/S3/Combinatorics/SpectralGraph/FiedlerResistanceK2mOptimizer