# P1: Nonzero determinants of the Fibonacci-sum matrix

- ID: `P1`
- Reference: `fib-problem-nonzero-support`
- Page: https://theoremdb.org/statements/P1
- Record maturity: Reviewed problem with recorded work

## Problem

For each integer \(n\ge 1\), define the integer matrix \(M_n=(m_{ij})_{1\le i,j\le n}\) by \[ m_{ij}=\begin{cases} 1, & i+j \text{ is a Fibonacci number}, \\ 0, & \text{otherwise}. \end{cases} \] Determine the set \(\{n\

## Status

Unresolved in this packet after the dated source check. Strongest checked result: The Bareiss replay exactly determines the nonzero indices for 1 <= n <= 120. The MathOverflow answer separately supplies a source-reported support and Zeckendorf table through n=1219 and conjectures primary, secondary, and tertiary gap families; those families are observations rather than proved classifications. Exact unresolved remainder: Give a necessary-and-sufficient condition for every n >= 1 with det M_n != 0 and prove that it covers the replicated blocks, mirror rules, and boundary exceptions, or give an exact counterexample to a proposed classification. [1](#reference-1) [2](#reference-2) [3](#reference-3)

## Work

### Evidence for the current status

**Claim 1 (Dated status and exact unresolved remainder).** Unresolved in this packet after the dated source check. Strongest checked result: The Bareiss replay exactly determines the nonzero indices for 1 <= n <= 120. The MathOverflow answer separately supplies a source-reported support and Zeckendorf table through n=1219 and conjectures primary, secondary, and tertiary gap families; those families are observations rather than proved classifications. Exact unresolved remainder: Give a necessary-and-sufficient condition for every n >= 1 with det M_n != 0 and prove that it covers the replicated blocks, mirror rules, and boundary exceptions, or give an exact counterexample to a proposed classification.

The packet's cited sources and equivalent formulations were checked in the dated review recorded below.

Strongest checked result: The Bareiss replay exactly determines the nonzero indices for 1 <= n <= 120. The MathOverflow answer separately supplies a source-reported support and Zeckendorf table through n=1219 and conjectures primary, secondary, and tertiary gap families; those families are observations rather than proved classifications.

Exact unresolved remainder: Give a necessary-and-sufficient condition for every n >= 1 with det M_n != 0 and prove that it covers the replicated blocks, mirror rules, and boundary exceptions, or give an exact counterexample to a proposed classification.

### Other known results

- **Proposition 1** (supported): The determinant conjecture is equivalent to saying that allowed even and odd permutations differ in count by at most one. [3](#reference-3)
- **Theorem 1** (established): For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}.
- **Proposition 2** (review pending): Every square minor of every M_n has determinant in {-1,0,1}. [1](#reference-1) [2](#reference-2)
- **Proposition 3** (supported): For each forced singleton match, cofactor expansion removes one row and column, leaving det M_n equal up to sign to the residual core determinant.
- **Computation 1** (reproduced): Exact integer computation finds det M_n in {-1,0,1} for every 1 <= n <= 120.
- **Computation 2** (reproduced): The nonzero indices through 120 are 1,2,3,5,9,14,15,23,24,25,37,39,41,60,64,66,67,97,98,103,104,107,108,109.
- **Computation 3** (reproduced): The recurrence sequence 2,6,8,14,22,36,58 has Fibonacci growth and gives determinant 2 at n=5.
- **Computation 4** (reproduced): Repeated forced row or column matching leaves a nonempty core for 110 of the first 120 matrices.
- **Claim 2** (supported): At n=33 there are 10,800 allowed permutations, split into 5,400 even and 5,400 odd permutations. [3](#reference-3)
- **Claim 3** (reported): Powers of 2, powers of 3, and tribonacci numbers were reported to have the same determinant property in tested ranges. [3](#reference-3)
- **Claim 4** (reported): The peeled core retains the same Fibonacci-sum entry rule on a sparse, symmetric subset of row and column indices.
- **Claim 5** (supported): An observed row, including its primary gap, reappears as the middle block of the row four levels later. [3](#reference-3)
- **Claim 6** (supported): The first block of one row mirrors the final block of the previous row, and much of the middle block mirrors into the next final block. [3](#reference-3)
- **Claim 7** (supported): The repeated-block symmetry fails near boundaries where the initial support-difference sequence is copied into later rows. [3](#reference-3)
- **Claim 8** (reported): The MathOverflow author previously reported receiving claimed AI proofs without publishing their text. [3](#reference-3)

### Prior approaches

- **Route 1** (incomplete method): Repeatedly expand along a row or column with one nonzero entry and hope the matrix disappears.

### Open directions

- **Conjecture 1** (reported): Initial tests suggested the Fibonacci construction extends to Lucas sequences, including Lucas and Pell numbers. [3](#reference-3)
- **Conjecture 2** (supported): The largest observed gaps run from F_{k-1}+F_{k-4}-1 to F_k+F_{k-5}, with sizes 8,12,19,30,48,77 and onward. [3](#reference-3)
- **Conjecture 3** (supported): A shifted family appears between F_k+F_{k-5}+F_{k-8}-1 and F_k+F_{k-4}+F_{k-9}. [3](#reference-3)
- **Conjecture 4** (supported): A third observed family runs from F_k+F_{k-4}+F_{k-7}-1 to F_k+F_{k-4}+F_{k-6}, with sizes 3,4,6,9,14,22 and onward. [3](#reference-3)
- **Question 1** (supported): For the n by n matrix M_n with entry 1 exactly when i+j is Fibonacci, prove det M_n belongs to {-1,0,1} for every n. [3](#reference-3)
- **Route 2** (conjectured): Pair allowed permutations of opposite parity, leaving at most one fixed exception, to explain the determinant bound directly.
- **Route 3** (conjectured): Find integer row and column operations reducing M_n or its core to blocks with determinants 0, 1, or -1.
- **Route 4** (supported): Identify each residual core with a smaller Fibonacci-sum matrix or a bounded family of related matrices.
- **Route 5** (supported): Express surviving core indices by Zeckendorf bit patterns and fit the observed replication and mirror rules.
- **Route 6** (conjectured): Compute Smith normal forms of M_n and residual cores to test whether all nonzero invariant factors are one.
- **Route 7** (conjectured): Treat M_n as a bipartite adjacency matrix and study cancellation among perfect matchings through alternating cycles.
- **Route 8** (conjectured): Determine which increasing integer sequences make every finite sum-indicator matrix totally unimodular. [3](#reference-3)
- **Route 9** (conjectured): Look for sum-indicator matrices, Hankel-like Fibonacci supports, total unimodularity criteria, and related determinant recurrences.
- **Route 10** (conjectured): Define M_n over integers, state the determinant bound, and first certify forced-peeling and finite computational cases.
- **Route 11** (review pending): A complete argument through the outerplanar, chordal-bipartite support graph and Camion's criterion is recorded and awaits independent review.

### Formalizations

- **Formalization 1** (reported): The checked Lean object uses Matrix (Fin n) (Fin n) Int with entries determined by Fibonacci membership after converting indices to one-based naturals.
- **Formalization 2** (reported): Lean proves that every support square has corner sums q_(t-2), q_t, q_t, q_(t+1) and equal row and column increments q_(t-1).
- **Formalization 3** (reported): Lean proves that a least-order bad sign minor has determinant plus or minus two and none of its cofactors vanish.
- **Formalization 4** (reported): A reusable Lean theorem reduces total unimodularity to divisibility by four for square submatrices with even row and column sums.
- **Formalization 5** (reported): Lean proves that every Eulerian selected support is covered with odd multiplicity by finitely many contained support squares.
- **Formalization 6** (reported): The problem-specific Lean obligation says that every square Fibonacci-sum submatrix with even row and column sums contains a multiple of four ones.
- **Formalization 7** (reported): The checked Lean reduction combines Camion's criterion with the Fibonacci-specific divisibility obligation.
- **Formalization 8** (reported): The exact public target now has a checked Lean proof from the total-unimodularity obligation.

### Runnable artifacts

- **Artifact 1** (supported): The source reports 10,800 allowed permutations at n=33 with an even split by sign. [3](#reference-3)
- **Artifact 2** (supported): A table records nonzero indices, their Zeckendorf bit strings, and successive gaps through n=1219. [3](#reference-3)
- **Artifact 3** (supported): A MathOverflow image marks replicated, mirrored, and boundary-affected blocks in the support-gap sequence. [3](#reference-3)
- **Artifact 4** (conjectured): Compute residual cores through n=500, retain exact index sets, and search for a recursive Zeckendorf map.
- **Artifact 5** (reproduced): A dependency-free Python program reconstructs M_n and verifies the determinant range through n=120 using exact arithmetic.
- **Artifact 6** (reproduced): For the sequence 2,6,8,14,22,36,58, the 5 by 5 sum-indicator matrix has determinant 2.
- **Artifact 7** (reproduced): The executable sweep reports a nonempty residual core for 110 of n=1 through 120.
- **Artifact 8** (reproduced): The checker can emit the surviving row and column sets after forced peeling for each n.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `fib-problem-nonzero-support`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

8 declarations, with 0 open proof obligations.

### fibSumMatrix_det_range

- State: source contains no sorry; verification pending
- Role: target declaration
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`
- Depends on: `fibSumMatrix_totallyUnimodular`

```lean
theorem fibSumMatrix_det_range : DeterminantRangeStatement := by
  intro n
  obtain ⟨s, hs⟩ := fibSumMatrix_totallyUnimodular n n id id Function.injective_id Function.injective_id
  cases s <;> simp_all
```

### fibSumMatrix_totallyUnimodular

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`
- Depends on: `fibSumMatrix`, `isTotallyUnimodular_of_camion`, `fibSumMatrix_camion_divisibility`

```lean
theorem fibSumMatrix_totallyUnimodular (n : ℕ) : (fibSumMatrix n).IsTotallyUnimodular := by
  classical
  apply TheoremDB.Matrix.isTotallyUnimodular_of_camion
  · intro i j
    by_cases h : IsFibonacci (i.val + j.val + 2)
    · use 1
      simp [fibSumMatrix, h]
    · use 0
      simp [fibSumMatrix, h]
  · exact fibSumMatrix_camion_divisibility n
```

### fibSumMatrix

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`

```lean
noncomputable def fibSumMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℤ := fun i j => if IsFibonacci (i.val + j.val + 2) then 1 else 0
```

### fibSumMatrix_camion_divisibility

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`
- Depends on: `fibSubmatrixSupport_has_odd_square_cover`

```lean
theorem fibSumMatrix_camion_divisibility (n k : ℕ) (f : Fin k → Fin n) (g : Fin k → Fin n) (hf : f.Injective) (hg : g.Injective) (hrows : HasEvenRowSums ((fibSumMatrix n).submatrix f g)) (hcols : HasEvenColumnSums ((fibSumMatrix n).submatrix f g)) : (4 : ℤ) ∣ entrySum ((fibSumMatrix n).submatrix f g) := by
  rw [entrySum_fibSumMatrix_submatrix]
  exact_mod_cast fibSubmatrixSupport_card_dvd_four n k f g hf hg hrows hcols
```

### isTotallyUnimodular_of_camion

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`
- Depends on: `minimal_bad_square_minor_det_and_adjugate_nonzero`

```lean
theorem isTotallyUnimodular_of_camion {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (A : Matrix m n ℤ) (hentries : ∀ i j, A i j ∈ Set.range SignType.cast) (hcamion : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), f.Injective → g.Injective → HasEvenRowSums (A.submatrix f g) → HasEvenColumnSums (A.submatrix f g) → (4 : ℤ) ∣ entrySum (A.submatrix f g)) : A.IsTotallyUnimodular := by
  by_contra hA
  rcases exists_minimal_bad_square_minor A hA with ⟨k, f, g, hf, hg, hbad, hminimal⟩
  rcases minimal_bad_square_minor_is_camion_obstruction A hentries k f g hf hg hbad hminimal with ⟨hrows, hcols, hnot_four⟩
  exact hnot_four (hcamion k f g hf hg hrows hcols)
```

### fibSubmatrixSupport_has_odd_square_cover

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`
- Depends on: `fibonacci_support_four_corner_classification`

```lean
theorem fibSubmatrixSupport_has_odd_square_cover (n k : ℕ) (f : Fin k → Fin n) (g : Fin k → Fin n) (hf : f.Injective) (hg : g.Injective) (hrows : HasEvenRowSums ((fibSumMatrix n).submatrix f g)) (hcols : HasEvenColumnSums ((fibSumMatrix n).submatrix f g)) : ∃ faces : Finset (SelectedSupportSquare n k f g), ∀ edge ∈ fibSubmatrixSupport n k f g, Odd (faces.filter fun S => edge ∈ S.edges).card := by
  -- Kernel-checked square-toggle induction in OddSquareCover.lean
```

### minimal_bad_square_minor_det_and_adjugate_nonzero

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`

```lean
theorem minimal_bad_square_minor_det_and_adjugate_nonzero {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (A : Matrix m n ℤ) (hentries : ∀ i j, A i j ∈ Set.range SignType.cast) (k : ℕ) (f : Fin k → m) (g : Fin k → n) (hf : f.Injective) (hg : g.Injective) (hbad : (A.submatrix f g).det ∉ Set.range SignType.cast) (hminimal : ∀ (l : ℕ), l < k → ∀ (f' : Fin l → m) (g' : Fin l → n), f'.Injective → g'.Injective → (A.submatrix f' g').det ∈ Set.range SignType.cast) (hk : 3 ≤ k) : ((A.submatrix f g).det = 2 ∨ (A.submatrix f g).det = -2) ∧ ∀ i j, (A.submatrix f g).adjugate i j ≠ 0 := by
  exact ⟨minimal_bad_square_minor_det_eq_two_or_neg_two A k f g hf hg hbad hminimal hk, minimal_bad_square_minor_adjugate_nonzero A k f g hf hg hbad hminimal (by omega)⟩
```

### fibonacci_support_four_corner_classification

- State: source contains no sorry; verification pending
- Role: dependency depth 4
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc`
- Depends on: `fibSumMatrix`

```lean
theorem fibonacci_support_four_corner_classification {x X y Y : ℕ} (_hx : x < X) (hy : y < Y) (hmiddle : x + Y ≤ X + y) (hA : IsFibonacci (x + y + 2)) (hB : IsFibonacci (x + Y + 2)) (hC : IsFibonacci (X + y + 2)) (hD : IsFibonacci (X + Y + 2)) : ∃ t : ℕ, 3 ≤ t ∧ x + y + 2 = positiveFib (t - 2) ∧ x + Y + 2 = positiveFib t ∧ X + y + 2 = positiveFib t ∧ X + Y + 2 = positiveFib (t + 1) ∧ X = x + positiveFib (t - 1) ∧ Y = y + positiveFib (t - 1) := by
  -- Checked proof in formal/lean/TheoremDB/Fibonacci/Graph.lean
```

## References

1. <a id="reference-1"></a>Andrii Arman, David S. Gunderson, and Pak Ching Li, “Properties of the Fibonacci-sum graph”. arXiv:1710.10303 (2017). The outerplanarity result for the Fibonacci-sum graph https://arxiv.org/abs/1710.10303
   - preprint; primary source; arXiv:1710.10303v1; checked 2026-08-01
   - Source use: original_summary
   - For fib problem determinant range; fib problem nonzero support: Supplies the graph-theoretic antecedent used in the packet's independent proof of outerplanarity for the bipartite support graph.
   - Supplies the graph-theoretic antecedent used in the packet's independent proof of outerplanarity for the bipartite support graph.
2. <a id="reference-2"></a>Paul Camion, “Characterization of totally unimodular matrices”. Proceedings of the American Mathematical Society 16(5) (1965), 1068-1073. DOI 10.1090/S0002-9939-1965-0180568-2. Characterization theorem, pp. 1068-1073 https://doi.org/10.1090/S0002-9939-1965-0180568-2
   - journal_article; primary source; publisher version; checked 2026-08-01
   - Source use: original_summary
   - For fib problem determinant range; fib problem nonzero support: Supplies the total-unimodularity criterion applied in the final step of the proof.
   - Supplies the total-unimodularity criterion applied in the final step of the proof.
3. <a id="reference-3"></a>Philip Weiss, Is the determinant of this "Fibonacci sum" indicator matrix always -1, 0, or 1?, MathOverflow question 513340 (2026), with answers and comments. Question, answers, and comments cited by the individual research records. https://mathoverflow.net/questions/513340/is-the-determinant-of-this-fibonacci-sum-indicator-matrix-always-1-0-or/513372
   - Also cited at question line 60
   - Also cited at question line 64
   - Also cited at comment line 135
   - Also cited at answer lines 304-306
   - Also cited at answer lines 305-306
   - Also cited at answer line 306
   - Also cited at answer lines 327-371
   - Also cited at comment lines 109-135
   - Also cited at answer line 303
   - Also cited at question lines 57-60
   - Also cited at MathOverflow comments
   - Also cited at answer lines 169-306
   - Also cited at answer image after line 304
   - forum; primary source; web version checked 2026-08-01; checked 2026-08-01
   - Source use: original_summary
   - For fib problem determinant range; fib problem nonzero support: Supplies the problem statement, reported computations, discussion, and community observations recorded in the packet.
   - Source named by the research packet.