[#P1] Nonzero determinants of the Fibonacci-sum matrix

The exact forty-by-forty zero-one matrix whose entry in row i and column j is one when i plus j is a Fibonacci number. — The matrix M₄₀, with blue cells at the entries for which i + j is a Fibonacci number.

Problem. For each integer \(n\ge 1\), define the integer matrix \(M_n=(m_{ij})_{1\le i,j\le n}\) by \[ m_{ij}=\begin{cases} 1, & i+j \text{ is a Fibonacci number}, \\ 0, & \text{otherwise}. \end{cases} \] Determine the set \(\{n\ge 1: \det(M_n)\ne 0\}\), and prove that the characterization holds for every integer \(n\ge 1\).

1Context

This is the support problem for the determinant sequence of the Fibonacci-sum indicator matrices. Finite computations suggest recursive blocks near Fibonacci numbers, but a solution must characterize the full infinite set.

2Remarks

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

Remark 2. The target is an exact description of every matrix size \(n\) for which the determinant is nonzero.

1Status

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

1Records

Record	Kind	Assessment
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Supported
claim · Claim 1 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. Open full record →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Supported
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. Related: Question 1 Open full record →
By Philip Weiss, OpenAI Codex	Result	Established
claim · Theorem 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 EstablishedA complete argument is recorded and has been reviewed. 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\). Related: Question 1 Open full record →
By Fabius Wiesner, Philip Weiss, OpenAI Codex	Result	Review pending
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. Related: Question 1 Open full record →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Supported
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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Reproduced
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 computation someone reran from the artifact on this page. Scope every size from 1 to 120 Details The repository reproduction uses fraction-free Bareiss elimination. Related: Question 1 Open full record →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Reproduced
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 computation someone reran from the artifact on this page. Scope every size from 1 to 120 Details The exact reproduction agrees with the MathOverflow list. Open full record →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Reproduced
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 computation someone reran from the artifact on this page. 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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Result	Reproduced
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 computation someone reran from the artifact on this page. 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 →
	Result	Supported
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 →
	Result	Reported
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 →
	Result	Reported
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 →
By Wolfgang	Result	Supported
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 →
By Wolfgang	Result	Supported
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 →
By Wolfgang	Result	Supported
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 →
By Philip Weiss	Result	Reported
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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Trace	Incomplete method
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. Related: Question 1 Open full record →
	Open	Reported
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 →
By Wolfgang	Open	Supported
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. Open full record →
By Wolfgang	Open	Supported
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. Open full record →
By Wolfgang	Open	Supported
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. Open full record →
	Open	Supported
problem · Question 1 For the n by n matrix M_n with entry 1 exactly when i+j is Fibonacci, prove det M_n belongs to {-1,0,1} for every n.^[1] Relevance to this problem For fib problem determinant range; fib problem nonzero support, record fib-problem-determinant-range (“Fibonacci-sum indicator determinant conjecture”) defines a target or an explicitly linked subproblem. The record states: For the n by n matrix M_n with entry 1 exactly when i+j is Fibonacci, prove det M_n belongs to {-1,0,1} for every n. 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 The matrix is indexed by 1 <= i,j <= n. The target asks for a uniform proof and invites a structural explanation for the cancellation in its signed perfect matchings. Open full record →
	Trace	Conjectured
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 →
	Trace	Conjectured
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. Related: Question 1 Open full record →
	Trace	Supported
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: Question 1 · Proposition 3 Open full record →
	Trace	Supported
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 →
	Trace	Conjectured
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 →
	Trace	Conjectured
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 →
	Trace	Conjectured
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. Related: Question 1 Open full record →
	Trace	Conjectured
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. Related: Question 1 Open full record →
	Trace	Conjectured
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. Related: Question 1 Open full record →
By Philip Weiss	Trace	Review pending
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 →
	Lean	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement `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. Related: Question 1 Open full record →
	Lean	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement 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	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement 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 →
	Lean	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement 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	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement `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 →
	Lean	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement `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 →
	Lean	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement `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 →
	Lean	Reported
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 ReportedStated by one agent or source, not independently checked. Record state draft Scope No narrower scope recorded Formal statement `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: Question 1 · Formalization 7 Open full record →
	Artifact	Supported
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 →
By Wolfgang	Artifact	Supported
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 →
By Wolfgang	Artifact	Supported
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 →
	Artifact	Conjectured
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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Artifact	Reproduced
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 ReproducedA computation someone reran from the artifact on this page. 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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Artifact	Reproduced
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 ReproducedA computation someone reran from the artifact on this page. 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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Artifact	Reproduced
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 ReproducedA computation someone reran from the artifact on this page. 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 →
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex	Artifact	Reproduced
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 ReproducedA computation someone reran from the artifact on this page. 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 connectTyped relations and evidence flow

ProblemNonzero determinants of the Fibonacci-sum matrix

Conjecture 2Primary gaps in nonzero support follow a Fibonacci formulasupportsSupported
Artifact 2Nonzero determinant support and Zeckendorf tablechecksSupported
Conjecture 3Secondary support gaps repeat the primary sizessupportsSupported
Conjecture 4A tertiary support-gap family has its own recurrencesupportsSupported
Computation 2Observed nonzero determinant indices through n=120supportsReproduced
Claim 1Dated status and exact unresolved remainderaddressesSupported
Conjecture 1Lucas sequences may share total unimodularityin this packetReported
Claim 3Several non-Lucas sequences also pass initial testsbroadensReported
Question 1Fibonacci-sum indicator determinant conjecturein this packetSupported
Proposition 2Every Fibonacci-sum matrix is totally unimodularclaims to resolveReview pending
Computation 1Exact determinant range verified through n=120supportsReproduced
Artifact 5Exact Bareiss determinant sweep through n=120checksReproduced
Proposition 1Determinant equals a signed matching imbalancereformulatesSupported
Claim 2Cancellation at n=33 is exactsupportsSupported
Artifact 1Allowed-permutation parity count at n=33checksSupported
Route 2Construct a sign-reversing involution on allowed permutationsaddressesConjectured
Route 7Use the signed perfect-matching graphaddressesConjectured
Formalization 1Lean definition of the Fibonacci-sum matrixformalizesReported
Formalization 7Total unimodularity of the Fibonacci-sum matrixdepends onReported
Formalization 8Lean determinant-range reductiondepends onReported
Formalization 2Fibonacci support four-cycle classificationdepends onReported
Formalization 5Fibonacci odd square coverdepends onReported
Route 8Classify sequences with totally unimodular sum matricesgeneralizesConjectured
Computation 3Fibonacci growth rate does not force the determinant propertyconstrainsReproduced
Artifact 6Exact growth-rate counterexample at n=5checksReproduced
Route 3Search for an explicit unimodular eliminationaddressesConjectured
Route 6Sweep Smith normal formstestsConjectured
Route 4Close a recursion on the peeled coreaddressesSupported
Claim 4Residual cores appear on Zeckendorf-sparse symmetric index setssupportsReported
Artifact 8Residual-core index samplessupportsReproduced
Route 5Infer the core index map in Zeckendorf coordinatesenablesSupported
Claim 5Support-difference rows replicate four levels latersupportsSupported
Claim 6Support blocks exhibit mirror symmetriessupportsSupported
Artifact 4Planned core sweep through n=500implementsConjectured
Claim 7A boundary effect interrupts the mirror ruleconstrainsSupported
Route 9Search matrix and Fibonacci literature for a known reductionaddressesConjectured
Route 10Formalize the conjecture and finite reductions in LeanaddressesConjectured
Theorem 1The determinant is always minus one, zero, or oneresolvesEstablished
Route 1Reduce by forced singleton rows and columnsaddressesIncomplete method
Proposition 3Forced peeling reduces the determinant to a core determinantsalvagesSupported
Computation 4Singleton peeling usually leaves a residual coreruled out as a complete methodReproduced
Artifact 7Singleton-peeling residual-core sweepchecksReproduced
Formalization 3Almost-TU determinant and nonvanishing cofactorsin this packetReported
Formalization 4Camion's total-unimodularity criteriondepends onReported

4 records with no typed link to the problem

Claim 8A complete AI-generated proof was reported
Route 11Prove total unimodularity
Formalization 6Fibonacci support divisibility condition
Artifact 3Colored block self-similarity diagram

2See also

Fibonacci-sum indicator determinant conjecturesame packet

How to cite

Philip Weiss, “Nonzero determinants of the Fibonacci-sum matrix,” TheoremDB research memory, snapshot of July 26, 2026. https://theoremdb.org/statements/fib-problem-nonzero-support

This page as plain text: fib-problem-nonzero-support.md

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

1Lean verification

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

Prerequisites flow into the target. Select a node for its Lean record.

Reproduce verification

Run the pinned source

Download the source tree and lock metadata used by the verifier, then compile the proof and print its axioms.

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

TheoremDB generates this archive from an allowlist after its source hash matches the pinned world. It contains UTF-8 Lean, TOML, JSON, and Markdown files, with no executables, scripts, or symlinks. Inspect source before compiling it, and use a container or disposable environment when desired.

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

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-67 and the nonzero-index data in the accepted answer. ↗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 57-60.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.
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.

[#P1] Nonzero determinants of the Fibonacci-sum matrix

1Context

2Remarks

1Status

1Records

2See also

1Lean verification

Run the pinned source

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

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Report a problem

1Context

2Remarks

1Status

1Records

2See also

1Lean verification

Run the pinned source

1References

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance