CompositionInversion

Abstract

Stable A274190 diagonals and inversion of the unbordered-word series.

Definition 1.1 (a274190).

$$(\forall (n:\mathbb{N}),a274190n0=1)\wedge (\forall (m:\mathbb{N}),a2741900(m+1)=0)\wedge (\forall (nm:\mathbb{N}),a274190(n+1)(m+1)=\mathrm{if}m+1\le n+1\mathrm{then}a274190nm+a274190n(2\cdot (m+1))\mathrm{else}0)$$

Formalization. D5/S1/Words/BlockPalindromes/CompositionInversion.a274190 (✓ 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 recurrence is the A274190 triangle, with row zero and column zero included. Its reverse diagonal stabilizes to A274199.

Theorem 1.2 (a274190_stable).

$$\forall Nd:\mathbb{N},2\cdot d\le N\Rightarrow a274190N(N-d)=a274190(2\cdot d)d$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.3 (a274190_diagonal_limit).

$$\forall (d:\mathbb{N}),\mathrm{Tendsto}(\mathrm{fun}N:\mathbb{N}\mapsto (a274190N(N-d):\mathbb{R}))\mathrm{atTop}(\mathrm{nhds}(a274190(2\cdot d)d:\mathbb{R}))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.4 (compCount).

$$(\forall (b:\mathbb{N}),\mathrm{compCount}0b=1)\wedge (\forall (nb:\mathbb{N}),\mathrm{compCount}(n+1)b=\sum _{i\in \mathrm{Finset}.\mathrm{range}(n+1)}\mathrm{if}i+1\le b\mathrm{then}\mathrm{compCount}(n-i)(2\cdot i+1)\mathrm{else}0)$$

Formalization. D5/S1/Words/BlockPalindromes/CompositionInversion.compCount (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of compCount.

Theorem 1.5 (a274190_compCount).

$$\forall Nm:\mathbb{N},m\le N\Rightarrow a274190Nm=\mathrm{compCount}(N-m)(m+1)$$

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

Source. Repository-derived.

Commentary.

The recurrence of the reverse triangle is the first-part recurrence for compositions whose next part is less than twice its predecessor.

Theorem 1.6 (a274190_stable_compCount).

$$\forall (d:\mathbb{N}),a274190(2\cdot d)d=\mathrm{compCount}dd$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.7 (compCount_fib_bound).

$$\forall nb:\mathbb{N},\mathrm{compCount}nb\le \mathrm{Nat}.\mathrm{fib}(n+1)$$

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

Source. Repository-derived.

Commentary.

The restricted composition count is at most Nat.fib(n+1). The bound gives absolute convergence at every reciprocal integer alphabet size k≥2.

Theorem 1.8 (composition_series_summable).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\mathrm{Summable}(\mathrm{fun}d:\mathbb{N}\mapsto (\mathrm{compCount}dd:\mathbb{R})/(k:\mathbb{R}{)}^d))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.9 (compTerm).

$$\forall (k:\mathbb{N}),\forall (b:\mathbb{N}),\forall (d:\mathbb{N}),\mathrm{compTerm}kbd=(\mathrm{compCount}db:\mathbb{R})/(k:\mathbb{R}{)}^d$$

Formalization. D5/S1/Words/BlockPalindromes/CompositionInversion.compTerm (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of compTerm.

Definition 1.10 (totalSeries).

$$\forall (k:\mathbb{N}),\mathrm{totalSeries}k=\sum _{d:\mathbb{N}}^{\prime }\mathrm{compTerm}kdd$$

Formalization. D5/S1/Words/BlockPalindromes/CompositionInversion.totalSeries (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of totalSeries.

Theorem 1.11 (unbordered_composition_series).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\mathrm{totalSeries}k=1/(1-qk(\mathrm{uCount}k)))$$

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

Source. Repository-derived.

Commentary.

Pairing the two regions j<2i and 2i≤j cancels their signed convolution contributions. The remaining identity relates the unbordered-word series to the full restricted-composition series.

References

• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.a274190
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.a274190_compCount
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.a274190_diagonal_limit
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.a274190_stable
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.a274190_stable_compCount
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.compCount
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.compCount_fib_bound
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.compTerm
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.composition_series_summable
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.totalSeries
• Truth anchor: D5/S1/Words/BlockPalindromes/CompositionInversion.unbordered_composition_series
• Dependency: D5/S1/Words/BlockPalindromes/GreedyRenewal