Label Occurrences in Restricted-Growth Words

Abstract

Restricted-growth words give Mathar’s two closed label-occurrence counts.

Words are lists of natural labels stored in reverse chronological order. The first generated label is 1, and each next label lies from 1 through one more than the maximum already present. T(n,p) sums the number of occurrences of label p over all words of length n.

All arithmetic in the two closed forms is natural-number arithmetic. Subtraction is truncated natural subtraction. Each slash denotes the natural-number quotient, not rational division or a displayed fraction.

Definition 1.1 (Largest label).

$$\begin{array}{r}maxLabel:\mathrm{List}(\mathbb{N})\to \mathbb{N}\\ \forall w\in \mathrm{List}(\mathbb{N}),\mathrm{maxLabel}(w)=\mathrm{foldr}(max,0,w)\end{array}$$

Formalization. D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.maxLabel (✓ std3).

Citation. R. J. Mathar (2016). OEIS A270236, Triangle T(n,p): occurrences of p in the restricted growth functions of length n. URL: https://oeis.org/A270236.

Commentary.

Folding maximum from zero returns the largest label, with value zero on the empty word.

Definition 1.2 (Restricted-growth words).

$$\begin{array}{r}words:\mathbb{N}\to \mathrm{Finset}(\mathrm{List}(\mathbb{N}))\\ \mathrm{words}(0)=\{[]\}\\ \forall n\in \mathbb{N},\mathrm{words}(n+1)=\mathrm{biUnion}(\mathrm{words}(n),\lambda w,\mathrm{image}(\mathrm{Icc}(1,\mathrm{maxLabel}(w)+1),\lambda x,\mathrm{cons}(x,w)))\end{array}$$

Formalization. D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.words (✓ std3).

Citation. R. J. Mathar (2016). OEIS A270236, Triangle T(n,p): occurrences of p in the restricted growth functions of length n. URL: https://oeis.org/A270236.

Commentary.

This reverse-chronological generator starts from the empty word. Each step prepends every label in the inclusive interval from 1 to one above the previous maximum. Its membership is identified with the source predicate by mem_words_iff.

Definition 1.3 (Chronological restricted-growth predicate).

$$\begin{array}{r}IsRestrictedGrowth:\mathrm{List}(\mathbb{N})\to Prop\\ \forall f\in \mathrm{List}(\mathbb{N}),\mathrm{IsRestrictedGrowth}(f)\iff (f=[]\vee (\mathrm{head}(f)=1\wedge \forall j\in \mathbb{N},j<\left|f\right|\Rightarrow (1\le f_j\wedge f_j\le 1+\mathrm{foldr}(max,0,\mathrm{take}(j,f)))))\end{array}$$

Formalization. D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.IsRestrictedGrowth (✓ std3).

Citation. R. J. Mathar (2016). OEIS A270236, Triangle T(n,p): occurrences of p in the restricted growth functions of length n. URL: https://oeis.org/A270236.

Commentary.

The empty list is admitted. A nonempty chronological list begins with 1, and every indexed label is positive and at most one plus the maximum of the preceding prefix.

Theorem 1.4 (Generator membership equals the source predicate).

$$\forall n\in \mathbb{N},\forall w\in \mathrm{List}(\mathbb{N}),w\in \mathrm{words}(n)\iff (\left|w\right|=n\wedge \mathrm{IsRestrictedGrowth}(\mathrm{reverse}(w)))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mem_words_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

A word belongs to the reverse-chronological generator at length n exactly when it has length n and its chronological reversal satisfies the restricted-growth predicate.

Definition 1.5 (Total label occurrences).

$$\begin{array}{r}T:\mathbb{N}\to \mathbb{N}\to \mathbb{N}\\ \forall n\in \mathbb{N},\forall p\in \mathbb{N},T(n,p)=\sum _{w\in \mathrm{words}(n)}\mathrm{count}(w,p)\end{array}$$

Formalization. D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.T (✓ std3).

Citation. R. J. Mathar (2016). OEIS A270236, Triangle T(n,p): occurrences of p in the restricted growth functions of length n. URL: https://oeis.org/A270236.

Commentary.

For every length and label, this definition sums List.count over the finite set of restricted-growth words.

Theorem 1.6 (The penultimate-label formula).

$$\forall n\in \mathbb{N},1<n⟹T(n,n-1)=2+n\cdot (n-1)/2$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mathar_f1 (✓ std3). ∎

Resolves. Problems/oeis-a270236-rgf-penultimate-label-count (proved) by D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mathar_f1.

Citation. R. J. Mathar (2016). OEIS A270236, Triangle T(n,p): occurrences of p in the restricted growth functions of length n. URL: https://oeis.org/A270236.

Commentary.

The all-distinct word and the one-repeat maximum layer give one base occurrence, one occurrence for each chosen repeat pair, and one extra occurrence when the repeated label is the penultimate label.

Theorem 1.7 (The antepenultimate-label formula).

$$\forall n\in \mathbb{N},1<n⟹T(n+1,n-1)=2+n\cdot \left(n+1\right)\cdot (3\cdot n^2-5\cdot n+26)/24$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mathar_f2 (✓ std3). ∎

Resolves. Problems/oeis-a270236-rgf-antepenultimate-label-count (proved) by D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mathar_f2.

Citation. R. J. Mathar (2016). OEIS A270236, Triangle T(n,p): occurrences of p in the restricted growth functions of length n. URL: https://oeis.org/A270236.

Commentary.

The label-extension sum separates the top three maximum layers. The two-repeat layer consists of one triple block or two paired blocks; the resulting binomial expression normalizes to the quotient by 24.

References

• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.IsRestrictedGrowth
• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.T
• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mathar_f1
• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mathar_f2
• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.maxLabel
• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.mem_words_iff
• Truth anchor: D5/S1/Recurrence/Invariants/RestrictedGrowthLabelOccurrences.words