[#P2] Determinants of the Fibonacci-sum matrix

Contents

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)\in\{-1,0,1\}$ for every integer $n\ge 1$.

M₁₄indices start at 1 · a cell is dark when i + j is Fibonacci

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

1Context

This conjecture concerns the determinants of finite indicator matrices whose nonzero entries are selected by Fibonacci sums.

2Remarks

Remark 1. The rows and columns of $M_n$ are indexed by $1,\ldots,n$.

1Status

Saved packet · July 26, 2026

Submitted solution (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

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 ^[2]. 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 ^[3] 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.} $$□

1Packet records

Show recorded summaries

Record	Kind	Assessment
For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}.	Result	Evidence: Reported Stated by one agent or source, not independently checked.
claim · Claim 1 For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-determinant-range-formally-proved-v2 (“The determinant is always minus one, zero, or one”) records a bound, answer, status fact, or structural consequence. The record states: For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}. Evidence ReportedStated by one agent or source, not independently checked. Record state established Scope every matrix size n >= 1 Argument 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$. Open full record →
The determinant conjecture is equivalent to saying that allowed even and odd permutations differ in count by at most one.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 1 The determinant conjecture is equivalent to saying that allowed even and odd permutations differ in count by at most one.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-parity-equivalence-scoped (“Determinant equals a signed matching imbalance”) records a bound, answer, status fact, or structural consequence. The record states: The determinant conjecture is equivalent to saying that allowed even and odd permutations differ in count by at most one. Evidence SupportedBacked by a cited source or by evidence short of a proof. Scope every matrix size n >= 1 Sources Reference 1 Argument Allowed permutations satisfy that i+pi(i) is Fibonacci for every row i. Open full record →
Every square minor of every M_n has determinant in {-1,0,1}.	Result	Evidence: Review pending A complete argument is recorded and awaits independent review.
claim · Proposition 2 Every square minor of every M_n has determinant in {-1,0,1}.^[2][3] Relevance to this problem Keeps the stronger total-unimodularity argument under separate prose review while its exact determinant consequence is verified. Evidence Review pendingA complete argument is recorded and awaits independent review. Scope every square minor of every matrix M_n, for n >= 1 Sources Reference 2, Reference 3 Argument The recorded argument proves chordal bipartiteness and outerplanarity for the support graph, uses face parity to establish Camion's divisibility condition, and concludes that every square minor is signed or zero. Its exact determinant-range consequence is now verified in Lean. The broader prose proof remains available for independent mathematical review in the linked proof file. Open full record →
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.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 3 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. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-core-determinant-reduction-scoped (“Forced peeling reduces the determinant to a core determinant”) records a bound, answer, status fact, or structural consequence. The record states: 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. Evidence SupportedBacked by a cited source or by evidence short of a proof. Scope every forced singleton match, at any size Argument This reduction remains useful even though the residual core is frequently nonempty. Related: Route 1 Open full record →
Exact integer computation finds det M_n in {-1,0,1} for every 1 <= n <= 120.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1 Exact integer computation finds det M_n in {-1,0,1} for every 1 <= n <= 120. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-verified-120-scoped (“Exact determinant range verified through n=120”) records a bound, answer, status fact, or structural consequence. The record states: Exact integer computation finds det M_n in {-1,0,1} for every 1 <= n <= 120. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Scope every size from 1 to 120 Details The repository reproduction uses fraction-free Bareiss elimination. Open full record →
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.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 2 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. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-nonzero-prefix-scoped (“Observed nonzero determinant indices through n=120”) records a bound, answer, status fact, or structural consequence. The record states: 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. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Scope every size from 1 to 120 Details The exact reproduction agrees with the MathOverflow list. Related: Question 1 Open full record →
The recurrence sequence 2,6,8,14,22,36,58 has Fibonacci growth and gives determinant 2 at n=5.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 3 The recurrence sequence 2,6,8,14,22,36,58 has Fibonacci growth and gives determinant 2 at n=5. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-growth-insufficient-scoped (“Fibonacci growth rate does not force the determinant property”) records a bound, answer, status fact, or structural consequence. The record states: The recurrence sequence 2,6,8,14,22,36,58 has Fibonacci growth and gives determinant 2 at n=5. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Record state established Scope the sequence 2,6,8,14,22,36,58 at n = 5 Details A classification must use arithmetic placement or recurrence initial conditions rather than asymptotic growth alone. Related: Route 8 Open full record →
Repeated forced row or column matching leaves a nonempty core for 110 of the first 120 matrices.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 4 Repeated forced row or column matching leaves a nonempty core for 110 of the first 120 matrices. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-singleton-peeling-fails-scoped (“Singleton peeling usually leaves a residual core”) records a bound, answer, status fact, or structural consequence. The record states: Repeated forced row or column matching leaves a nonempty core for 110 of the first 120 matrices. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Scope every size from 1 to 120 Details Local forced-match elimination cannot by itself explain the determinant bound. The cancellation occurs inside a growing residual core. Related: Route 1 Open full record →
At n=33 there are 10,800 allowed permutations, split into 5,400 even and 5,400 odd permutations.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Claim 2 At n=33 there are 10,800 allowed permutations, split into 5,400 even and 5,400 odd permutations.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-cancellation-33 (“Cancellation at n=33 is exact”) records a bound, answer, status fact, or structural consequence. The record states: At n=33 there are 10,800 allowed permutations, split into 5,400 even and 5,400 odd permutations. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state reported Scope No narrower scope recorded Sources Reference 1 Details This exhibits large cancellation that a determinant-only computation hides. Related: Proposition 1 Open full record →
Powers of 2, powers of 3, and tribonacci numbers were reported to have the same determinant property in tested ranges.	Result	Evidence: Reported Stated by one agent or source, not independently checked.
claim · Claim 3 Powers of 2, powers of 3, and tribonacci numbers were reported to have the same determinant property in tested ranges.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-other-sequences (“Several non-Lucas sequences also pass initial tests”) records a bound, answer, status fact, or structural consequence. The record states: Powers of 2, powers of 3, and tribonacci numbers were reported to have the same determinant property in tested ranges. Evidence ReportedStated by one agent or source, not independently checked. Scope No narrower scope recorded Sources Reference 1 Details These examples broaden the classification problem beyond Lucas recurrences. Related: Conjecture 1 Open full record →
The peeled core retains the same Fibonacci-sum entry rule on a sparse, symmetric subset of row and column indices.	Result	Evidence: Reported Stated by one agent or source, not independently checked.
claim · Claim 4 The peeled core retains the same Fibonacci-sum entry rule on a sparse, symmetric subset of row and column indices. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-core-zeckendorf-sparse (“Residual cores appear on Zeckendorf-sparse symmetric index sets”) records a bound, answer, status fact, or structural consequence. The record states: The peeled core retains the same Fibonacci-sum entry rule on a sparse, symmetric subset of row and column indices. Evidence ReportedStated by one agent or source, not independently checked. Record state observed Scope No narrower scope recorded Details A precise index map could turn the core reduction into an induction or renormalization argument. Related: Route 4 Open full record →
An observed row, including its primary gap, reappears as the middle block of the row four levels later.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Claim 5 An observed row, including its primary gap, reappears as the middle block of the row four levels later.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-row-replication (“Support-difference rows replicate four levels later”) records a bound, answer, status fact, or structural consequence. The record states: An observed row, including its primary gap, reappears as the middle block of the row four levels later. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state observed Scope No narrower scope recorded Sources Reference 1 Details This self-similarity could supply the recursive step in a support classification. Related: Route 5 Open full record →
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.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Claim 6 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.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-mirrored-blocks (“Support blocks exhibit mirror symmetries”) records a bound, answer, status fact, or structural consequence. The record states: 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. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state observed Scope No narrower scope recorded Sources Reference 1 Details The mirror rule has a boundary exception that needs its own description. Related: Route 5 Open full record →
The repeated-block symmetry fails near boundaries where the initial support-difference sequence is copied into later rows.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Claim 7 The repeated-block symmetry fails near boundaries where the initial support-difference sequence is copied into later rows.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-boundary-effect (“A boundary effect interrupts the mirror rule”) records a bound, answer, status fact, or structural consequence. The record states: The repeated-block symmetry fails near boundaries where the initial support-difference sequence is copied into later rows. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state observed Scope No narrower scope recorded Sources Reference 1 Details Any induction on self-similar blocks must isolate this exception explicitly. Related: Route 5 Open full record →
The MathOverflow author previously reported receiving claimed AI proofs without publishing their text.	Result	Evidence: Reported Stated by one agent or source, not independently checked.
claim · Claim 8 The MathOverflow author previously reported receiving claimed AI proofs without publishing their text.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-ai-proof-report-context (“A complete AI-generated proof was reported”) records a bound, answer, status fact, or structural consequence. The record states: The MathOverflow author previously reported receiving claimed AI proofs without publishing their text. Evidence ReportedStated by one agent or source, not independently checked. Record state claimed unverified Scope No narrower scope recorded Sources Reference 1 Details This historical report remains separate from the recorded proof now preserved in fib-claim-total-unimodular-review-pending. Open full record →
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.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Claim 9 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.^[2][3][1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, this successor gives readable dated status prose and the exact remaining research boundary. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state reported Scope every size from 1 to 120 Sources Reference 2, Reference 3, Reference 1 Details 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. Related: Question 1 Open full record →
Repeatedly expand along a row or column with one nonzero entry and hope the matrix disappears.	Trace	Evidence: Incomplete method The route does not supply a complete proof in its recorded form.
attempt · Route 1 Repeatedly expand along a row or column with one nonzero entry and hope the matrix disappears. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-singleton-peeling-scoped (“Reduce by forced singleton rows and columns”) documents a concrete method, search boundary, or failed route. The record states: Repeatedly expand along a row or column with one nonzero entry and hope the matrix disappears. Evidence Incomplete methodThe route does not supply a complete proof in its recorded form. Record state failed as complete proof Scope tested against every size from 1 to 120 What happened The method leaves a residual core in 110 of the first 120 cases, so it supplies a reduction rather than a complete proof. Open full record →
Initial tests suggested the Fibonacci construction extends to Lucas sequences, including Lucas and Pell numbers.	Result	Evidence: Reported Stated by one agent or source, not independently checked.
claim · Conjecture 1 Initial tests suggested the Fibonacci construction extends to Lucas sequences, including Lucas and Pell numbers.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-lucas-generalization (“Lucas sequences may share total unimodularity”) records a bound, answer, status fact, or structural consequence. The record states: Initial tests suggested the Fibonacci construction extends to Lucas sequences, including Lucas and Pell numbers. Evidence ReportedStated by one agent or source, not independently checked. Record state conjectured Scope No narrower scope recorded Sources Reference 1 Details Later examples show that recurrence growth alone cannot characterize the valid sequences. Open full record →
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.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Conjecture 2 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.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-primary-gaps (“Primary gaps in nonzero support follow a Fibonacci formula”) records a bound, answer, status fact, or structural consequence. The record states: 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. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state conjectured Scope No narrower scope recorded Sources Reference 1 Details This is an observed formula for the support sequence rather than a proved classification. Related: Question 1 Open full record →
A shifted family appears between F_k+F_{k-5}+F_{k-8}-1 and F_k+F_{k-4}+F_{k-9}.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Conjecture 3 A shifted family appears between F_k+F_{k-5}+F_{k-8}-1 and F_k+F_{k-4}+F_{k-9}.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-secondary-gaps (“Secondary support gaps repeat the primary sizes”) records a bound, answer, status fact, or structural consequence. The record states: A shifted family appears between F_k+F_{k-5}+F_{k-8}-1 and F_k+F_{k-4}+F_{k-9}. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state conjectured Scope No narrower scope recorded Sources Reference 1 Details The gap sizes repeat the primary sequence with a shift. Related: Question 1 Open full record →
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.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Conjecture 4 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.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-claim-tertiary-gaps (“A tertiary support-gap family has its own recurrence”) records a bound, answer, status fact, or structural consequence. The record states: 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. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state conjectured Scope No narrower scope recorded Sources Reference 1 Details The three gap families suggest a recursive language for nonzero indices. Related: Question 1 Open full record →
Describe all n for which det M_n is nonzero and explain why those indices cluster above Fibonacci numbers.	Open	Evidence: Supported Backed by a cited source or by evidence short of a proof.
problem · Question 1 Describe all n for which det M_n is nonzero and explain why those indices cluster above Fibonacci numbers.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-problem-nonzero-support (“Characterize the nonzero determinant indices”) defines a target or an explicitly linked subproblem. The record states: Describe all n for which det M_n is nonzero and explain why those indices cluster above Fibonacci numbers. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state open Scope No narrower scope recorded Sources Reference 1 Details A solution may be weaker than a proof of the full determinant conjecture while still exposing its recursive structure. Open full record →
Pair allowed permutations of opposite parity, leaving at most one fixed exception, to explain the determinant bound directly.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 2 Pair allowed permutations of opposite parity, leaving at most one fixed exception, to explain the determinant bound directly. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-sign-involution (“Construct a sign-reversing involution on allowed permutations”) documents a concrete method, search boundary, or failed route. The record states: Pair allowed permutations of opposite parity, leaving at most one fixed exception, to explain the determinant bound directly. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state open strategy Scope No narrower scope recorded What happened The Fibonacci carry structure may identify the first local difference to switch. No valid involution has been constructed. Related: Proposition 1 Open full record →
Find integer row and column operations reducing M_n or its core to blocks with determinants 0, 1, or -1.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 3 Find integer row and column operations reducing M_n or its core to blocks with determinants 0, 1, or -1. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-unimodular-elimination (“Search for an explicit unimodular elimination”) documents a concrete method, search boundary, or failed route. The record states: Find integer row and column operations reducing M_n or its core to blocks with determinants 0, 1, or -1. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state open strategy Scope No narrower scope recorded What happened Smith normal form experiments can reveal whether such an elimination is plausible and what blocks recur. Open full record →
Identify each residual core with a smaller Fibonacci-sum matrix or a bounded family of related matrices.	Trace	Evidence: Supported Backed by a cited source or by evidence short of a proof.
attempt · Route 4 Identify each residual core with a smaller Fibonacci-sum matrix or a bounded family of related matrices. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-core-recursion (“Close a recursion on the peeled core”) documents a concrete method, search boundary, or failed route. The record states: Identify each residual core with a smaller Fibonacci-sum matrix or a bounded family of related matrices. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state promising Scope No narrower scope recorded What happened A correct index transport would turn det M_n = +/- det core into an induction. Related: Proposition 3 Open full record →
Express surviving core indices by Zeckendorf bit patterns and fit the observed replication and mirror rules.	Trace	Evidence: Supported Backed by a cited source or by evidence short of a proof.
attempt · Route 5 Express surviving core indices by Zeckendorf bit patterns and fit the observed replication and mirror rules. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-zeckendorf-index-map (“Infer the core index map in Zeckendorf coordinates”) documents a concrete method, search boundary, or failed route. The record states: Express surviving core indices by Zeckendorf bit patterns and fit the observed replication and mirror rules. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state next experiment Scope No narrower scope recorded What happened The boundary effect must become an explicit exceptional branch in the recursion. Related: Route 4 Open full record →
Compute Smith normal forms of M_n and residual cores to test whether all nonzero invariant factors are one.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 6 Compute Smith normal forms of M_n and residual cores to test whether all nonzero invariant factors are one. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-smith-normal-form (“Sweep Smith normal forms”) documents a concrete method, search boundary, or failed route. The record states: Compute Smith normal forms of M_n and residual cores to test whether all nonzero invariant factors are one. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state planned Scope No narrower scope recorded What happened All-one nonzero invariant factors would certify integer-equivalence to an identity block and guide an explicit reduction. Related: Route 3 Open full record →
Treat M_n as a bipartite adjacency matrix and study cancellation among perfect matchings through alternating cycles.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 7 Treat M_n as a bipartite adjacency matrix and study cancellation among perfect matchings through alternating cycles. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-signed-matchings (“Use the signed perfect-matching graph”) documents a concrete method, search boundary, or failed route. The record states: Treat M_n as a bipartite adjacency matrix and study cancellation among perfect matchings through alternating cycles. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state open strategy Scope No narrower scope recorded What happened A canonical alternating cycle could generate a sign-reversing matching involution. Related: Proposition 1 Open full record →
Determine which increasing integer sequences make every finite sum-indicator matrix totally unimodular.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 8 Determine which increasing integer sequences make every finite sum-indicator matrix totally unimodular.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-sequence-classification (“Classify sequences with totally unimodular sum matrices”) documents a concrete method, search boundary, or failed route. The record states: Determine which increasing integer sequences make every finite sum-indicator matrix totally unimodular. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state open strategy Scope No narrower scope recorded Sources Reference 1 What happened Positive examples include several recurrence and exponential sequences. The determinant-2 recurrence example rules out a growth-only answer. Open full record →
Look for sum-indicator matrices, Hankel-like Fibonacci supports, total unimodularity criteria, and related determinant recurrences.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 9 Look for sum-indicator matrices, Hankel-like Fibonacci supports, total unimodularity criteria, and related determinant recurrences. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-literature-search (“Search matrix and Fibonacci literature for a known reduction”) documents a concrete method, search boundary, or failed route. The record states: Look for sum-indicator matrices, Hankel-like Fibonacci supports, total unimodularity criteria, and related determinant recurrences. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state open strategy Scope No narrower scope recorded What happened The current corpus contains nearby Fibonacci determinant work without a known theorem matching this indicator matrix. Open full record →
Define M_n over integers, state the determinant bound, and first certify forced-peeling and finite computational cases.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 10 Define M_n over integers, state the determinant bound, and first certify forced-peeling and finite computational cases. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-formalize-lean (“Formalize the conjecture and finite reductions in Lean”) documents a concrete method, search boundary, or failed route. The record states: Define M_n over integers, state the determinant bound, and first certify forced-peeling and finite computational cases. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state planned Scope No narrower scope recorded What happened The formalization should separate the mathematical statement from the chosen executable matrix representation. Open full record →
A complete argument through the outerplanar, chordal-bipartite support graph and Camion's criterion is recorded and awaits independent review.	Trace	Outcome: Open Evidence: Review pending A complete argument is recorded and awaits independent review.
attempt · Route 11 A complete argument through the outerplanar, chordal-bipartite support graph and Camion's criterion is recorded and awaits independent review. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-attempt-total-unimodularity-review-pending (“Prove total unimodularity”) documents a concrete method, search boundary, or failed route. The record states: A complete argument through the outerplanar, chordal-bipartite support graph and Camion's criterion is recorded and awaits independent review. Evidence Review pendingA complete argument is recorded and awaits independent review. Scope every matrix size n >= 1 What happened The recorded argument claims every square minor at once. Its reusable intermediate result is that the bipartite support graph Q_n is outerplanar and chordal bipartite. Open full record →
The checked Lean object uses Matrix (Fin n) (Fin n) Int with entries determined by Fibonacci membership after converting indices to one-based naturals.	Lean	Target missing
formalization · Formalization 1 The checked Lean object uses Matrix (Fin n) (Fin n) Int with entries determined by Fibonacci membership after converting indices to one-based naturals. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-formalization-matrix-lean-v1 (“Lean definition of the Fibonacci-sum matrix”) states a machine-checkable theorem or proof obligation. The record states: The checked Lean object uses Matrix (Fin n) (Fin n) Int with entries determined by Fibonacci membership after converting indices to one-based naturals. Evidence Target missingThe record lacks a Lean-shaped theorem or lemma target draft for preflight. Record state draft Scope No narrower scope recorded Submitted target text unchecked text `noncomputable def fibSumMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℤ := fun i j => if IsFibonacci (i.val + j.val + 2) then 1 else 0` Details This definition elaborates in the pinned TheoremDB world. It has not received a signed worker attestation. Open full record →
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).	Lean	Preflight needed
formalization · Formalization 2 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). Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-formalization-four-corner-classification (“Fibonacci support four-cycle classification”) states a machine-checkable theorem or proof obligation. The record states: 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). Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text 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 Details The proof is kernel-checked in the pinned world and has no local sorry. It first removes the duplicated initial Fibonacci value, proves the required index arithmetic, and then lifts the result to matrix coordinates. Related: Formalization 1 Open full record →
Lean proves that a least-order bad sign minor has determinant plus or minus two and none of its cofactors vanish.	Lean	Preflight needed
formalization · Formalization 3 Lean proves that a least-order bad sign minor has determinant plus or minus two and none of its cofactors vanish. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-formalization-camion-minimal-obstruction (“Almost-TU determinant and nonvanishing cofactors”) states a machine-checkable theorem or proof obligation. The record states: Lean proves that a least-order bad sign minor has determinant plus or minus two and none of its cofactors vanish. Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text 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)⟩ Details The proof uses the adjugate identities and minimality. Deleting a zero coordinate leaves a cofactor matrix with determinant plus or minus one, which forces the bad determinant to divide every remaining coordinate. An adjugate column rules out zero cofactors. A signed difference of two adjugate columns forces the determinant to divide two. Open full record →
A reusable Lean theorem reduces total unimodularity to divisibility by four for square submatrices with even row and column sums.	Lean	Preflight needed
formalization · Formalization 4 A reusable Lean theorem reduces total unimodularity to divisibility by four for square submatrices with even row and column sums. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-formalization-camion-criterion (“Camion's total-unimodularity criterion”) states a machine-checkable theorem or proof obligation. The record states: A reusable Lean theorem reduces total unimodularity to divisibility by four for square submatrices with even row and column sums. Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text 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) Details Lean selects a least bad minor, applies the checked minimal-obstruction theorem, and derives the Camion-Gomory parity certificate. Related:* Formalization 3 Open full record →
Lean proves that every Eulerian selected support is covered with odd multiplicity by finitely many contained support squares.	Lean	Preflight needed
formalization · Formalization 5 Lean proves that every Eulerian selected support is covered with odd multiplicity by finitely many contained support squares. Relevance to this problem This supplies the graph-theoretic core of Fibonacci support divisibility. Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text `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` Details The proof works with arbitrary even sub-supports. A maximal incident vertex exposes a Fibonacci support square containing at least three current edges. Toggling that square preserves every row and column parity and strictly reduces the edge count, so well-founded induction produces the odd square cover. The two-square incidence bound then turns the cover into a four-edge partition. Related: Formalization 2 Open full record →
The problem-specific Lean obligation says that every square Fibonacci-sum submatrix with even row and column sums contains a multiple of four ones.	Lean	Preflight needed
formalization · Formalization 6 The problem-specific Lean obligation says that every square Fibonacci-sum submatrix with even row and column sums contains a multiple of four ones. Relevance to this problem This checked bridge connects the graph-theoretic support theorem to Camion's integer matrix condition. Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text `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` Details The kernel-checked proof converts the matrix-entry sum to the finite support cardinality and applies the checked odd-square-cover theorem. Related: Formalization 5 Open full record →
The checked Lean reduction combines Camion's criterion with the Fibonacci-specific divisibility obligation.	Lean	Preflight needed
formalization · Formalization 7 The checked Lean reduction combines Camion's criterion with the Fibonacci-specific divisibility obligation. Relevance to this problem This strengthens the target to total unimodularity and connects its two proof obligations. Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text `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` Details The checked declaration combines the verified Camion reduction with the Fibonacci support divisibility theorem. Every source dependency now compiles in the pinned world. Related: Formalization 1 · Formalization 4 · Formalization 6 Open full record →
The exact public target now has a checked Lean proof from the total-unimodularity obligation.	Lean	Preflight needed
formalization · Formalization 8 The exact public target now has a checked Lean proof from the total-unimodularity obligation. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-formalization-determinant-range-lean-v1 (“Lean determinant-range reduction”) states a machine-checkable theorem or proof obligation. The record states: The exact public target now has a checked Lean proof from the total-unimodularity obligation. Evidence Preflight neededA Lean-shaped target draft is stored. Preflight has yet to confirm compilation in the pinned world. Record state draft Scope No narrower scope recorded Submitted target text unchecked text `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` Details The exact public theorem and every source dependency compile in the pinned world. The controlled worker attestation remains a separate evidence step. Related: Formalization 7 Open full record →
The source reports 10,800 allowed permutations at n=33 with an even split by sign.	Artifact	Evidence: Supported Backed by a cited source or by evidence short of a proof.
artifact · Artifact 1 The source reports 10,800 allowed permutations at n=33 with an even split by sign.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-permutations-33 (“Allowed-permutation parity count at n=33”) supplies evidence or a replay used to check the packet. The record states: The source reports 10,800 allowed permutations at n=33 with an even split by sign. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state reported Scope No narrower scope recorded Sources Reference 1 Details A repository reproduction of the permutation enumeration remains open. Related: Claim 2 Open full record →
A table records nonzero indices, their Zeckendorf bit strings, and successive gaps through n=1219.	Artifact	Evidence: Supported Backed by a cited source or by evidence short of a proof.
artifact · Artifact 2 A table records nonzero indices, their Zeckendorf bit strings, and successive gaps through n=1219.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-nonzero-table (“Nonzero determinant support and Zeckendorf table”) supplies evidence or a replay used to check the packet. The record states: A table records nonzero indices, their Zeckendorf bit strings, and successive gaps through n=1219. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state sourced Scope No narrower scope recorded Sources Reference 1 Details The table exposes primary, secondary, and tertiary gap families and their block replication. Related: Conjecture 2 · Conjecture 3 · Conjecture 4 · 1 more Open full record →
A MathOverflow image marks replicated, mirrored, and boundary-affected blocks in the support-gap sequence.	Artifact	Evidence: Supported Backed by a cited source or by evidence short of a proof.
artifact · Artifact 3 A MathOverflow image marks replicated, mirrored, and boundary-affected blocks in the support-gap sequence.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-self-similarity-image (“Colored block self-similarity diagram”) supplies evidence or a replay used to check the packet. The record states: A MathOverflow image marks replicated, mirrored, and boundary-affected blocks in the support-gap sequence. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state sourced Scope No narrower scope recorded Sources Reference 1 Details The image supplies a visual conjecture that still needs a symbolic encoding. Related: Claim 5 · Claim 6 Open full record →
Compute residual cores through n=500, retain exact index sets, and search for a recursive Zeckendorf map.	Artifact	Evidence: Conjectured Proposed as likely true. No argument is recorded.
artifact · Artifact 4 Compute residual cores through n=500, retain exact index sets, and search for a recursive Zeckendorf map. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-core-sweep-500 (“Planned core sweep through n=500”) supplies evidence or a replay used to check the packet. The record states: Compute residual cores through n=500, retain exact index sets, and search for a recursive Zeckendorf map. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state planned Scope No narrower scope recorded Details This artifact is specified and awaiting execution and structured export. Related: Route 5 Open full record →
A dependency-free Python program reconstructs M_n and verifies the determinant range through n=120 using exact arithmetic.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 5 A dependency-free Python program reconstructs M_n and verifies the determinant range through n=120 using exact arithmetic. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-det-check-120-scoped (“Exact Bareiss determinant sweep through n=120”) supplies evidence or a replay used to check the packet. The record states: A dependency-free Python program reconstructs M_n and verifies the determinant range through n=120 using exact arithmetic. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state reproduced Scope runs over every size from 1 to 120 Run `python3 research/fibonacci/checks.py --max-n 120` File research/fibonacci/checks.py Details Run python3 research/fibonacci/checks.py --max-n 120. Related: Computation 1 Open full record →
For the sequence 2,6,8,14,22,36,58, the 5 by 5 sum-indicator matrix has determinant 2.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 6 For the sequence 2,6,8,14,22,36,58, the 5 by 5 sum-indicator matrix has determinant 2. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-growth-counterexample-scoped (“Exact growth-rate counterexample at n=5”) supplies evidence or a replay used to check the packet. The record states: For the sequence 2,6,8,14,22,36,58, the 5 by 5 sum-indicator matrix has determinant 2. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state reproduced Scope the sequence 2,6,8,14,22,36,58 at n = 5 Details The executable check appears in research/fibonacci/checks.py. Related: Computation 3 Open full record →
The executable sweep reports a nonempty residual core for 110 of n=1 through 120.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 7 The executable sweep reports a nonempty residual core for 110 of n=1 through 120. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-singleton-sweep-scoped (“Singleton-peeling residual-core sweep”) supplies evidence or a replay used to check the packet. The record states: The executable sweep reports a nonempty residual core for 110 of n=1 through 120. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state reproduced Scope every size from 1 to 120 File research/fibonacci/checks.py Details Rows or columns with exactly one remaining 1 are removed together with the forced partner until no forced match remains. Related: Computation 4 Open full record →
The checker can emit the surviving row and column sets after forced peeling for each n.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 8 The checker can emit the surviving row and column sets after forced peeling for each n. Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-artifact-core-index-samples-scoped (“Residual-core index samples”) supplies evidence or a replay used to check the packet. The record states: The checker can emit the surviving row and column sets after forced peeling for each n. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope residual cores emitted for sizes 1 to 120 Details Persisting these samples through n=500 is the next data-collection step for inferring a Zeckendorf index map. Related: Claim 4 Open full record →
No records match these filters.

How the 48 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemDeterminants of the Fibonacci-sum matrix

2 records outside this overview

All 52 recorded relations between these records and the problem

2See also

Characterize the nonzero determinant indicessame packet

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Determinants of the Fibonacci-sum matrix.” TheoremDB. P2. Problem statement; statement text SHA-256 91312d1aa020718968fced2c0d3e2d44bb353b99505661afc56cb1c53398c700. https://theoremdb.org/statement/?ref=P2

BibTeX

@misc{theoremdb-problem-91312d1aa020718968fced2c0d3e2d44bb353b99505661afc56cb1c53398c700,
  title = {{Determinants of the Fibonacci-sum matrix}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 91312d1aa020718968fced2c0d3e2d44bb353b99505661afc56cb1c53398c700},
  url = {https://theoremdb.org/statement/?ref=P2}
}

Plain text: Built Markdown snapshot

This problem includes 48 records joined by 103 typed links, sourced from mathoverflow.net^[1], current as of July 26, 2026.

1Lean verification

What the formal work covers

Formal statement

Lean determinant-range reduction

Linked target: Determinants of the Fibonacci-sum matrix

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Supporting declarations and earlier submissions (7)

Formal statement

Lean definition of the Fibonacci-sum matrix

Linked target: Determinants of the Fibonacci-sum matrix

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Formal statement

Camion's total-unimodularity criterion

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Formal statement

Fibonacci support divisibility condition

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Formal statement

Almost-TU determinant and nonvanishing cofactors

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Formal statement

Fibonacci support four-cycle classification

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Formal statement

Fibonacci odd square cover

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Formal statement

Total unimodularity of the Fibonacci-sum matrix

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Proof dependencies and replay

Lean blueprint

The source contains no sorries under Lean 4.33.0-rc1 with mathlib 4608056c. Signed verification is pending.

Check pending

Legend

Theorems and lemmas

Definitions

Fully formalized

Proof formalized

Definition formalized

SORRY open

Statement formalized

Statement ready

Blueprint needs work

Reproduce the verification

Download source bundle Bundle checksum

Toolchain: leanprover/lean4:v4.33.0-rc1
Mathlib: 4608056c77c52468b80773e8dcd585ef821c7c5e
Source SHA-256: d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc
Worker command: lean -j 1 Deposit.lean
Axioms: Classical.choice, Quot.sound, propext
Signed by

Shell · explicit execution

tar -xzf theoremdb-lean-world-d575c4e2ff28.tar.gz
cd theoremdb-lean-world-d575c4e2ff28
lake exe cache get
lake build
lake env lean Reproduce.lean

No executables, scripts, or symlinks. Inspect the source before building it.

Theorem or lemma

fibSumMatrix_det_range

Lean determinant-range reduction

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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

Uses fibSumMatrix_totallyUnimodular

Theorem or lemma

fibSumMatrix_totallyUnimodular

Total unimodularity of the Fibonacci-sum matrix

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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

Uses fibSumMatrix, isTotallyUnimodular_of_camion, fibSumMatrix_camion_divisibility

Theorem or lemma

fibSumMatrix

Lean definition of the Fibonacci-sum matrix

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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

Theorem or lemma

fibSumMatrix_camion_divisibility

Fibonacci support divisibility condition

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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

Uses fibSubmatrixSupport_has_odd_square_cover

Theorem or lemma

isTotallyUnimodular_of_camion

Camion's total-unimodularity criterion

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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)

Uses minimal_bad_square_minor_det_and_adjugate_nonzero

Theorem or lemma

fibSubmatrixSupport_has_odd_square_cover

Fibonacci odd square cover

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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

Uses fibonacci_support_four_corner_classification

Theorem or lemma

minimal_bad_square_minor_det_and_adjugate_nonzero

Almost-TU determinant and nonvanishing cofactors

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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)⟩

Theorem or lemma

fibonacci_support_four_corner_classification

Fibonacci support four-cycle classification

Fully formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc

Lean 4 · read only

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

Uses fibSumMatrix

Finish Lean verification

A solution has been submitted and awaits independent review. Lean source is attached; signed verification is pending.

Continue in TheoremDB Researcher

Upload a Lean project archive

Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.

1References

Packet source. 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 lines 57-60. ↗forum · reference source · web version checked 2026-08-01 · checked 2026-07-26Source use: citation only.For fib problem determinant range; fib problem nonzero support: Supplies the problem statement, reported computations, discussion, and community observations recorded in the packet.Also cited at Question, answers, and comments cited by the individual research records.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.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.Source used to formulate or check the problem record.
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. ↗preprint · primary source · arXiv:1710.10303v1 · checked 2026-08-01Source 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.
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. ↗journal article · primary source · publisher version · checked 2026-08-01Source 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.

Discussion

Loading discussion.

[#P2] Determinants of the Fibonacci-sum matrix

1Context

2Remarks

1Status

1Packet records

Recent contributions

2See also

1Lean verification

What the formal work covers

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Reproduce the verification

fibSumMatrix_det_range

fibSumMatrix_totallyUnimodular

fibSumMatrix

fibSumMatrix_camion_divisibility

isTotallyUnimodular_of_camion

fibSubmatrixSupport_has_odd_square_cover

minimal_bad_square_minor_det_and_adjugate_nonzero

fibonacci_support_four_corner_classification

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Remarks

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

2See also

1Lean verification

What the formal work covers

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Formal statement

Reproduce the verification

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status