LargestFactorizationExpectedWidth

Abstract

The expected largest block-palindrome width converges to the A274199 series.

Definition 1.1 (tailProbability).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (r:\mathbb{N}),\mathrm{tailProbability}knr=((\mathrm{tailWords}knr).\mathrm{card}:\mathbb{R})/(k:\mathbb{R}{)}^n$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.tailProbability (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of tailProbability.

Theorem 1.2 (renewal_tail_limit).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\forall (r:\mathbb{N}),\mathrm{Tendsto}(\mathrm{fun}(n:\mathbb{N})\mapsto \mathrm{tailProbability}knr)\mathrm{atTop}(\mathrm{nhds}((qk(\mathrm{uCount}k){)}^r)))$$

Proof. Machine-checked in Lean as D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.renewal_tail_limit (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact renewal recursion, summability of its coefficients, and dominated convergence give the r-th power of the unbordered-word mass as the limit.

Definition 1.3 (peelCentre).

$$\forall (alpha:\mathrm{Type})(w:\mathrm{List}alpha),\mathrm{peelCentre}w=\mathrm{if}hw:\exists (b:\mathrm{List}alpha),\mathrm{IsBorder}wb\mathrm{then}\mathrm{peelCentre}(\mathrm{peeledCore}whw)\mathrm{else}w$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.peelCentre (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of peelCentre.

Definition 1.4 (emptyWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{emptyWords}kn=((\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))).\mathrm{filter}(\mathrm{fun}w\mapsto \mathrm{peelCentre}w=[])$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.emptyWords (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of emptyWords.

Definition 1.5 (emptyProbability).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{emptyProbability}kn=((\mathrm{emptyWords}kn).\mathrm{card}:\mathbb{R})/(k:\mathbb{R}{)}^n$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.emptyProbability (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of emptyProbability.

Definition 1.6 (QSeries).

$$\forall (k:\mathbb{N}),\mathrm{QSeries}k=\mathrm{PowerSeries}.\mathrm{mk}(\mathrm{qCoeff}k)$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.QSeries (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of QSeries.

Definition 1.7 (ESeries).

$$\forall (k:\mathbb{N}),\mathrm{ESeries}k=\mathrm{PowerSeries}.\mathrm{mk}(\mathrm{fun}(m:\mathbb{N})\mapsto \mathrm{emptyProbability}k(2\cdot m))$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.ESeries (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of ESeries.

Theorem 1.8 (empty_centre_powerSeries).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\mathrm{ESeries}k=(1-\mathrm{QSeries}k{)}^{-1})$$

Proof. Machine-checked in Lean as D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.empty_centre_powerSeries (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coefficient of degree m is the empty-centre probability at length 2m. Its convolution recursion gives the inverse of one minus the renewal series.

Definition 1.9 (expectedWidth).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{expectedWidth}kn=\frac{{\sum }_{w:\mathrm{Fin}n\to \mathrm{Fin}k}(\mathrm{largestBPWidth}(\mathrm{List}.\mathrm{ofFn}w):\mathbb{R})}{(k:\mathbb{R}{)}^n}$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.expectedWidth (✓ std3).

Citation. D. Gabrić and J. Shallit (2023). Smallest and Largest Block Palindrome Factorizations. DOI: 10.1007/978-3-031-33180-0_14. URL: https://arxiv.org/abs/2302.13147.

Commentary.

The source states (arXiv v2, p. 5): “From the definition of expected value, it follows that Eₙ,ₖ = (1/kⁿ)∑ᵢ₌₁ⁿ i·LBPₖ(n,i).” The cardinality counts length-n words whose largest BP-factorization has width i; the empty word has width zero.

Theorem 1.10 (expectedWidth_limit).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\mathrm{Tendsto}(\mathrm{expectedWidth}k)\mathrm{atTop}(\mathrm{nhds}(2/(1-qk(\mathrm{uCount}k))-1)))$$

Proof. Machine-checked in Lean as D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.expectedWidth_limit (✓ std3). ∎

Source. Repository-derived.

Commentary.

The width equals twice the number of peeled pairs plus the indicator of a nonempty centre. Geometric domination of the tails and vanishing empty-centre probability give the stated limit.

Definition 1.11 (claim).

$$\mathrm{claim}⟺\forall (k:\mathbb{N}),2\le k\Rightarrow \exists (a:\mathbb{N}\to \mathbb{R}),(\forall d,\mathrm{Tendsto}(\mathrm{fun}(N:\mathbb{N})\mapsto (a274190N(N-d):\mathbb{R}))\mathrm{atTop}(\mathrm{nhds}(ad)))\wedge \mathrm{Summable}(\mathrm{fun}(i:\mathbb{N})\mapsto 2\cdot a(i+1)/(k:\mathbb{R}{)}^{i+1})\wedge \mathrm{Tendsto}(\mathrm{fun}n\mapsto \mathrm{expectedWidth}kn)\mathrm{atTop}(\mathrm{nhds}(1+\sum _{i:\mathbb{N}}^{\prime }2\cdot a(i+1)/(k:\mathbb{R}{)}^{i+1}))$$

Formalization. D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.claim (✓ std3).

Citation. D. Gabrić and J. Shallit (2023). Smallest and Largest Block Palindrome Factorizations. DOI: 10.1007/978-3-031-33180-0_14. URL: https://arxiv.org/abs/2302.13147.

Commentary.

Conjecture 5 (arXiv v2, §3, p. 5): “Let k ≥ 2. Then E_k = 1+∑{i=1}^∞ a_i k^{-i} where the sequence (a_n/2){n≥1} is A274199 in the On-Line Encyclopedia of Integer Sequences (OEIS).” A274199(d) is the stabilized diagonal a274190 (2*d) d. The positive index is i+1, so the source expansion starts with coefficients 2,4,6,10.

Theorem 1.12 (result).

$$\mathrm{claim}$$

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

Resolves. Problems/gabric-shallit-2023-block-palindrome-expected-width (proved) by D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.result.

Source. Repository-derived.

Acknowledgement. D. Gabrić and J. Shallit (2023). Smallest and Largest Block Palindrome Factorizations. DOI: 10.1007/978-3-031-33180-0_14. URL: https://arxiv.org/abs/2302.13147.

Commentary.

For every alphabet size k≥2, every reverse-row coefficient converges, the positively indexed coefficient series is summable, and the expected largest width converges to one plus that series. The proof uses the exact renewal recursion and does not use the source Lemma 3.

References

• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.ESeries
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.QSeries
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.claim
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.emptyProbability
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.emptyWords
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.empty_centre_powerSeries
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.expectedWidth
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.expectedWidth_limit
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.peelCentre
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.renewal_tail_limit
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.result
• Truth anchor: D5/S1/Words/BlockPalindromes/LargestFactorizationExpectedWidth.tailProbability
• Dependency: D5/S1/Words/BlockPalindromes/CompositionInversion