Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Giacomelli’s cone of infinitely log-concave initial data

Abstract

Two positive geometric solutions have infinitely log-concave initial data, but their midpoint has a negative first log-concavity determinant.

Definition 1.1 (The recurrent sequence).

Formalization. D5/S0/Certificates/GiacomelliLogConcaveConeNonconvex.seq (✓ std3).

Citation. P. Giacomelli (2026). Log-Concavity and Infinite Log-Concavity of Linear Recurrent Sequences with Linear Coefficients via Companion Matrix Methods. DOI: 10.48550/arXiv.2604.14391. URL: https://arxiv.org/abs/2604.14391v1.

Commentary.

Equation (3), printed page 2: a_{n+1} = Σ_{k=0}^{d−1} (p_k n + q_k) a_{n−k}, n ≥ d − 1, with p_k, q_k ∈ ℝ and initial data (a_0, …, a_{d−1}) ∈ ℝ^d. The argument m is n + 1, and the entries of v0 are in increasing index order. Subtraction in natural indices is truncated. The cast to Real follows subtraction.

Definition 1.2 (The log-concave operator).

Formalization. D5/S0/Certificates/GiacomelliLogConcaveConeNonconvex.logConcaveOp (✓ std3).

Citation. P. Giacomelli (2026). Log-Concavity and Infinite Log-Concavity of Linear Recurrent Sequences with Linear Coefficients via Companion Matrix Methods. DOI: 10.48550/arXiv.2604.14391. URL: https://arxiv.org/abs/2604.14391v1.

Commentary.

Definition 2.1, printed page 3: “Let (aₖ)ₖ∈ℕ be a sequence of real numbers. The log-concave operator L is defined by L(aₖ) = (bₖ), bₖ = aₖ² − aₖ₊₁aₖ₋₁. The sequence (aₖ) is log-concave if bₖ ≥ 0 for all k. For i ≥ 1, (aₖ) is i-fold log-concave if Lⁱ(aₖ) ≥ 0, and ∞-log-concave if Lⁱ(aₖ) ≥ 0 for all i ∈ ℕ.” The function argument a has domain Nat; k − 1 uses natural subtraction.

Definition 1.3 (Infinitely log-concave initial data).

Formalization. D5/S0/Certificates/GiacomelliLogConcaveConeNonconvex.coneInf (✓ std3).

Citation. P. Giacomelli (2026). Log-Concavity and Infinite Log-Concavity of Linear Recurrent Sequences with Linear Coefficients via Companion Matrix Methods. DOI: 10.48550/arXiv.2604.14391. URL: https://arxiv.org/abs/2604.14391v1.

Commentary.

Section 7 (1), printed page 13, defines “C∞ = {v₀ : Lⁱ(aₙ) ≥ 0 ∀ n, i}”. The function seq is the sequence generated by v0. Iteration is function iteration on Nat → Real, and i ≤ n restricts evaluation to interior indices. Iteration zero includes nonnegativity of the original sequence.

Definition 1.4 (The affirmative convexity assertion).

Formalization. D5/S0/Certificates/GiacomelliLogConcaveConeNonconvex.claim (✓ std3).

Citation. P. Giacomelli (2026). Log-Concavity and Infinite Log-Concavity of Linear Recurrent Sequences with Linear Coefficients via Companion Matrix Methods. DOI: 10.48550/arXiv.2604.14391. URL: https://arxiv.org/abs/2604.14391v1.

Commentary.

Section 7 (1), printed page 13: “(Cone of initial data for variable coefficients.) Proposition 3.4 gives a matrix condition on v₀ for log-concavity of a general P-recursive sequence. Characterize the geometry of the cone C∞ = {v₀ : Lⁱ(aₙ) ≥ 0 ∀ n, i} for d ≥ 3. Is it convex? Simply connected?” The affirmative convexity assertion ranges over every natural d ≥ 3 and every pair p, q of real coefficient vectors. Convex is Mathlib’s real convexity predicate.

Theorem 1.5 (The cone need not be convex).

Proof. Machine-checked in Lean as D5/S0/Certificates/GiacomelliLogConcaveConeNonconvex.result (✓ std3). ∎

Resolves. Problems/giacomelli-2026-log-concave-cone-convexity-question (refuted) by D5/S0/Certificates/GiacomelliLogConcaveConeNonconvex.result.

Source. Repository-derived.

Acknowledgement. P. Giacomelli (2026). Log-Concavity and Infinite Log-Concavity of Linear Recurrent Sequences with Linear Coefficients via Companion Matrix Methods. DOI: 10.48550/arXiv.2604.14391. URL: https://arxiv.org/abs/2604.14391v1.

Commentary.

Take d = 3, p = (1, −3, 2), q = (3, −2, 0). Strong induction shows that U = (1, 1, 1) and V = (1, 2, 4) generate 1 and 2ⁿ. Induction on the iterate shows that each positive iterate is zero whenever 1 ≤ i ≤ n. Both sequences are nonnegative, so U and V belong to coneInf p q. Their midpoint is (1, 3/2, 5/2). At index 1 its first determinant is (3/2)² − (5/2)·1 = −1/4. This contradicts convexity. Characterization and simple connectedness are separate questions.

References