Maximum Number of Scattered Palindromes

Abstract

The sharp maximum of distinct scattered palindromes and its alphabet sizes.

Words are List A, and List.Sublist is scattered containment. Finite sets remove duplicate embeddings. The empty subword is excluded. Nat.div is integer division, so Nat.div (n+1) 2 represents ⌈n/2⌉. Every subtraction is truncated natural subtraction.

Definition 1.1 (Distinct nonempty palindromic subsequences).

$$\forall A\in Type,[\mathrm{DecidableEq}\left(A\right)],\forall w\in \mathrm{List}\left(A\right),\mathrm{spal}\left(w\right)=\mathrm{Finset}.filter\left(fun(u:\mathrm{List}\left(A\right))\mapsto u\ne []\wedge \mathrm{List}.reverse\left(u\right)=u,\mathrm{List}.toFinset\left(\mathrm{List}.sublists\left(w\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.spal (✓ std3).

Citation. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Section 2, page 2: “We denote by PAL(w) and SPAL(w), the set of all non-empty palindromic factors, and scattered palindromic subwords of w, respectively.” List.sublists enumerates scattered subwords; List.toFinset counts each word once. A palindrome satisfies List.reverse u = u.

Definition 1.2 (Number of scattered palindromes).

$$\forall A\in Type,[\mathrm{DecidableEq}\left(A\right)],\forall w\in \mathrm{List}\left(A\right),\mathrm{sp}\left(w\right)=\mathrm{Finset}.card\left(\mathrm{spal}\left(w\right)\right)$$

Formalization. D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.sp (✓ std3).

Citation. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Section 2, page 2: “Also, P(w)=|PAL(w)| and SP(w)=|SPAL(w)|.” Page 3: “Throughout the paper, by the number of palindromic factors (resp. scattered palindromic subwords), we mean the number of non-empty distinct palindromic factors (resp. scattered palindromic subwords) in a word.”

Definition 1.3 (Number of distinct letters).

$$\forall A\in Type,[\mathrm{DecidableEq}\left(A\right)],\forall w\in \mathrm{List}\left(A\right),\mathrm{alphabetSize}\left(w\right)=\mathrm{Finset}.card\left(\mathrm{List}.toFinset\left(w\right)\right)$$

Formalization. D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.alphabetSize (✓ std3).

Citation. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Section 2, page 2: “Alph(w) denotes the set of all the subwords of w of length 1.” List.toFinset contains exactly the letters that occur in w, so its cardinality is the source’s q.

Definition 1.4 (The proposed sharp maximum).

$$\forall n\in Nat,\mathrm{maxSP}\left(n\right)=if\mathrm{Nat}.mod\left(n,2\right)=1then3\cdot 2^{\mathrm{Nat}.div\left(n+1,2\right)-1}-2else(2^{\mathrm{Nat}.div\left(n,2\right)+1}-2)$$

Formalization. D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.maxSP (✓ std3).

Citation. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Conjecture 5.6, page 18:

“The maximum number of scattered palindromic subwords in a word of length n is

3(2^{⌈n/2⌉−1})−2, if n is odd,

2^{n/2+1}−2, if n is even.

and this bound is achieved only when

q =

⌈n/2⌉, if n is odd

n/2 and n/2+1, if n is even.”

The two printed cases are encoded literally with natural integer division.

Definition 1.5 (The extremal alphabet sizes).

$$\forall n\in Nat,\forall q\in Nat,\mathrm{permittedQ}\left(n,q\right)\iff if\mathrm{Nat}.mod\left(n,2\right)=1thenq=\mathrm{Nat}.div\left(n+1,2\right)else(q=\mathrm{Nat}.div\left(n,2\right)\vee q=\mathrm{Nat}.div\left(n,2\right)+1)$$

Formalization. D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.permittedQ (✓ std3).

Citation. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Conjecture 5.6, page 18:

“The maximum number of scattered palindromic subwords in a word of length n is

3(2^{⌈n/2⌉−1})−2, if n is odd,

2^{n/2+1}−2, if n is even.

and this bound is achieved only when

q =

⌈n/2⌉, if n is odd

n/2 and n/2+1, if n is even.”

The even case is a disjunction between two alphabet sizes.

Definition 1.6 (Conjecture 5.6).

$$\mathrm{claim}\left(\right)\iff \left(\left(\forall A\in Type,[\mathrm{DecidableEq}\left(A\right)],\forall w\in \mathrm{List}\left(A\right),\mathrm{sp}\left(w\right)\le \mathrm{maxSP}\left(\mathrm{List}.length\left(w\right)\right)\right)\wedge \left(\left(\forall n\in Nat,\forall q\in Nat,1\le n\Rightarrow \left(\mathrm{permittedQ}\left(n,q\right)\Rightarrow \left(\exists w\in \mathrm{List}\left(Nat\right),\mathrm{List}.length\left(w\right)=n\wedge \left(\mathrm{alphabetSize}\left(w\right)=q\wedge \mathrm{sp}\left(w\right)=\mathrm{maxSP}\left(n\right)\right)\right)\right)\right)\wedge \left(\forall A\in Type,[\mathrm{DecidableEq}\left(A\right)],\forall w\in \mathrm{List}\left(A\right),1\le \mathrm{List}.length\left(w\right)\Rightarrow \left(\mathrm{sp}\left(w\right)=\mathrm{maxSP}\left(\mathrm{List}.length\left(w\right)\right)\Rightarrow \mathrm{permittedQ}\left(\mathrm{List}.length\left(w\right),\mathrm{alphabetSize}\left(w\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.claim (✓ std3).

Citation. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Conjecture 5.6, page 18:

“The maximum number of scattered palindromic subwords in a word of length n is

3(2^{⌈n/2⌉−1})−2, if n is odd,

2^{n/2+1}−2, if n is even.

and this bound is achieved only when

q =

⌈n/2⌉, if n is odd

n/2 and n/2+1, if n is even.”

The encoding states a universal upper bound, attainment for every positive length and every permitted alphabet size, and necessity for every extremal nonempty word. Natural-number letters suffice for attainment; the bound and necessity quantify over every decidable alphabet.

Theorem 1.7 (The conjecture holds).

$$\mathrm{claim}\left(\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.result (✓ std3). ∎

Resolves. Problems/mahalingam-pandoh-2021-scattered-palindrome-maximum (proved) by D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.result.

Source. Repository-derived.

Acknowledgement. K. Mahalingam, P. Pandoh (2021). Counting scattered palindromes in a finite word. URL: https://arxiv.org/abs/2108.02729v1.

Commentary.

Partition by the outer letter. A letter occurring once contributes one palindrome; a repeated letter contributes two plus the number of palindromes between its first and last occurrences. The convex endpoint matching estimate and the recurrence maxSP(n+2)=2 maxSP(n)+2 yield a residue bound by strong induction. Equality forces the residual length k to satisfy maxSP(k)=k and hence k≤2, and forces all repeated letters to occur exactly twice. For each permitted q, start with k distinct letters, where k is zero, one or two, and add r fresh matching outer pairs. The resulting word has length 2r+k, alphabet size r+k and count maxSP(2r+k). This constructs extremizers and restricts their alphabet sizes; it does not classify all extremal words or determine the maximum at every fixed alphabet size below half the length.

References

• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.alphabetSize
• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.claim
• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.maxSP
• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.permittedQ
• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.result
• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.sp
• Truth anchor: D5/S1/Words/Palindromes/ScatteredPalindromeMaximum.spal
• Dependency: D5/S1/Words/Palindromes/ScatteredPalindromeMatching