GreedyRenewal

Abstract

Shortest borders, maximal block-palindrome width, and exact renewal counts.

Definition 1.1 (IsBPFactorization).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (bs:\mathrm{List}(\mathrm{List}alpha)),\forall (c:\mathrm{List}alpha),\mathrm{IsBPFactorization}wbsc⟺(\forall b\in bs,b\ne [])\wedge w=bs.\mathrm{reverse}.\mathrm{flatten}++c++bs.\mathrm{flatten}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.IsBPFactorization (✓ 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. 2): “Let w be a non-empty word. A block palindrome factorization (or BP-factorization) of w is a factorization w = wₘ⋯w₁w₀w₁⋯wₘ of a word such that w₀ is a possibly empty word, and every other factor wᵢ is non-empty for all i with 1 ≤ i ≤ m.” Here bs is [w₁,…,wₘ] and c is w₀. The empty word has width zero.

Definition 1.2 (bpWidth).

$$\forall (alpha:\mathrm{Type}),\forall (bs:\mathrm{List}(\mathrm{List}alpha)),\forall (c:\mathrm{List}alpha),\mathrm{bpWidth}bsc=2\cdot bs.\mathrm{length}+\mathrm{if}c=[]\mathrm{then}0\mathrm{else}1$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.bpWidth (✓ 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. 2): “We say that a BP-factorization wₘ⋯w₁w₀w₁⋯wₘ is of width t where t = 2m+1 if w₀ is non-empty and t = 2m otherwise.” Here m is bs.length and c is w₀.

Definition 1.3 (largestBPWidth).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\mathrm{largestBPWidth}w=\mathrm{sSup}\{t:\mathbb{N}\mid \exists (bs:\mathrm{List}(\mathrm{List}alpha))(c:\mathrm{List}alpha),\mathrm{IsBPFactorization}wbsc\wedge \mathrm{bpWidth}bsc=t\}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.largestBPWidth (✓ 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. 2): “The largest BP-factorization of a word w is a BP-factorization w = wₘ⋯w₁w₀w₁⋯wₘ where m is maximized (i.e., where the width of the BP-factorization is maximized).” The supremum is over all valid widths and is bounded by w.length.

Theorem 1.4 (largestBPWidth_le_length).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\mathrm{largestBPWidth}w\le w.\mathrm{length}$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.5 (IsBorder).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (b:\mathrm{List}alpha),\mathrm{IsBorder}wb⟺b\ne []\wedge b.\mathrm{length}<w.\mathrm{length}\wedge \mathrm{List}.\mathrm{IsPrefix}bw\wedge \mathrm{List}.\mathrm{IsSuffix}bw$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.IsBorder (✓ 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. 1): “A border of a word w is a non-empty word that is both a proper prefix and suffix of w.” Properness is expressed by b.length < w.length.

Definition 1.6 (IsUnbordered).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\mathrm{IsUnbordered}w⟺\forall (b:\mathrm{List}alpha),\neg \mathrm{IsBorder}wb$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.IsUnbordered (✓ 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. 1): “A word is said to be bordered if it has a border. Otherwise, the word is said to be unbordered.”

Definition 1.7 (IsShortestBorder).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (b:\mathrm{List}alpha),\mathrm{IsShortestBorder}wb⟺\mathrm{IsBorder}wb\wedge \forall (c:\mathrm{List}alpha),\mathrm{IsBorder}wc\Rightarrow b.\mathrm{length}\le c.\mathrm{length}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.IsShortestBorder (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of IsShortestBorder.

Theorem 1.8 (shortest_border_unbordered).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (b:\mathrm{List}alpha),(\mathrm{IsShortestBorder}wb)\Rightarrow (\mathrm{IsUnbordered}b)$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.9 (shortest_border_le_half).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (b:\mathrm{List}alpha),(\mathrm{IsShortestBorder}wb)\Rightarrow (2\cdot b.\mathrm{length}\le w.\mathrm{length})$$

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

Source. Repository-derived.

Commentary.

An overlapping border would produce a shorter nonempty border, so a shortest border occupies at most half of its word.

Theorem 1.10 (unbordered_outer_shortest).

$$\forall (alpha:\mathrm{Type}),\forall (u:\mathrm{List}alpha),\forall (v:\mathrm{List}alpha),(u\ne [])\Rightarrow ((\mathrm{IsUnbordered}u)\Rightarrow (\mathrm{IsShortestBorder}(u++v++u)u))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.11 (maximal_outer_unbordered).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (c:\mathrm{List}alpha),\forall (b:\mathrm{List}alpha),\forall (bs:\mathrm{List}(\mathrm{List}alpha)),(\mathrm{IsBPFactorization}w(bs++[b])c)\Rightarrow ((\mathrm{bpWidth}(bs++[b])c=\mathrm{largestBPWidth}w)\Rightarrow (\mathrm{IsUnbordered}b))$$

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

Source. Repository-derived.

Commentary.

A bordered outer block splits into matching nonempty outer blocks. This increases the width and contradicts maximality.

Definition 1.12 (shortestBorder).

$$\forall (alpha:\mathrm{Type})(w:\mathrm{List}alpha)(hw:\exists b:\mathrm{List}alpha,\mathrm{IsBorder}wb)(chooseProof:\exists b:\mathrm{List}alpha,\mathrm{IsShortestBorder}wb),\mathrm{shortestBorder}whw=\mathrm{Classical}.\mathrm{choose}chooseProof$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.shortestBorder (✓ std3).

Source. Repository-derived.

Commentary.

Classical.choose selects a shortest border. The displayed choice proof has the exact existential type; proof irrelevance makes the chosen value independent of which proof of that existential is supplied.

Theorem 1.13 (shortestBorder_spec).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (hw:\exists (b:\mathrm{List}alpha),\mathrm{IsBorder}wb),\mathrm{IsShortestBorder}w(\mathrm{shortestBorder}whw)$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.14 (peeledCore).

$$\forall (alpha:\mathrm{Type})(w:\mathrm{List}alpha)(hw:\exists b:\mathrm{List}alpha,\mathrm{IsBorder}wb)(chooseProof:\exists v:\mathrm{List}alpha,w=\mathrm{shortestBorder}whw++v++\mathrm{shortestBorder}whw\wedge v.\mathrm{length}=w.\mathrm{length}-2\cdot (\mathrm{shortestBorder}whw).\mathrm{length}),\mathrm{peeledCore}whw=\mathrm{Classical}.\mathrm{choose}chooseProof$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.peeledCore (✓ std3).

Source. Repository-derived.

Commentary.

Classical.choose selects the central word between the shortest matching outer borders. The existential contains both the concatenation identity and its exact length. Proof irrelevance makes the choice independent of the proof supplied.

Theorem 1.15 (peeledCore_spec).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (hw:\exists (b:\mathrm{List}alpha),\mathrm{IsBorder}wb),w=\mathrm{shortestBorder}whw++\mathrm{peeledCore}whw++\mathrm{shortestBorder}whw\wedge (\mathrm{peeledCore}whw).\mathrm{length}=w.\mathrm{length}-2\cdot (\mathrm{shortestBorder}whw).\mathrm{length}$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.16 (peeledCore_shorter).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\forall (hw:\exists (b:\mathrm{List}alpha),\mathrm{IsBorder}wb),(\mathrm{peeledCore}whw).\mathrm{length}<w.\mathrm{length}$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.17 (peelWidth).

$$\forall (alpha:\mathrm{Type})(w:\mathrm{List}alpha),\mathrm{peelWidth}w=\mathrm{if}hw:\exists (b:\mathrm{List}alpha),\mathrm{IsBorder}wb\mathrm{then}2+\mathrm{peelWidth}(\mathrm{peeledCore}whw)\mathrm{else}\mathrm{if}w=[]\mathrm{then}0\mathrm{else}1$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.peelWidth (✓ std3).

Source. Repository-derived.

Commentary.

The recursion removes the shortest border pair until the remaining word is empty or unbordered. Every removal increases the width by two.

Theorem 1.18 (largest_eq_peelWidth).

$$\forall (alpha:\mathrm{Type}),\forall (w:\mathrm{List}alpha),\mathrm{largestBPWidth}w=\mathrm{peelWidth}w$$

Proof. Machine-checked in Lean as D5/S1/Words/BlockPalindromes/GreedyRenewal.largest_eq_peelWidth (✓ 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.

Induction on word length shows that greedy shortest-border peeling realizes the largest factorization width.

Theorem 1.19 (mem_words).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (w:\mathrm{List}(\mathrm{Fin}k)),w\in (\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))⟺w.\mathrm{length}=n$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.20 (card_words).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),((\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))).\mathrm{card}=k^n$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.21 (ubWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{ubWords}kn=((\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))).\mathrm{filter}\mathrm{IsUnbordered}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.ubWords (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of ubWords.

Definition 1.22 (uCount).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{uCount}kn=(\mathrm{ubWords}kn).\mathrm{card}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.uCount (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of uCount.

Theorem 1.23 (mem_ubWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (w:\mathrm{List}(\mathrm{Fin}k)),w\in \mathrm{ubWords}kn⟺w.\mathrm{length}=n\wedge \mathrm{IsUnbordered}w$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.24 (outerWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (i:\mathbb{N}),\mathrm{outerWords}kni=((\mathrm{ubWords}ki)\times ((\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}(n-2\cdot i):\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k))))).\mathrm{image}(\mathrm{fun}p\mapsto p.1++p.2++p.1)$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.outerWords (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of outerWords.

Theorem 1.25 (mem_outerWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (i:\mathbb{N}),\forall (w:\mathrm{List}(\mathrm{Fin}k)),w\in \mathrm{outerWords}kni⟺\exists (uv:\mathrm{List}(\mathrm{Fin}k)),u.\mathrm{length}=i\wedge \mathrm{IsUnbordered}u\wedge v.\mathrm{length}=n-2\cdot i\wedge w=u++v++u$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.26 (outerWords_disjoint).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (i:\mathbb{N}),\forall (j:\mathbb{N}),(0<i)\Rightarrow ((0<j)\Rightarrow ((i\ne j)\Rightarrow (\mathrm{Disjoint}(\mathrm{outerWords}kni)(\mathrm{outerWords}knj))))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.27 (borderedWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{borderedWords}kn=((\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))).\mathrm{filter}(\mathrm{fun}w\mapsto \neg \mathrm{IsUnbordered}w)$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.borderedWords (✓ std3).

Source. Repository-derived.

Commentary.

The fixed-length words that have a nonempty proper border.

Theorem 1.28 (shortest_partition).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{borderedWords}kn=(\mathrm{Finset}.\mathrm{Icc}1((\mathrm{Nat}.\mathrm{div}n2))).\mathrm{biUnion}(\mathrm{outerWords}kn)$$

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

Source. Repository-derived.

Commentary.

Every bordered word has one shortest border length. Unbordered words and these outer-block families partition the words of fixed length. Nat.div is division in the natural numbers, rounded down.

Definition 1.29 (q).

$$\forall (k:\mathbb{N}),\forall (u:\mathbb{N}\to \mathbb{N}),qku=\sum _{j:\mathbb{N}}^{\prime }(u(j+1):\mathbb{R})/(k:\mathbb{R}{)}^{2\cdot (j+1)}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.q (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of q.

Theorem 1.30 (unbordered_q_lt_one).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (qk(\mathrm{uCount}k)<1)$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.31 (peelPairs).

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

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.peelPairs (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of peelPairs.

Theorem 1.32 (core_of_unbordered_outer).

$$\forall (alpha:\mathrm{Type}),\forall (u:\mathrm{List}alpha),\forall (v:\mathrm{List}alpha),(u\ne [])\Rightarrow ((\mathrm{IsUnbordered}u)\Rightarrow (\forall (hw:\exists (b:\mathrm{List}alpha),\mathrm{IsBorder}(u++v++u)b),\mathrm{peeledCore}(u++v++u)hw=v))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.33 (tailWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (r:\mathbb{N}),\mathrm{tailWords}knr=((\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))).\mathrm{filter}(\mathrm{fun}w\mapsto r\le \mathrm{peelPairs}w)$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.tailWords (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of tailWords.

Theorem 1.34 (mem_tailWords).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (r:\mathbb{N}),\forall (w:\mathrm{List}(\mathrm{Fin}k)),w\in \mathrm{tailWords}knr⟺w.\mathrm{length}=n\wedge r\le \mathrm{peelPairs}w$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.35 (renewal_tail_count).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\forall (r:\mathbb{N}),(\mathrm{tailWords}kn(r+1)).\mathrm{card}=\sum _{i\in \mathrm{Finset}.\mathrm{Icc}1((\mathrm{Nat}.\mathrm{div}n2))}\mathrm{uCount}ki\cdot (\mathrm{tailWords}k(n-2\cdot i)r).\mathrm{card}$$

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

Source. Repository-derived.

Commentary.

A word with at least r+1 peeled pairs has one shortest unbordered outer block and a centre with at least r peeled pairs. Different shortest lengths give disjoint families. Nat.div is division in the natural numbers, rounded down.

Theorem 1.36 (tailWords_zero).

$$\forall (k:\mathbb{N}),\forall (n:\mathbb{N}),\mathrm{tailWords}kn0=(\mathrm{DepthBudgetIidGreedyOptimality}.\mathrm{words}n:\mathrm{Finset}(\mathrm{List}(\mathrm{Fin}k)))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Definition 1.37 (qCoeff).

$$\forall (k:\mathbb{N}),\forall (i:\mathbb{N}),\mathrm{qCoeff}ki=\mathrm{if}i=0\mathrm{then}0\mathrm{else}(\mathrm{uCount}ki:\mathbb{R})/(k:\mathbb{R}{)}^{2\cdot i}$$

Formalization. D5/S1/Words/BlockPalindromes/GreedyRenewal.qCoeff (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of qCoeff.

Theorem 1.38 (qCoeff_nonneg).

$$\forall (k:\mathbb{N}),\forall (i:\mathbb{N}),0\le \mathrm{qCoeff}ki$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.39 (qCoeff_summable).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\mathrm{Summable}(\mathrm{qCoeff}k))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.40 (tsum_qCoeff).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow ((\sum _{i:\mathbb{N}}^{\prime }\mathrm{qCoeff}ki)=qk(\mathrm{uCount}k))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.41 (q_nonneg).

$$\forall (k:\mathbb{N}),0\le qk(\mathrm{uCount}k)$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments.

Theorem 1.42 (qCoeff_recurrence).

$$\forall (k:\mathbb{N}),(2\le k)\Rightarrow (\forall (n:\mathbb{N}),(0<n)\Rightarrow (\mathrm{qCoeff}kn=(1-\sum _{i\in \mathrm{Finset}.\mathrm{Icc}1((\mathrm{Nat}.\mathrm{div}n2))}\mathrm{qCoeff}ki)/(k:\mathbb{R}{)}^n))$$

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

Source. Repository-derived.

Commentary.

The displayed statement holds for all of its quantified arguments. Nat.div is division in the natural numbers, rounded down.

References

• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.IsBPFactorization
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.IsBorder
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.IsShortestBorder
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.IsUnbordered
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.borderedWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.bpWidth
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.card_words
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.core_of_unbordered_outer
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.largestBPWidth
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.largestBPWidth_le_length
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.largest_eq_peelWidth
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.maximal_outer_unbordered
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.mem_outerWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.mem_tailWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.mem_ubWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.mem_words
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.outerWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.outerWords_disjoint
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.peelPairs
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.peelWidth
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.peeledCore
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.peeledCore_shorter
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.peeledCore_spec
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.q
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.qCoeff
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.qCoeff_nonneg
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.qCoeff_recurrence
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.qCoeff_summable
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.q_nonneg
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.renewal_tail_count
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.shortestBorder
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.shortestBorder_spec
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.shortest_border_le_half
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.shortest_border_unbordered
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.shortest_partition
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.tailWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.tailWords_zero
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.tsum_qCoeff
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.uCount
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.ubWords
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.unbordered_outer_shortest
• Truth anchor: D5/S1/Words/BlockPalindromes/GreedyRenewal.unbordered_q_lt_one
• Dependency: D5/S0/Computability/Coding/DepthBudgetIidGreedyOptimality