Tech-update

1. The Core Result: Formally Proved

The primary conjecture—that for every integer $n \ge 1$, the determinant of the Fibonacci-sum indicator matrix $M_n$ belongs to $\{-1, 0, 1\}$—has been formally proved and verified in Lean.

The Logic of the Proof: The proof does not rely on a simple induction on $n$, but rather establishes a much stronger structural property: Total Unimodularity.

1. Graph Structure: The bipartite support graph $Q_n$ (where edges exist if $i+j$ is Fibonacci) is shown to be outerplanar and chordal bipartite.
2. Divisibility via Square Covers: Using the properties of this graph, it was proved that any square submatrix with even row and column sums must have an entry sum divisible by 4 (derived from a "square-toggle" induction and odd square covers).
3. Camion's Criterion: The proof applies Camion's Theorem, which states that a $0, \pm 1$ matrix is totally unimodular if and only if every square submatrix with even row/column sums has an entry sum divisible by 4.
4. Conclusion: Since $M_n$ is totally unimodular, every one of its square minors (including the determinant of the full matrix) must be in $\{-1, 0, 1\}$.

2. Computational Evidence

The formal proof is supported by extensive numerical verification:

• Range Verification: Exact integer computation (using fraction-free Bareiss elimination) confirmed that $\det(M_n) \in \{-1, 0, 1\}$ for all $1 \le n \le 120$.
• Nonzero Indices: The specific values of $n$ within the first 120 where the determinant is non-vanishing were explicitly identified (e.g., $n = 1, 2, 3, 5, 9, 14, 15, \dots$).
• Cancellation: At $n=33$, it was observed that there are 10,800 allowed permutations, perfectly split between even and odd parity (5,400 each), resulting in a determinant of 0 despite the high number of perfect matchings.

3. Open Problems and Research Boundaries

While the range of the determinant is settled, the support (the set of $n$ where $\det(M_n) \neq 0$) remains an active area of research.

• The Nonzero Index Characterization: There is currently no necessary-and-sufficient condition to predict exactly which $n$ produce a non-vanishing determinant.
• Gap Conjectures: Observations through $n=1219$ suggest that indices where $\det(M_n) \neq 0$ cluster around Fibonacci numbers, following three distinct "gap families" (primary, secondary, and tertiary). These are currently conjectures based on Zeckendorf representations.
• Generalization to Other Sequences: It was found that simply having a Fibonacci-like growth rate is insufficient to guarantee this determinant property. A counterexample sequence with Fibonacci growth was found to produce $\det(M_5) = 2$.

Summary Table