Minimal Binary Unimodular Expansion

Abstract

Nonnegative integral binary matrices have sharp expansion floors determined by the sign of their unimodular determinant.

Theorem 1.1 (The Fibonacci matrix realizes both sharp determinant-sign bounds).

$$\begin{array}{r}\forall M:\mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{N}),lambda:\mathbb{R},\\ 1<lambda\wedge \mathrm{IsRoot}(\mathrm{charpoly}(\mathrm{cast}(\mathbb{R},M)),lambda)\Rightarrow \\ (\det (\mathrm{cast}(\mathbb{Z},M))=-1\Rightarrow \phi \le lambda)\wedge \\ (\det (\mathrm{cast}(\mathbb{Z},M))=1\Rightarrow {\phi }^2\le lambda)\wedge \\ (letF:=matrix2(1,1,1,0),\det (\mathrm{cast}(\mathbb{Z},F))=-1\wedge \mathrm{cast}(\mathbb{R},F)=fibonacciSubstitution\wedge 1<\phi \wedge \mathrm{IsRoot}(\mathrm{charpoly}(\mathrm{cast}(\mathbb{R},F)),\phi ))\wedge \\ (letF:=matrix2(1,1,1,0),letF2:=F^2,F2=matrix2(2,1,1,1)\wedge \det (\mathrm{cast}(\mathbb{Z},F2))=1\wedge 1<{\phi }^2\wedge \mathrm{IsRoot}(\mathrm{charpoly}(\mathrm{cast}(\mathbb{R},F2)),{\phi }^2)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenCoding/MinimalBinaryUnimodularBreak.minimal_binary_unimodular_break (✓ std3). ∎

Source. Repository-derived.

Commentary.

The matrix M has nonnegative integral entries, and lambda is a real characteristic root above one. In determinant sign minus one, the integral trace is at least one; in determinant sign one, it is at least three. Factoring the corresponding quadratics gives the two displayed lower bounds.

The public equality clauses use the integral Fibonacci matrix itself. Its real cast is the repository’s canonical Fibonacci substitution, while direct finite arithmetic identifies its square and verifies both determinants and characteristic roots.

References

• Truth anchor: D5/S3/Observer/GoldenCoding/MinimalBinaryUnimodularBreak.minimal_binary_unimodular_break
• Dependency: D5/S1/Eigenstructure/FibonacciMatrixDiscriminant