# P2: Determinants of the Fibonacci-sum matrix

- ID: `P2`
- Reference: `fib-problem-determinant-range`
- Page: https://theoremdb.org/statements/P2
- 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} \] Prove that \(\det(M_n)\i

## The answer

For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}.

**Review status:** Established.

**Lean verification:** signed verification record `fib-formalization-determinant-range-lean-v1-lean-5e5b725441ec-verified-e4e988240074` is attached to the live packet.

### Proof

Let

$$
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\}$.

1. The support graph.

Let $Q_n$ be the bipartite graph with row vertices
$r_1,\ldots,r_n$, column vertices $c_1,\ldots,c_n$, and an edge
$r_i c_j$ exactly when $i+j$ is Fibonacci. The matrix $M_n$ is the
biadjacency matrix of $Q_n$. A diagonal entry of $M_n$ becomes the ordinary
bipartite edge $r_i c_i$, so loops never arise in $Q_n$.

The ordinary loopless Fibonacci-sum graph has analogous chord and
outerplanarity properties [1](#reference-1). The argument below treats the
bipartite row-column support graph directly.

Lemma 1. $Q_n$ is chordal bipartite.

Every cycle of length at least six has a chord.

Take such a cycle and let $m$ be its largest numerical label. Row-column
symmetry lets us suppose that $r_m$ lies on the cycle. Choose $k$ with

$$
q_k\leq m<q_{k+1}.
$$

If $c_j$ is a neighbor of $r_m$ whose label is at most $m$, then
$m+j\in(m,2m]$. The only possible Fibonacci numbers in this interval are
$q_{k+1}$ and $q_{k+2}$. If $q_{k+2}>2m$, this gives at most one
neighbor, so $r_m$ cannot lie on a cycle. We may therefore assume
$q_{k+2}\leq 2m$. The two cycle neighbors of $r_m$ must then be

$$
c_a,\quad c_b,\qquad
a=q_{k+1}-m,\quad b=q_{k+2}-m.
$$

Put $z=m-q_k$. We have $b>q_k$. Among vertices with labels at most $m$,
the vertex $c_b$ therefore has exactly two neighbors, namely $r_m$ and
$r_z$, because

$$
b+m=q_{k+2},\qquad b+z=q_{k+1}.
$$

Also

$$
a+z=(q_{k+1}-m)+(m-q_k)=q_{k-1}.
$$

Thus the cycle contains the path

$$
c_a-r_m-c_b-r_z
$$

and $r_zc_a$ is an edge. On a cycle of length at least six, that edge is a
chord. The same calculation covers $b=m$. In that case $a=z$, while
$r_a,c_a,r_m,c_m$ are still four distinct graph vertices.

Lemma 2. Every edge of $Q_n$ lies in at most two four-cycles.

First classify the four-cycles in the infinite version of the graph. Suppose a
four-cycle uses rows $x<X$ and columns $y<Y$. Set

$$
A=x+y,\quad B=x+Y,\quad C=X+y,\quad D=X+Y.
$$

All four numbers are Fibonacci, $A<B,C<D$, and

$$
A+D=B+C.
$$

Assume $B\leq C$, and write

$$
A=q_\alpha,\quad B=q_\beta,\quad C=q_\gamma,\quad D=q_\delta.
$$

Then

$$
q_\delta-q_\gamma=q_\beta-q_\alpha.
$$

If $\delta\geq\gamma+2$, the left side is at least $q_{\gamma+1}$,
while the right side is smaller than $q_\beta\leq q_\gamma$. Hence
$\delta=\gamma+1$, and the common difference is $q_{\gamma-1}$.
If $\beta\leq\gamma-1$, the right side is smaller than
$q_\beta\leq q_{\gamma-1}$. Hence $\beta=\gamma$, followed by
$\alpha=\gamma-2$.

Writing $t=\gamma$, every four-cycle has corner sums

$$
q_{t-2},\quad q_t,\quad q_t,\quad q_{t+1},
$$

and its row and column increments are both

$$
q_t-q_{t-2}=q_{t-1}.
$$

Now fix an edge $r_xc_y$ with $x+y=q_s$. It can occur in a classified
four-cycle in three ways:

1. As the $q_{t-2}$ corner. This determines at most one four-cycle.

2. As the $q_{t+1}$ corner. This determines at most one four-cycle and
   requires $x,y>q_{s-2}$.

3. As one of the two $q_t$ corners. The two orientations require,
   respectively, $x>q_{s-1}$ or $y>q_{s-1}$.

The two orientations in the third case cannot both occur, since
$x+y=q_s<2q_{s-1}$. The second and third cases cannot occur together,
since their inequalities would give

$$
x+y>q_{s-2}+q_{s-1}=q_s.
$$

There is therefore at most one four-cycle from the first case and at most one
from the other two cases combined.

Lemma 3. $Q_n$ is outerplanar.

We construct an outerplane embedding by induction on $n$. The claim is
immediate for $n=1$. Assume $Q_{m-1}$ has an outerplane embedding, and
choose $k$ with $q_k\leq m<q_{k+1}$. Set

$$
a=q_{k+1}-m.
$$

If $2m<q_{k+2}$, the new vertices $r_m,c_m$ add the two pendant edges
$r_mc_a$ and $r_ac_m$. Draw them in the outer face.

Suppose $2m=q_{k+2}$. Then

$$
a=m-q_k,\qquad 2a=q_{k-1}.
$$

The old graph contains $r_ac_a$, and the two new vertices complete the
four-cycle

$$
r_a-c_a-r_m-c_m-r_a.
$$

Suppose $2m>q_{k+2}$. Put

$$
b=q_{k+2}-m,\qquad z=m-q_k.
$$

Here $b<m$. In $Q_{m-1}$, $c_b$ is pendant at $r_z$, and $r_b$
is pendant at $c_z$. The new vertices complete two four-cycles, attached
along the old edges

$$
r_zc_a\qquad\text{and}\qquad r_ac_z.
$$

In both the equality and strict cases, each attachment edge borders the outer
face of the chosen embedding. To see this, suppose an attachment edge bordered
two bounded faces. It lies in a two-connected block. Each of those faces has
an induced cycle as its boundary, and Lemma 1 makes each boundary a
four-cycle. The new four-cycle would place the attachment edge in three
four-cycles, contrary to Lemma 2.

We can therefore draw each new four-cycle in the outer face beside its
attachment edge. The old pendant vertices $c_b$ and $r_b$ can be moved
within that face into the required positions. In the last case the two
attachment edges are vertex-disjoint, since

$$
z-a=2m-q_{k+2}>0.
$$

This completes the induction.

2. The divisibility condition.

We need one plane-graph observation.

Lemma 4. Eulerian outerplane quadrangulations have a multiple of four edges.

Let $H$ be an outerplane graph in which every vertex has even degree and
every bounded face is a four-cycle. Then $|E(H)|$ is divisible by four.

It is enough to work one connected component at a time. A connected graph in
which every vertex has even degree has no bridges. Its plane dual is bipartite,
so its faces admit a black-white coloring with adjacent faces receiving
opposite colors. Color the outer face white. Every edge then borders exactly
one black face. All black faces are bounded four-faces, and hence

$$
|E(H)|
=\sum_{\text{black faces }f}|\partial f|
=4\cdot\#\{\text{black faces}\}.
$$

3. Camion's criterion.

Camion's criterion [2](#reference-2) says that a $0,\pm1$ matrix is totally
unimodular if and only if the sum of the entries in every square submatrix
with even row sums and even column sums is divisible by four.

Take any square submatrix $B=M_n[I,J]$ whose row and column sums are even.
Its support graph is the subgraph of $Q_n$ induced by

$$
\{r_i:i\in I\}\cup\{c_j:j\in J\}.
$$

This graph remains outerplanar and chordal bipartite. Every vertex has even
degree. In an outerplane embedding, each bounded face is an induced cycle
inside a two-connected block. Lemma 1 makes every such face a four-cycle.
Lemma 4 now gives

$$
\sum_{i\in I,\ j\in J} B_{ij}=|E(B)|\equiv0\pmod4.
$$

Camion's criterion applies to every such $B$. Thus $M_n$ is totally
unimodular for every $n$, which proves

$$
\boxed{\det M_n\in\{-1,0,1\}\quad\text{for every }n\geq1.}
$$

**Sources cited in proof:** [1 Andrii Arman (2017)](#reference-1); [2 Paul Camion (1965)](#reference-2).

## Work

### Proof and evidence for the resolution

**Theorem 1 (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. Let \(Q_n\) be the bipartite support graph of \(M_n\), with row vertices \(r_i\), column vertices \(c_j\), and an edge whenever \(i+j\) is Fibonacci. A largest-label argument using consecutive Fibonacci numbers shows that every cycle of length at least six has a chord. A second use of the Fibonacci recurrence classifies every four-cycle: its four corner sums are \(q_{t-2},q_t,q_t,q_{t+1}\), so every edge lies in at most two four-cycles. These facts support an induction that embeds \(Q_n\) outerplanarly.

Now take any square submatrix \(B\) of \(M_n\) whose row and column sums are even. Its support graph is an Eulerian induced subgraph of \(Q_n\). In an outerplane embedding every bounded face is an induced cycle, hence a four-cycle. Color the faces black and white with the outer face white. Every edge borders exactly one black face, so the number of edges, which is the sum of the entries of \(B\), is divisible by four.

Camion's criterion now applies: a \(0,\!\pm\!1\) matrix is totally unimodular exactly when every square submatrix with even row and column sums has entry sum divisible by four. Therefore every square minor of \(M_n\) belongs to \(\{-1,0,1\}\). In particular, \(\det(M_n)\in\{-1,0,1\}\) for every \(n\ge1\).

### Supporting 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)
- **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 1** (supported): At n=33 there are 10,800 allowed permutations, split into 5,400 even and 5,400 odd permutations. [3](#reference-3)
- **Claim 2** (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 3** (reported): The peeled core retains the same Fibonacci-sum entry rule on a sparse, symmetric subset of row and column indices.
- **Claim 4** (supported): An observed row, including its primary gap, reappears as the middle block of the row four levels later. [3](#reference-3)
- **Claim 5** (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 6** (supported): The repeated-block symmetry fails near boundaries where the initial support-difference sequence is copied into later rows. [3](#reference-3)
- **Claim 7** (reported): The MathOverflow author previously reported receiving claimed AI proofs without publishing their text. [3](#reference-3)
- **Claim 8** (supported): 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)

### 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): Describe all n for which det M_n is nonzero and explain why those indices cluster above Fibonacci numbers. [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-determinant-range`, 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
```

### Continue Lean verification

Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.

[Continue Lean verification with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20fib-problem-determinant-range%0A%0AExact%20title%3A%20Determinants%20of%20the%20Fibonacci-sum%20matrix%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Ffib-problem-determinant-range%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## 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 65-67
   - 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.