Forbidden Neighbour Determinant

Abstract

Weighted forbidden-neighbour configurations, their Gram determinant, and quantum readout.

Theorem 1.1 (Admissibility as exclusion).

$$\forall n\in \mathbb{N},\forall b\in \mathrm{Fin}(n)\to \mathrm{Bool},AdmissibleCount.Adm(n,b)\iff \left(\forall i\in \mathrm{Fin}(n),\forall j\in \mathrm{Fin}(n),\mathrm{val}(i)+1=\mathrm{val}(j)\Rightarrow \left(b(i)=\mathrm{false}\vee b(j)=\mathrm{false}\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.adm_iff_no_adjacent_true (✓ std3). ∎

Source. Repository-derived.

Commentary.

AdmissibleCount.Adm owns the configuration predicate, with its existing decAdm instance. Coordinates are zero-based; a true Boolean means occupied. This characterization gives the adjacency reading used by reversal and quantum normalization.

Definition 1.2 (Occupation number).

$$\forall n\in \mathbb{N},\forall b\in \mathrm{Fin}(n)\to \mathrm{Bool},\mathrm{occupationCount}(b)=\sum _{i:\mathrm{Fin}(n)}(Bool.toNat(b(i)))$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.occupationCount (✓ std3).

Source. Repository-derived.

Commentary.

Bool.toNat maps false to zero and true to one.

Definition 1.3 (The configuration polynomial).

$$\forall n\in \mathbb{N},\forall w\in \mathrm{Fin}(n)\to \mathbb{R},\mathrm{forbiddenPartition}(w)=\sum _{b:\{b:\mathrm{Fin}(n)\to \mathrm{Bool}\mid AdmissibleCount.Adm(n,b)\}}((Polynomial.X{)}^{\mathrm{occupationCount}(\mathrm{val}(b))}\cdot Polynomial.C(\prod _{i:\mathrm{Fin}(n)}((w(i){)}^{Bool.toNat(\mathrm{val}(b)(i))})))$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.forbiddenPartition (✓ std3).

Source. Repository-derived.

Commentary.

The sum is over the legal subtype. Polynomial.X and Polynomial.C are the indeterminate and constant embedding. Coefficients use only powers and products of weights.

Definition 1.4 (The explicit bidiagonal matrix).

$$\forall d\in \mathbb{N},\forall w\in \mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathbb{R},\forall i\in \mathrm{Fin}(d),\forall j\in \mathrm{Fin}(d),\mathrm{lowerBidiagonal}(w)(i,j)=\mathrm{ite}(i=j,Real.sqrt(w(Fin.mk(2\cdot \mathrm{val}(i)))),\mathrm{ite}(\mathrm{val}(j)+1=\mathrm{val}(i),Real.sqrt(w(Fin.mk(2\cdot \mathrm{val}(j)+1))),0))$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.lowerBidiagonal (✓ std3).

Source. Repository-derived.

Commentary.

Fin.mk carries the displayed index with its bound proof. Odd one-based weights form the diagonal; even one-based weights form the subdiagonal. The remaining entries are zero.

Theorem 1.5 (Gram positivity).

$$\forall d\in \mathbb{N},\forall w\in \mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathbb{R},Matrix.PosSemidef(Matrix.transpose(\mathrm{lowerBidiagonal}(w))\cdot \mathrm{lowerBidiagonal}(w))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.gramPosSemidef (✓ std3). ∎

Source. Repository-derived.

Commentary.

This companion binds Mathlib Gram positivity for the explicit matrix. It includes singular matrices and does not need strictly positive weights.

Definition 1.6 (The Gram eigenvalues).

$$\forall d\in \mathbb{N},\forall w\in \mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathbb{R},\mathrm{gramEigenvalue}(w)=Matrix.IsHermitian.eigenvalues(Matrix.PosSemidef.isHermitian(\mathrm{gramPosSemidef}(w)))$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.gramEigenvalue (✓ std3).

Source. Repository-derived.

Commentary.

The eigenvalues are Mathlib’s real Hermitian eigenvalue list, including any zero eigenvalues.

Definition 1.7 (Normalized configuration amplitudes).

$$\forall n\in \mathbb{N},\forall w\in \mathrm{Fin}(n)\to \mathbb{R},\forall r\in \mathbb{R},\forall b\in \{b:\mathrm{Fin}(n)\to \mathrm{Bool}\mid AdmissibleCount.Adm(n,b)\},\mathrm{quantumState}(w,r)(b)=Complex.ofReal(\frac{1}{Real.sqrt(Polynomial.eval(r,\mathrm{forbiddenPartition}(w)))}\cdot (r{)}^{\frac{Nat.cast(\mathbb{R},\mathrm{occupationCount}(\mathrm{val}(b)))}{2}}\cdot \prod _{i:\mathrm{Fin}(n)}((w(i){)}^{\frac{Nat.cast(\mathbb{R},Bool.toNat(\mathrm{val}(b)(i)))}{2}}))$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.quantumState (✓ std3).

Source. Repository-derived.

Commentary.

Both half exponents are real exponents. Nat.cast here denotes the real coercion. The complex vector uses the legal configurations as its coordinates.

Definition 1.8 (The occupation observable).

$$\forall n\in \mathbb{N},\mathrm{numberOperator}(n)=Matrix.diagonal((b:\{b:\mathrm{Fin}(n)\to \mathrm{Bool}\mid AdmissibleCount.Adm(n,b)\}\mapsto Nat.cast(\mathbb{C},\mathrm{occupationCount}(\mathrm{val}(b)))))$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.numberOperator (✓ std3).

Source. Repository-derived.

Commentary.

Nat.cast here is the complex coercion. This diagonal matrix acts on the configuration space.

Definition 1.9 (Single-particle tunnelling).

$$\forall d\in \mathbb{N},\forall w\in \mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathbb{R},\mathrm{tunnellingMatrix}(w)=Matrix.fromBlocks(0,\mathrm{lowerBidiagonal}(w),Matrix.transpose(\mathrm{lowerBidiagonal}(w)),0)$$

Formalization. D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.tunnellingMatrix (✓ std3).

Source. Repository-derived.

Commentary.

The two blocks are indexed by Fin d. This single-particle space is distinct from the configuration space.

Theorem 1.10 (Determinant realization and quantum readout).

$$\begin{array}{r}\forall d:\mathbb{N},w:\mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathbb{R},\\ (1\le d\wedge \left(\forall i\in \mathrm{Fin}(Nat.sub(2\cdot d,1)),0\le w(i)\right))⟹\\ (\mathrm{forbiddenPartition}(w)=Matrix.det(1+Polynomial.X\cdot Matrix.map(Matrix.transpose(\mathrm{lowerBidiagonal}(w))\cdot \mathrm{lowerBidiagonal}(w),Polynomial.C)))\\ \wedge (Matrix.PosSemidef(Matrix.transpose(\mathrm{lowerBidiagonal}(w))\cdot \mathrm{lowerBidiagonal}(w)))\\ \wedge (\forall i\in \mathrm{Fin}(d),0\le \mathrm{gramEigenvalue}(w,i))\\ \wedge (\mathrm{forbiddenPartition}(w)=\prod _{i:\mathrm{Fin}(d),\mathrm{gramEigenvalue}(w,i)\ne 0}(1+Polynomial.C(\mathrm{gramEigenvalue}(w,i))\cdot Polynomial.X))\\ \wedge (\forall z\in \mathbb{C},Polynomial.eval(z,Polynomial.map(Complex.ofRealHom,\mathrm{forbiddenPartition}(w)))=0\Rightarrow \left(\exists t\in \mathbb{R},t<0\wedge \left(z=Complex.ofReal(t)\wedge \left(\exists i\in \mathrm{Fin}(d),0<\mathrm{gramEigenvalue}(w,i)\wedge t=-(\frac{1}{\mathrm{gramEigenvalue}(w,i)})\right)\right)\right))\\ \wedge (Matrix.charpoly(\mathrm{tunnellingMatrix}(w))=Matrix.det((Polynomial.X{)}^2\cdot 1-Matrix.map(Matrix.transpose(\mathrm{lowerBidiagonal}(w))\cdot \mathrm{lowerBidiagonal}(w),Polynomial.C)))\\ \wedge (\forall v\in \mathbb{R},v\ne 0\Rightarrow Polynomial.eval(v,Matrix.charpoly(\mathrm{tunnellingMatrix}(w)))=(v{)}^{2\cdot d}\cdot Polynomial.eval(-(\frac{1}{(v{)}^2}),\mathrm{forbiddenPartition}(w)))\\ \wedge (\forall n\in \mathbb{N},\forall u\in \mathrm{Fin}(n+2)\to \mathbb{R},\mathrm{forbiddenPartition}(u)=\mathrm{forbiddenPartition}((i:\mathrm{Fin}(n+1)\mapsto u(Fin.castSucc(i))))+Polynomial.X\cdot Polynomial.C(u(Fin.last(n+1)))\cdot \mathrm{forbiddenPartition}((i:\mathrm{Fin}(n)\mapsto u(Fin.castSucc(Fin.castSucc(i))))))\\ \wedge (\forall r\in \mathbb{R},\mathrm{quantumState}(w,r)=\frac{1}{Complex.ofReal(Real.sqrt(Polynomial.eval(r,\mathrm{forbiddenPartition}(w))))}\cdot \sum _{b:\{b:\mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathrm{Bool}\mid AdmissibleCount.Adm(Nat.sub(2\cdot d,1),b)\}}(Complex.ofReal((r{)}^{\frac{Nat.cast(\mathbb{R},\mathrm{occupationCount}(\mathrm{val}(b)))}{2}}\cdot \prod _{i:\mathrm{Fin}(Nat.sub(2\cdot d,1))}((w(i){)}^{\frac{Nat.cast(\mathbb{R},Bool.toNat(\mathrm{val}(b)(i)))}{2}}))\cdot Pi.single(b,1)))\\ \wedge (\forall r\in \mathbb{R},0<r\Rightarrow \mathrm{dotProduct}(\mathrm{star}(\mathrm{quantumState}(w,r)),\mathrm{quantumState}(w,r))=1)\\ \wedge (\forall b\in \{b:\mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathrm{Bool}\mid AdmissibleCount.Adm(Nat.sub(2\cdot d,1),b)\},Matrix.mulVec(\mathrm{numberOperator}(Nat.sub(2\cdot d,1)),Pi.single(b,1))=Nat.cast(\mathbb{C},\mathrm{occupationCount}(\mathrm{val}(b)))\cdot Pi.single(b,1))\\ \wedge (\forall r\in \mathbb{R},\forall theta\in \mathbb{R},0<r\Rightarrow \mathrm{dotProduct}(\mathrm{star}(\mathrm{quantumState}(w,r)),Matrix.mulVec(NormedSpace.exp(Complex.ofReal(theta)\cdot Complex.I\cdot \mathrm{numberOperator}(Nat.sub(2\cdot d,1))),\mathrm{quantumState}(w,r)))=\frac{Polynomial.eval(Complex.ofReal(r)\cdot Complex.exp(Complex.ofReal(theta)\cdot Complex.I),Polynomial.map(Complex.ofRealHom,\mathrm{forbiddenPartition}(w)))}{Complex.ofReal(Polynomial.eval(r,\mathrm{forbiddenPartition}(w)))})\\ \wedge (\forall P\in \mathrm{Polynomial}(\mathbb{R}),\forall r\in \mathbb{R},\forall theta\in \mathbb{R},\left(\mathrm{forbiddenPartition}(w)=P\wedge 0<r\right)\Rightarrow \mathrm{dotProduct}(\mathrm{star}(\mathrm{quantumState}(w,r)),Matrix.mulVec(NormedSpace.exp(Complex.ofReal(theta)\cdot Complex.I\cdot \mathrm{numberOperator}(Nat.sub(2\cdot d,1))),\mathrm{quantumState}(w,r)))=\frac{Polynomial.eval(Complex.ofReal(r)\cdot Complex.exp(Complex.ofReal(theta)\cdot Complex.I),Polynomial.map(Complex.ofRealHom,P))}{Complex.ofReal(Polynomial.eval(r,P))})\\ \wedge (Fintype.card(\{b:\mathrm{Fin}(Nat.sub(2\cdot d,1))\to \mathrm{Bool}\mid AdmissibleCount.Adm(Nat.sub(2\cdot d,1),b)\})=Nat.fib(2\cdot d+1)\wedge Fintype.card(\mathrm{Sum}(\mathrm{Fin}(d),\mathrm{Fin}(d)))=2\cdot d)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.forbidden_neighbour_determinant (✓ std3). ∎

Citation. Ole J. Heilmann and Elliott H. Lieb (1972). Theory of monomer-dimer systems. DOI: 10.1007/BF01877590.

Commentary.

The parenthesized rows hold simultaneously. The weights are nonnegative, including zero; d is at least one. Matrix multiplication, scalar multiplication and polynomial evaluation have their displayed Mathlib meanings.

The configuration recurrence is derived by splitting endpoint occupancy. A second endpoint expansion gives the path determinant recurrence, and interleaving the two parts of the explicit bidiagonal block matrix identifies the Gram determinant. Square roots cancel before the final polynomial coefficients.

The negative-root clause is the weighted-path specialization of the Heilmann-Lieb zero principle (1972). The exact bidiagonal realization and normalized readout are the repository’s explicit construction; the literature note attributes only the zero principle.

The charpoly identity is an identity of real polynomials and applies at zero. The reciprocal evaluation formula is written for nonzero v; its polynomial continuation is the preceding identity, so totalized division at zero is never used to claim that formula.

The symbol P in the conditional row is an arbitrary real polynomial. Substituting the actual Jensen polynomial requires the independent equality forbiddenPartition(w)=P. No RH assumption or such Jensen equality is asserted.

The final row gives the two basis counts. Equality of partition polynomials does not assert a unitary equivalence of the complete physical systems. Nat.sub is natural truncated subtraction; every other division displayed below is in the real or complex field.

References

• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.adm_iff_no_adjacent_true
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.forbiddenPartition
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.forbidden_neighbour_determinant
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.gramEigenvalue
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.gramPosSemidef
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.lowerBidiagonal
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.numberOperator
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.occupationCount
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.quantumState
• Truth anchor: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant.tunnellingMatrix
• Dependency: D5/S1/Words/AdmissibleWords/AdmissibleCount