Costa–Catarino bidimensional Fibonacci matrices

Costa and Catarino, On Matrices with Bidimensional Fibonacci Numbers, Annales Mathematicae Silesianae 40(1), 59–76 (2026), DOI 10.2478/amsil-2025-0014, state an unnumbered conjecture at the end of §4 (p. 73): every order-two bidimensional Fibonacci matrix has nonzero determinant for all nonnegative indices. The source definitions are Definition 2.1 (p. 63), Lemma 2.5 (p. 64), and Definition 3.1 (p. 67). Preregistration and the verbatim statement are in issue #22448.

Statement echo

The Lean declaration D5.S1.Recurrence.CostaCatarinoBidimensionalFibonacci.claim keeps the source recurrences with guards $2 \le m$ and $2 \le n$, all four complex corner values, and the matrix with both negative entries. The definition sourceClosedForm separately retains the literal closed form. The claim adds an existence conjunct so the universal determinant assertion cannot be vacuous, and quantifies over every source sequence, every $m$, and every $n$; axes and the diagonal are included.

The conjecture concerns the determinant of the matrices generated by the two-coordinate Fibonacci recurrence. Establishing it closes the named open problem and gives a kernel-verified result for the source's full natural-index scope.

Issue #22448 recorded the conjecture as open before this settlement. The literature screen checked the DOI source, citation metadata, related matrix/Fibonacci searches, and arXiv/Zenodo queries; no published settlement of this exact statement was found in that checked scope. Literature completeness remains ASSUMED-UNVERIFIED. The source's printed Proposition 4.6 axis formula is inconsistent with Definition 3.1 and Example 4.1 at $(1,0)$; the settlement follows Definition 3.1 and does not use that formula.

The closed form sourceClosedForm satisfies both guarded recurrences and the four corner conditions. A two-stage order-two recurrence uniqueness argument identifies every source sequence with it. Expanding the determinant and taking its imaginary coordinate reduces the problem to a signed sum of consecutive Fibonacci products. The frozen Cassini/Vajda identity gives the sign relation, while positivity and strict monotonicity of the products rule out cancellation. The resulting theorem is D5.S1.Recurrence.CostaCatarinoBidimensionalFibonacci.result.

A counterexample would be a natural pair $(m,n)$ and a source sequence satisfying the four corners and both recurrences whose matrix determinant is zero. The delivered theorem rules out every such pair in the stated source scope. Generalized recurrence parameters, other corner data, and negative-index extensions are outside this claim.

• Settling declaration: D5.S1.Recurrence.CostaCatarinoBidimensionalFibonacci.result.
• Direct frozen dependency: D5/S1/Recurrence/FibVajda, declaration D5.S1.Recurrence.FibVajda.fib_vajda, declaration statement_id sha256:68cf09f524d730d13c876dd486737247ac0bf595476fa92c2f5a9e5b5b080e65.

Exact-integer experiment

Experiment directory at commit 9293e94c58b78241797dc11821b3070715a2be31. The immutable check.py has SHA-256 278f475f07e25174bb860dfe2ee6675bad457c81c01c1ac35e70047b97569328. Command: python3 /tmp/op-cc2025/experiment-check.py (the exact pinned script extracted with git show); exit code 0. It checks 10,609 sequence values, all 10,000 matrix pairs with $0 \le m,n < 100$, including 199 axis pairs, and 100 diagonal determinants. The minimum observed $|\operatorname{Im}\det M(m,n)|$ is $1$. All four fidelity examples are reproduced. At $(1,0)$ the printed Proposition 4.6 formula gives $-7-2i$, while Definition 3.1 and Example 4.1 give $-7+i$. These are finite exact computations; no uniform conclusion follows from the experiment alone.

Escape audit remains unfinished at #22505; no declared_validated claim is made without the required CI reading.

theorem; resolution proved; admission basis open-problem-resolution (#22448; Proved); generality: I; utility: none.

What the settlement shows

• Proved (kernel-checked): the recursively specified two-coordinate source exists and is unique, with closed form sourceClosedForm; the private declarations closed_form_is_source and source_unique supply existence and uniqueness, and result supplies existence together with universal nonsingularity.
• Proved (kernel-checked): $\operatorname{Im}(\det M(m,n)) \ne 0$ for every natural pair, by the private declaration determinant_im_ne_zero for sourceClosedForm, with source_unique identifying every source sequence. The private declarations signed_identity, t_pos and t_strictMono supply the signed Cassini identity, positivity and strict increase. This is the mathematical mechanism; it is not a qualifying §3.2 escape witness for the bind-only proof.
• Proved (kernel-checked): both axes and the diagonal are specializations of result, whose natural indices are unrestricted; the printed Proposition 4.6 determinant formula is not used.
• Computed: the exact-integer experiment above checks 10,609 sequence values and 10,000 matrix pairs with $0 \le m,n < 100$, including 199 axis pairs; its minimum observed absolute imaginary part is $1$. It reproduces all four fidelity examples and the printed axis-formula discrepancy. The experiment entry gives the command, exit code, immutable source and script SHA-256.
• Open: other recurrence parameters, other corner data, and negative-index extensions are outside this binding claim; no formal generalization is delivered.

The result node carries the typed OpenProblemResolutionClaim(Proved) for this dossier. The source note records the bounded literature screen with completeness ASSUMED-UNVERIFIED.

The literature/arXiv completeness screen is ASSUMED-UNVERIFIED: the checked citation indexes, related searches, and arXiv/Zenodo queries do not establish exhaustive worldwide absence or priority. The escape audit is unfinished because a faithful registration of the result’s existence-and-universality conjunction is missing; the template gap and required CI current DTR-Unregistered readings are recorded in #22505.