Choosable Initial Intervals

Abstract

Distinct representatives of increasing initial intervals exist exactly above the diagonal.

OEIS A388711 compares partitions with choosable initial intervals and superdiagonal reversed partitions. Ordinary parts are sorted decreasingly; reversed parts are sorted increasingly. Indices below start at zero, so the diagonal condition contains i+1. All parts and representatives are naturals.

Definition 1.1 (Distinct positive representatives).

$$\forall l:\mathrm{List}\left(\mathbb{N}\right),\mathrm{ChoosableInitial}\left(l\right)⟺(\exists f:\mathrm{Fin}\left(\mathrm{length}\left(l\right)\right)\Rightarrow \mathbb{N},\mathrm{Injective}\left(f\right)\wedge (\forall i:\mathrm{Fin}\left(\mathrm{length}\left(l\right)\right),1\le f\left(i\right)\wedge f\left(i\right)\le \mathrm{get}\left(l,i\right)))$$

Formalization. D5/S1/Words/Compositions/ChoosableInitialIntervals.ChoosableInitial (✓ std3).

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2025). OEIS A388711. URL: https://oeis.org/A388711.

Commentary.

A representative is chosen at each list position, is at least one, and is at most that position’s part. Injectivity makes the choices distinct. A zero part has no allowed choice; the empty family is choosable.

Definition 1.2 (The diagonal condition).

$$\forall l:\mathrm{List}\left(\mathbb{N}\right),\mathrm{Superdiagonal}\left(l\right)⟺(\forall i:\mathrm{Fin}\left(\mathrm{length}\left(l\right)\right),i+1\le \mathrm{get}\left(l,i\right))$$

Formalization. D5/S1/Words/Compositions/ChoosableInitialIntervals.Superdiagonal (✓ std3).

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2025). OEIS A388711. URL: https://oeis.org/A388711.

Commentary.

The part at zero-based position i is at least i+1. The list theorem does not assume positivity; the condition itself implies it.

Lemma 1.3 (Order invariance).

$$\forall l:\mathrm{List}\left(\mathbb{N}\right),\forall m:\mathrm{List}\left(\mathbb{N}\right),\mathrm{Perm}\left(l,m\right)⟹(\mathrm{ChoosableInitial}\left(l\right)⟺\mathrm{ChoosableInitial}\left(m\right))$$

Proof. Machine-checked in Lean as D5/S1/Words/Compositions/ChoosableInitialIntervals.choosableInitial_congr_perm (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2025). OEIS A388711. URL: https://oeis.org/A388711.

Commentary.

Represent the choice map as a nodup list related positionwise to the parts. Mathlib’s relational permutation lemma transports that list and preserves nodup. Thus choosability depends only on the multiset of parts.

Theorem 1.4 (The initial-interval criterion).

$$\forall l:\mathrm{List}\left(\mathbb{N}\right),\mathrm{Pairwise}\left((a,b\mapsto a\le b),l\right)⟹(\mathrm{ChoosableInitial}\left(l\right)⟺\mathrm{Superdiagonal}\left(l\right))$$

Proof. Machine-checked in Lean as D5/S1/Words/Compositions/ChoosableInitialIntervals.choosableInitial_iff_superdiagonal (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2025). OEIS A388711. URL: https://oeis.org/A388711.

Commentary.

Restrict the injection to the first i+1 positions. Monotonicity bounds all these positive representatives by the part at i. Subtracting one gives an injection Fin(i+1) into Fin(l[i]); finite cardinal comparison proves the bound. In the other direction choose i+1. This elementary criterion is not claimed as a new mathematical theorem or a new form of Hall’s theorem.

Theorem 1.5 (Equality of the two partition counts).

$$\forall n:\mathbb{N},\forall k:\mathbb{N},\mathrm{card}\left(\mathrm{filter}\left((p\mapsto \mathrm{card}\left(\mathrm{parts}\left(p\right)\right)=k\wedge ChoosableInitial\left(\mathrm{sort}\left(\mathrm{parts}\left(p\right),(a,b\mapsto a\ge b)\right)\right)),(\mathrm{univ}\left(\right):\mathrm{Finset}\left(\mathrm{Partition}\left(n\right)\right))\right)\right)=\mathrm{card}\left(\mathrm{filter}\left((p\mapsto \mathrm{card}\left(\mathrm{parts}\left(p\right)\right)=k\wedge Superdiagonal\left(\mathrm{sort}\left(\mathrm{parts}\left(p\right),(a,b\mapsto a\le b)\right)\right)),(\mathrm{univ}\left(\right):\mathrm{Finset}\left(\mathrm{Partition}\left(n\right)\right))\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Compositions/ChoosableInitialIntervals.card_choosable_eq_superdiagonal (✓ std3). ∎

Resolves. Problems/oeis-a388711-choosable-initial-intervals (proved) by D5/S1/Words/Compositions/ChoosableInitialIntervals.card_choosable_eq_superdiagonal.

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2025). OEIS A388711. URL: https://oeis.org/A388711.

Commentary.

Both filters range over Mathlib’s partitions of n and require exactly k positive parts. Order invariance relates descending and ascending order; the initial-interval criterion then identifies the predicates. The equality holds for all n and k, including the empty partition at n=k=0.

References

• Truth anchor: D5/S1/Words/Compositions/ChoosableInitialIntervals.ChoosableInitial
• Truth anchor: D5/S1/Words/Compositions/ChoosableInitialIntervals.Superdiagonal
• Truth anchor: D5/S1/Words/Compositions/ChoosableInitialIntervals.card_choosable_eq_superdiagonal
• Truth anchor: D5/S1/Words/Compositions/ChoosableInitialIntervals.choosableInitial_congr_perm
• Truth anchor: D5/S1/Words/Compositions/ChoosableInitialIntervals.choosableInitial_iff_superdiagonal