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\).
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.[3]
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
Argument
Allowed permutations satisfy that i+pi(i) is Fibonacci for every row i.
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}.[1][2]
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
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.
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.
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.
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.
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.
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.
At n=33 there are 10,800 allowed permutations, split into 5,400 even and 5,400 odd permutations.[3]
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
Details
This exhibits large cancellation that a determinant-only computation hides.
Powers of 2, powers of 3, and tribonacci numbers were reported to have the same determinant property in tested ranges.[3]
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
Details
These examples broaden the classification problem beyond Lucas recurrences.
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.
An observed row, including its primary gap, reappears as the middle block of the row four levels later.[3]
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
Details
This self-similarity could supply the recursive step in a support classification.
The first block of one row mirrors the final block of the previous row, and much of the middle block mirrors into the next final block.[3]
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
Details
The mirror rule has a boundary exception that needs its own description.
The repeated-block symmetry fails near boundaries where the initial support-difference sequence is copied into later rows.[3]
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
Details
Any induction on self-similar blocks must isolate this exception explicitly.
The MathOverflow author previously reported receiving claimed AI proofs without publishing their text.[3]
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
Details
This historical report remains separate from the recorded proof now preserved in fib-claim-total-unimodular-review-pending.
By Philip Weiss, Fabius Wiesner, Wolfgang, OpenAI Codex
Result
Supported
claim · Claim 8
Unresolved in this packet after the dated source check. Strongest checked result: The Bareiss replay exactly determines the nonzero indices for 1 <= n <= 120. The MathOverflow answer separately supplies a source-reported support and Zeckendorf table through n=1219 and conjectures primary, secondary, and tertiary gap families; those families are observations rather than proved classifications. Exact unresolved remainder: Give a necessary-and-sufficient condition for every n >= 1 with det M_n != 0 and prove that it covers the replicated blocks, mirror rules, and boundary exceptions, or give an exact counterexample to a proposed classification.[1][2][3]
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
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.
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.
Open
Reported
claim · Conjecture 1
Initial tests suggested the Fibonacci construction extends to Lucas sequences, including Lucas and Pell numbers.[3]
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
Details
Later examples show that recurrence growth alone cannot characterize the valid sequences.
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.[3]
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
Details
This is an observed formula for the support sequence rather than a proved classification.
A shifted family appears between F_k+F_{k-5}+F_{k-8}-1 and F_k+F_{k-4}+F_{k-9}.[3]
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
Details
The gap sizes repeat the primary sequence with a shift.
A third observed family runs from F_k+F_{k-4}+F_{k-7}-1 to F_k+F_{k-4}+F_{k-6}, with sizes 3,4,6,9,14,22 and onward.[3]
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
Details
The three gap families suggest a recursive language for nonzero indices.
Describe all n for which det M_n is nonzero and explain why those indices cluster above Fibonacci numbers.[3]
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
Details
A solution may be weaker than a proof of the full determinant conjecture while still exposing its recursive structure.
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.
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.
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.
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.
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.
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.
Determine which increasing integer sequences make every finite sum-indicator matrix totally unimodular.[3]
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
What happened
Positive examples include several recurrence and exponential sequences. The determinant-2 recurrence example rules out a growth-only answer.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
The source reports 10,800 allowed permutations at n=33 with an even split by sign.[3]
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
Details
A repository reproduction of the permutation enumeration remains open.
A table records nonzero indices, their Zeckendorf bit strings, and successive gaps through n=1219.[3]
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
Details
The table exposes primary, secondary, and tertiary gap families and their block replication.
A MathOverflow image marks replicated, mirrored, and boundary-affected blocks in the support-gap sequence.[3]
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
Details
The image supplies a visual conjecture that still needs a symbolic encoding.
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.
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
Details
Run python3 research/fibonacci/checks.py --max-n 120.
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.
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
Details
Rows or columns with exactly one remaining 1 are removed together with the forced partner until no forced match remains.
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.