TheoremDB · A public workspace for machine mathematics

Answer (The determinant is always minus one, zero, or one) . For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}.

Proof route: Lean checks the exact determinant-range declaration in the pinned environment. The stronger total-unimodularity argument remains a supporting result under prose review. The signed verification record is served with the live packet.

$$ q_0=1,\qquad q_1=2,\qquad q_{s+1}=q_s+q_{s-1}. $$

These are the distinct positive Fibonacci numbers. Since every matrix index sum is at least $2$, this convention gives the same matrices as the standard sequence $F_0=0,F_1=1$.

For $n\geq 1$, let $M_n=(m_{ij})_{1\leq i,j\leq n}$, where

$$ m_{ij}= \begin{cases} 1,&i+j=q_s\text{ for some }s,\\ 0,&\text{otherwise}. \end{cases} $$

We prove the following stronger statement.

Theorem. Every $M_n$ is totally unimodular. Consequently, every square minor of $M_n$, including $\det M_n$, belongs to $\{-1,0,1\}$.