Alternative q-Charlier Fibonacci Positivity

Abstract

Alternative q-Charlier Fibonacci positivity at rho = q = 1/4.

Definition 1.1 (The first tridiagonal determinant).

$\forall x \in N a t \to R e a l, y \in N a t \to R e a l, n \in N a t, A (x, y, n) = Matrix . det (Matrix . of ((f u n (i : F in (n)) \mapsto (f u n (j : F in (n)) \mapsto (i f ((i : N a t) = (j : N a t)) t h e n x ((i : N a t) + 1) e l se (i f ((j : N a t) = (i : N a t) + 1) t h e n y ((i : N a t) + 1) e l se (i f ((i : N a t) = (j : N a t) + 1) t h e n 1 e l se 0)))))))$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.A (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

Define two sequences of tridiagonal determinants as follows: (arXiv:2412.21126v2, p. 15, equation (2.10)). A is the determinant with diagonal x at indices 1 through ell, upper diagonal y and lower diagonal one. The displayed Matrix.of gives every entry, including zero outside these three diagonals. The empty determinant is one.

Definition 1.2 (The second tridiagonal determinant).

$\forall x \in N a t \to R e a l, y \in N a t \to R e a l, n \in N a t, B (x, y, n) = Matrix . det (Matrix . of ((f u n (i : F in (n + 1)) \mapsto (f u n (j : F in (n + 1)) \mapsto (i f (((i : N a t) = 0) \land ((j : N a t) = 0)) t h e n y (1) e l se (i f (((i : N a t) = 0) \land ((j : N a t) = 1)) t h e n x (1) \cdot y (2) e l se (i f ((i : N a t) = (j : N a t)) t h e n x ((i : N a t) + 2) e l se (i f ((j : N a t) = (i : N a t) + 1) t h e n y ((i : N a t) + 2) e l se (i f ((i : N a t) = (j : N a t) + 1) t h e n 1 e l se 0)))))))))$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.B (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

Define two sequences of tridiagonal determinants as follows: (arXiv:2412.21126v2, p. 15, equation (2.10)). B k has size k+1; its first row starts with y 1 and x 1 times y 2. The remaining diagonal starts at x 3, its upper diagonal at y 3, and its lower diagonal is one.

Definition 1.3 (Recursion with leading ones).

$\forall x \in N a t \to R e a l, y \in N a t \to R e a l, k \in N a t, s A ux (x, y, k, List . nil) = A (x, y, k) \forall x \in N a t \to R e a l, y \in N a t \to R e a l, k \in N a t, w \in L i s t (N a t), s A ux (x, y, k, List . cons (1, w)) = s A ux (x, y, k + 1, w) \forall x \in N a t \to R e a l, y \in N a t \to R e a l, k \in N a t, a \in N a t, u \in L i s t (N a t), (a \neq = 1) \Rightarrow (s A ux (x, y, k, List . cons (a, u)) = B ((f u n (j : N a t) \mapsto x (j + List . sum (u))), (f u n (j : N a t) \mapsto y (j + List . sum (u))), k) \cdot s A ux (x, y, 0, u))$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.sAux (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

For any Fibonacci word w, define the (biserial) clone Schur function s_w(x⃗ | y⃗) through the following recurrence: s_w(x⃗ | y⃗) := A_k(x⃗ | y⃗), if w = 1^k for some k ≥ 0; B_k(x⃗ + |u| | y⃗ + |u|) · s_u(x⃗ | y⃗), if w = 1^k2u for some k ≥ 0. (Definition 2.5, p. 15). The auxiliary recursion counts k initial letters one. At an empty tail it returns A k; a letter one increases k; every other letter contributes B k with sequences shifted by the sum of the remaining letters, followed by the recursion at zero. Only letters one and two occur in Fibonacci words.

Definition 1.4 (Biserial clone Schur functions).

$\forall x \in N a t \to R e a l, y \in N a t \to R e a l, w \in L i s t (N a t), s (x, y, w) = s A ux (x, y, 0, w)$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.s (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

For any Fibonacci word w, define the (biserial) clone Schur function s_w(x⃗ | y⃗) through the following recurrence: s_w(x⃗ | y⃗) := A_k(x⃗ | y⃗), if w = 1^k for some k ≥ 0; B_k(x⃗ + |u| | y⃗ + |u|) · s_u(x⃗ | y⃗), if w = 1^k2u for some k ≥ 0. (Definition 2.5, p. 15). Fibonacci words are lists over {1, 2}; the weight |u| is List.sum u. The function s starts sAux with zero initial letters one.

Definition 1.5 (Fibonacci positivity).

$\forall x \in N a t \to R e a l, y \in N a t \to R e a l, (F ib o na cc i P os i t i v e (x, y)) \Leftrightarrow ((\forall w \in L i s t (N a t), (\forall a \in N a t, (a \in w) \Rightarrow ((a = 1) \lor (a = 2))) \Rightarrow (0 < s (x, y, w))))$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.FibonacciPositive (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

If s_w(x⃗ | y⃗) > 0 for all w ∈ 𝕐𝔽, we say that (x⃗, y⃗) is Fibonacci positive. (Definition 4.1, p. 21). The real sequences are indexed from one. The implication restricts the list to letters one and two, and includes the empty word.

Definition 1.6 (The alternative q-Charlier x sequence).

$\forall r h o \in R e a l, q \in R e a l, k \in N a t, x A QC (r h o, q, k) = \frac{q ^{(k : I n t) - 1} \cdot ( 1 + r h o \cdot q ^{(k : I n t) - 2} + r h o \cdot q ^{(k : I n t) - 1} - r h o \cdot q ^{2 \cdot (k : I n t) - 2} )}{( 1 + r h o \cdot q ^{2 \cdot (k : I n t) - 3} ) \cdot ( 1 + r h o \cdot q ^{2 \cdot (k : I n t) - 1} )}$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.xAQC (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

There exist values of ρ and q for which the following specialization (which we call the alternative q-Charlier) is Fibonacci positive: (Conjecture 6.3, p. 31). This is its printed x expression. The sequence is used for k ≥ 1; its extension at zero is immaterial. Each exponent is an integer, so the negative exponents at k=1 are retained.

Definition 1.7 (The alternative q-Charlier y sequence).

$\forall r h o \in R e a l, q \in R e a l, k \in N a t, y A QC (r h o, q, k) = \frac{r h o \cdot q ^{3 \cdot (k : I n t) - 2} \cdot ( 1 - q ^{(k : I n t)} ) \cdot ( 1 + r h o \cdot q ^{(k : I n t) - 1} )}{( 1 + r h o \cdot q ^{2 \cdot (k : I n t)} ) \cdot ( 1 + r h o \cdot q ^{2 \cdot (k : I n t) - 1} ) ^{2} \cdot ( 1 + r h o \cdot q ^{2 \cdot (k : I n t) - 2} )}$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.yAQC (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

There exist values of ρ and q for which the following specialization (which we call the alternative q-Charlier) is Fibonacci positive: (Conjecture 6.3, p. 31). This is its printed y expression, used for k ≥ 1. The casts from natural k to Int and every denominator factor are displayed.

Definition 1.8 (Petrov–Scott Conjecture 6.3).

$(c l aim) \Leftrightarrow ((\exists r h o \in R e a l, q \in R e a l, F ib o na cc i P os i t i v e (x A QC (r h o, q), y A QC (r h o, q))))$

Formalization. D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.claim (✓ std3).

Citation. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

There exist values of ρ and q for which the following specialization (which we call the alternative q-Charlier) is Fibonacci positive: (Conjecture 6.3, p. 31). The specialization is xAQC and yAQC above. Both existential parameters range over Real, and positivity quantifies over every Fibonacci word.

Theorem 1.9 (Positive determinant from diagonal dominance).

$\forall (ι : T y p e), [F in t y p e (ι)] [Dec i d ab l e Eq (ι)] \forall M \in M a t r i x (ι, ι, R e a l), (\forall i \in ι, 0 < M (i, i)) \Rightarrow ((\forall i \in ι, Finset . sum (Finset . erase (Finset . univ, i), (f u n (j : ι) \mapsto ∥ M (i, j) ∥)) < M (i, i)) \Rightarrow (0 < Matrix . det (M)))$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.det_pos_of_dominant (✓ std3). ∎

Source. Repository-derived.

Commentary.

A real matrix with positive diagonal entries and strict row diagonal dominance has positive determinant.

Theorem 1.10 (Positivity at rho = q = one quarter).

$\exists r h o \in R e a l, q \in R e a l, F ib o na cc i P os i t i v e (x A QC (r h o, q), y A QC (r h o, q))$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.result (✓ std3). ∎

Resolves. Problems/petrov-scott-2026-alternative-q-charlier-fibonacci-positivity-conjecture-6-3 (proved) by D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.result.

Source. Repository-derived.

Acknowledgement. Leonid Petrov and Jeanne Scott (2026). Random Fibonacci words via clone Schur functions. DOI: 10.1017/fms.2025.10165. URL: https://arxiv.org/abs/2412.21126v2.

Commentary.

Take rho=q=1/4. A positive diagonal rescaling turns the tridiagonal determinants into strictly diagonally dominant matrices. The normalized sequence is nonnegative, at most 1/4, positive at positive indices, and, from index one onward, contracts by a factor at most 1/2. A continuous deformation to the diagonal matrix preserves nonsingularity and hence the positive determinant sign. Induction on the list then proves positivity for every Fibonacci word, with no bound on its weight.

References

Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.A
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.B
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.FibonacciPositive
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.claim
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.det_pos_of_dominant
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.result
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.s
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.sAux
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.xAQC
Truth anchor: D5/S3/Combinatorics/YoungFibonacci/PetrovScottAltQCharlierPositivity.yAQC

Keyboard shortcuts

trureturing — Discovering truth

Alternative q-Charlier Fibonacci Positivity

Abstract

References