Integer Fischer Selector

Abstract

Fischer’s determinant inequality gives a positive logarithmic loss independent of matrix dimension.

All index types are finite. Positive definiteness includes symmetry. For an integer matrix T, let R(T) denote its entrywise inclusion into the real matrices, let card(n) denote the number of indices, and let tr denote the trace. The selected integer k is at least two and the price p lies strictly between log((k+1)/k) and log(k/(k-1)). Write delta(k, p) for the minimum of the two endpoint margins log(k/(k-1))-p and p-log((k+1)/k) together with the two-coordinate loss log(k squared)-log(k squared minus one). Empty products equal one.

Theorem 1.1 (A two-coordinate principal block).

$$\begin{array}{c}\forall n:Type,[Fintype\left(n\right)][DecidableEq\left(n\right)],\\ \forall T:Matrix\left(n,n,\mathbb{R}\right),\\ \forall i\in n,j\in n,\left(PosDef\left(T\right)\wedge i\ne j\right)\Rightarrow det\left(T\right)\le (T\left(i,i\right)\cdot T\left(j,j\right)-T\left(i,j\right)\cdot T\left(j,i\right))\cdot \prod _{l\in n\setminus \{i,j\}}T\left(l,l\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/IntegerFischerSelector.fischer_two_block (✓ std3). ∎

Citation. Roger A. Horn and Charles R. Johnson (2012). Matrix Analysis. DOI: 10.1017/CBO9781139020411.

Commentary.

For distinct indices i and j, retain their two by two principal determinant and multiply by the other diagonal entries. This bounds the full determinant from above. An elementary shear has determinant one and changes only one diagonal entry under congruence. Hadamard’s inequality applied after this shear gives the stated bound.

Theorem 1.2 (A nonzero integer entry forces a loss).

$$\begin{array}{c}\forall n:Type,[Fintype\left(n\right)][DecidableEq\left(n\right)],\\ \forall T:Matrix\left(n,n,\mathbb{Z}\right),\\ \forall i\in n,j\in n,\left(PosDef\left(R\left(T\right)\right)\wedge \left(i\ne j\wedge T\left(i,j\right)\ne 0\right)\right)\Rightarrow det\left(T\right)\cdot (T\left(i,i\right)\cdot T\left(j,j\right))\le (T\left(i,i\right)\cdot T\left(j,j\right)-1)\cdot \prod _{l:n}T\left(l,l\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/IntegerFischerSelector.integer_fischer_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

The square of a nonzero integer is at least one. Symmetry therefore lowers the two-coordinate determinant by at least one relative to its diagonal product. Multiplication by the positive diagonal entries yields the integer form of the bound.

Theorem 1.3 (Only the endpoint margins determine the gap).

$$\forall k\in \mathbb{N},p\in \mathbb{R},\left(2\le k\wedge \left(log\left(\frac{k+1}{k}\right)<p\wedge p<log\left(\frac{k}{k-1}\right)\right)\right)\Rightarrow \delta (k,p)=min\left(log\left(\frac{k}{k-1}\right)-p,p-log\left(\frac{k+1}{k}\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/IntegerFischerSelector.selectorGap_eq_min (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two endpoint margins add to log(k squared) minus log(k squared minus one), since (k-1)(k+1) equals k squared minus one. Both margins are positive on the price interval, so their minimum does not exceed their sum. Thus delta(k, p) equals the minimum of the two endpoint margins.

Theorem 1.4 (A positive margin depending on k and p).

$$\forall k\in \mathbb{N},p\in \mathbb{R},\left(2\le k\wedge \left(log\left(\frac{k+1}{k}\right)<p\wedge p<log\left(\frac{k}{k-1}\right)\right)\right)\Rightarrow 0<min\left(min\left(log\left(\frac{k}{k-1}\right)-p,p-log\left(\frac{k+1}{k}\right)\right),log\left(k^2\right)-log\left(k^2-1\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/IntegerFischerSelector.selectorGap_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each of the three terms is positive on the strict price interval: the first two because the interval endpoints are strict, the third because the logarithm is strictly increasing and k squared exceeds k squared minus one. The margin contains no matrix dimension.

Theorem 1.5 (The scalar matrix is uniformly isolated).

$$\begin{array}{c}\forall n:Type,[Fintype\left(n\right)][DecidableEq\left(n\right)],\\ \forall T:Matrix\left(n,n,\mathbb{Z}\right),\\ \forall k\in \mathbb{N},p\in \mathbb{R},\left(\left(2\le k\wedge \left(log\left(\frac{k+1}{k}\right)<p\wedge p<log\left(\frac{k}{k-1}\right)\right)\right)\wedge PosDef\left(R\left(T\right)\right)\right)\Rightarrow \left(0<\delta (k,p)\wedge \left(log\left(det\left(T\right)\right)-p\cdot tr\left(T\right)\le (card\left(n\right))\cdot (log\left(k\right)-p\cdot k)\wedge \left(T\ne k\cdot I\left(n\right)\Rightarrow log\left(det\left(T\right)\right)-p\cdot tr\left(T\right)\le (card\left(n\right))\cdot (log\left(k\right)-p\cdot k)-\delta (k,p)\right)\right)\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/IntegerFischerSelector.integer_log_unique_maximum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The objective log(det(T))-p tr(T) is bounded above by the number of indices times log(k)-p k. Every matrix distinct from k times the identity loses at least the margin. If a diagonal entry differs from k, sum the scalar selector inequalities and retain that entry’s loss. If every diagonal entry equals k, a nonzero off-diagonal entry gives the two-coordinate loss. Taking logarithms cancels the remaining diagonal product, so this loss is independent of dimension.

Theorem 1.6 (The gap is attained in every nonempty dimension).

$$\forall n:Type,[Fintype\left(n\right)][DecidableEq\left(n\right)][Nonempty\left(n\right)],\forall k\in \mathbb{N},p\in \mathbb{R},\left(2\le k\wedge \left(log\left(\frac{k+1}{k}\right)<p\wedge p<log\left(\frac{k}{k-1}\right)\right)\right)\Rightarrow \left(\exists T\in Matrix\left(n,n,\mathbb{Z}\right),PosDef\left(R\left(T\right)\right)\wedge \left(T\ne k\cdot I\left(n\right)\wedge log\left(k^{card\left(n\right)}\right)-p\cdot (card\left(n\right)\cdot k)-(log\left(det\left(T\right)\right)-p\cdot tr\left(T\right))=\delta (k,p)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/IntegerFischerSelector.selectorGap_sharp (✓ std3). ∎

Source. Repository-derived.

Commentary.

Choose an index and replace its diagonal entry in k times the identity by k-1 or k+1. Both resulting integer matrices are positive definite and distinct from k times the identity. The logarithm of a diagonal determinant is the sum of the logarithms of its entries. All unchanged coordinates cancel from the objective difference, leaving exactly log(k/(k-1))-p or p-log((k+1)/k). Choose the smaller margin; equality with delta(k, p) shows that the uniform gap cannot be increased.

References

• Truth anchor: D5/S3/Arith/GoldenResource/IntegerFischerSelector.fischer_two_block
• Truth anchor: D5/S3/Arith/GoldenResource/IntegerFischerSelector.integer_fischer_gap
• Truth anchor: D5/S3/Arith/GoldenResource/IntegerFischerSelector.integer_log_unique_maximum
• Truth anchor: D5/S3/Arith/GoldenResource/IntegerFischerSelector.selectorGap_eq_min
• Truth anchor: D5/S3/Arith/GoldenResource/IntegerFischerSelector.selectorGap_pos
• Truth anchor: D5/S3/Arith/GoldenResource/IntegerFischerSelector.selectorGap_sharp
• Dependency: D5/S3/Arith/GoldenResource/DiscreteLogSelector
• Dependency: D5/S3/Arith/GoldenResource/IntegerHadamard