Marriageable and lonely singles partitions

DefinitionSame block after merging two blocks#✓fully proved

Let \(P\) be a set partition of \(\{0, \dots, n-1\}\) and let \(i, j, x, y \in \{0, \dots, n-1\}\). Then \(x\) and \(y\) lie in the same block after merging the blocks of \(i\) and \(j\) if either \(x\) and \(y\) lie in the same block of \(P\), or each of \(x\) and \(y\) lies in the block of \(i\) or in the block of \(j\). For singleton blocks \(\{i\}\) and \(\{j\}\) this joins them into the block \(\{i, j\}\).

def mergedSameBlock {n : ℕ} (P : SetPartition n) (i j x y : Fin n) : Prop :=
  P.part x = P.part y ∨ ((x ∈ P.part i ∨ x ∈ P.part j) ∧ (y ∈ P.part i ∨ y ∈ P.part j))

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 3 (the partition π' obtained by joining {i} and {j}).

Uses 1 · Used by 5

Statement usesSet partition

Used byNumber of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count · Crossing after merging two blocks

DefinitionCrossing after merging two blocks#✓fully proved

Let \(P\) be a set partition of \(\{0, \dots, n-1\}\) and let \(i, j \in \{0, \dots, n-1\}\). The partition obtained from \(P\) by merging the blocks of \(i\) and \(j\) has a crossing if there are \(a < b < c < d\) in \(\{0, \dots, n-1\}\) such that \(a\) and \(c\) lie in one of its blocks and \(b\) and \(d\) lie in a different one of its blocks.

def mergedHasCrossing {n : ℕ} (P : SetPartition n) (i j : Fin n) : Prop :=
  ∃ a b c d : Fin n, a < b ∧ b < c ∧ c < d ∧ mergedSameBlock P i j a c ∧
    mergedSameBlock P i j b d ∧ ¬ mergedSameBlock P i j a b

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definitions 2 and 3 (crossing partitions, the partition π').

Uses 2 · Used by 5

Statement usesSame block after merging two blocks · Set partition

Used byMarriageable singles partition · Number of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count

DefinitionMarriageable singles partition#✓fully proved

A set partition \(P\) of \(\{0, \dots, n-1\}\) is a marriageable singles partition if it has two distinct singleton blocks \(\{i\}\) and \(\{j\}\) such that the partition obtained from \(P\) by joining them into the block \(\{i, j\}\) has no crossing.

def IsMarriageableSingles {n : ℕ} (P : SetPartition n) : Prop :=
  ∃ i j : Fin n, i ≠ j ∧ P.part i = {i} ∧ P.part j = {j} ∧ ¬ mergedHasCrossing P i j

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 3.

Uses 2 · Used by 4

Statement usesCrossing after merging two blocks · Set partition

Used byNumber of lonely singles partitions · Small values of the lonely singles count · Number of marriageable singles partitions · Small values of the marriageable singles count

DefinitionNumber of marriageable singles partitions#✓fully proved

For \(n \ge 0\), \(M_n\) is the number of noncrossing partitions of \(\{0, \dots, n-1\}\) that are marriageable singles partitions.

def marriageableSinglesCount (n : ℕ) : ℕ :=
  (Finset.univ.filter fun P : _root_.NoncrossingPartition n => IsMarriageableSingles P.val).card

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 3.

Uses 7 · Used by 7

Statement usesMarriageable singles partition · Crossing after merging two blocks · Same block after merging two blocks · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Used byRecursive lower bound for marriageable singles partitions · Nonabsolute maximal sets of lanes are counted by marriageable singles partitions · Noncrossing partitions split into lonely and marriageable singles partitions · Strict growth of the lonely and marriageable singles counts · Lower bound for the number of marriageable singles partitions · Small values of the marriageable singles count · The marriageable and lonely singles counts tend to infinity

DefinitionNumber of lonely singles partitions#✓fully proved

For \(n \ge 0\), \(L_n\) is the number of lonely singles partitions of \(\{0, \dots, n-1\}\), that is, of noncrossing partitions of \(\{0, \dots, n-1\}\) that are not marriageable singles partitions.

def lonelySinglesCount (n : ℕ) : ℕ :=
  (Finset.univ.filter fun P : _root_.NoncrossingPartition n => ¬ IsMarriageableSingles P.val).card

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 3.

Uses 7 · Used by 7

Statement usesMarriageable singles partition · Crossing after merging two blocks · Same block after merging two blocks · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Used byAbsolute maximal sets of lanes are counted by lonely singles partitions · Noncrossing partitions split into lonely and marriageable singles partitions · Maximal sets of lanes without U-turns are counted by lonely singles partitions · Strict growth of the lonely and marriageable singles counts · Lower bound for the number of lonely singles partitions · Small values of the lonely singles count · The marriageable and lonely singles counts tend to infinity

TheoremSmall values of the marriageable singles count#✓fully proved

For every \(n \le 1\), the number of marriageable singles partitions of \(\{0, \dots, n-1\}\) is \(M_n = 0\): a marriageable singles partition needs two distinct points.

theorem marriageableSinglesCount_of_le_one {n : ℕ} (hn : n ≤ 1) :
    marriageableSinglesCount n = 0

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Table 1.

Uses 8

Statement usesNumber of marriageable singles partitions

Proof usesMarriageable singles partition · Crossing after merging two blocks · Same block after merging two blocks · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

TheoremSmall values of the lonely singles count#✓fully proved

The numbers of lonely singles partitions of \(\{0, \dots, n-1\}\) for \(n = 0\) and \(n = 1\) are \(L_0 = 1\) and \(L_1 = 1\).

theorem lonelySinglesCount_zero_one : lonelySinglesCount 0 = 1 ∧ lonelySinglesCount 1 = 1

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Table 1.

Uses 10

Statement usesNumber of lonely singles partitions

Proof usesMarriageable singles partition · Crossing after merging two blocks · Same block after merging two blocks · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition · Noncrossing partitions of a one-element set · Noncrossing partitions of the empty set

DefinitionNoncrossing partitions by number of blocks and of singleton blocks#✓fully proved

For natural numbers \(n\), \(m\) and \(k\), \(NC_{n,m,k}\) is the number of noncrossing partitions of \(\{0, \dots, n-1\}\) that have exactly \(m\) blocks, exactly \(k\) of which are singletons.

def noncrossingBlockSingletonCount (n m k : ℕ) : ℕ :=
  (Finset.univ.filter fun P : _root_.NoncrossingPartition n =>
    P.val.parts.card = m ∧ (P.val.parts.filter fun B => B.card = 1).card = k).card

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 23.

Uses 4 · Used by 2

Statement usesNoncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Used byCounting noncrossing partitions with no or one singleton block · Base value of the noncrossing block and singleton count

TheoremBase value of the noncrossing block and singleton count#✓fully proved

Exactly one noncrossing partition of the empty set has \(0\) blocks, \(0\) of which are singletons, namely the empty partition; that is, \(NC_{0,0,0} = 1\), where \(NC_{n,m,k}\) is the number of noncrossing partitions of \(\{0, \dots, n-1\}\) with \(m\) blocks of which \(k\) are singletons.

theorem noncrossingBlockSingletonCount_zero : noncrossingBlockSingletonCount 0 0 0 = 1

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Remark 25.

Uses 6

Statement usesNoncrossing partitions by number of blocks and of singleton blocks

Proof usesNoncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition · Noncrossing partitions of the empty set

DefinitionZero-extended binomial coefficient#✓fully proved

For integers \(a\) and \(b\), the zero-extended binomial coefficient \(\binom{a}{b}\) is the usual binomial coefficient of \(a\) and \(b\) when \(a \ge 0\) and \(b \ge 0\), and \(0\) otherwise.

This is the convention under which the paper's formulas "give \(0\)" in the degenerate cases (for example \(\binom{-1}{0} = 0\) in the count of noncrossing partitions of a one-element set with one block and no singleton block).

def zeroExtendedChoose (a b : ℤ) : ℕ :=
  if 0 ≤ a ∧ 0 ≤ b then a.toNat.choose b.toNat else 0

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, proof of Proposition 24 (degenerate cases giving 0).

Used by 5

Used byLower bound for the number of lonely singles partitions · Lower bound for the number of marriageable singles partitions · Counting noncrossing partitions with no or one singleton block · The zero-extended binomial coefficient on natural numbers · The zero-extended binomial coefficient vanishes at \((-1, 0)\)

TheoremThe zero-extended binomial coefficient on natural numbers#✓fully proved

Extend the binomial coefficient \(\binom{a}{b}\) to all integers \(a\), \(b\) by setting it to \(0\) when \(a < 0\) or \(b < 0\). For all natural numbers \(a\) and \(b\), this extended binomial coefficient at \(a\) and \(b\) viewed as integers equals the usual binomial coefficient \(\binom{a}{b}\).

theorem zeroExtendedChoose_natCast (a b : ℕ) : zeroExtendedChoose a b = a.choose b

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, proof of Proposition 24 (degenerate cases giving 0).

Uses 1

Statement usesZero-extended binomial coefficient

TheoremThe zero-extended binomial coefficient vanishes at \((-1, 0)\)#✓fully proved

Extend the binomial coefficient \(\binom{a}{b}\) to all integers \(a\), \(b\) by setting it to \(0\) when \(a < 0\) or \(b < 0\). Under this convention \(\binom{-1}{0} = 0\).

theorem zeroExtendedChoose_neg_one_zero : zeroExtendedChoose (-1) 0 = 0

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, proof of Proposition 24 (degenerate cases giving 0).

Uses 1

Statement usesZero-extended binomial coefficient

DefinitionLanes with a common point#✓fully proved

The standard road intersection of size \(n\) has entries \(E_0, \dots, E_{n-1}\) and exits \(X_0, \dots, X_{n-1}\) on a circle, with \(E_i\) at position \(2i\) and \(X_j\) at position \(2j + 1\); the lane \(E_iX_j\) is the chord from \(E_i\) to \(X_j\). Two lanes \(E_iX_j\) and \(E_{i'}X_{j'}\) have a common point if \(i = i'\), or \(j = j'\), or exactly one of the positions \(2i'\) and \(2j' + 1\) lies strictly between \(2i\) and \(2j + 1\) (that is, the chords cross).

def lanesMeet {n : ℕ} (ℓ ℓ' : Fin n × Fin n) : Prop :=
  ℓ.1 = ℓ'.1 ∨ ℓ.2 = ℓ'.2 ∨
    (let lo := min (2 * ℓ.1.val) (2 * ℓ.2.val + 1)
     let hi := max (2 * ℓ.1.val) (2 * ℓ.2.val + 1)
     ((lo < 2 * ℓ'.1.val ∧ 2 * ℓ'.1.val < hi) ↔ ¬ (lo < 2 * ℓ'.2.val + 1 ∧ 2 * ℓ'.2.val + 1 < hi)))

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definitions 10 and 13 (lanes, noncrossing lanes).

Used by 6

Used byAbsolute maximal sets of lanes are counted by lonely singles partitions · Nonabsolute maximal sets of lanes are counted by marriageable singles partitions · Maximal sets of lanes without U-turns are counted by lonely singles partitions · Maximal set of lanes · Maximal sets of lanes and noncrossing partitions · Maximal sets of lanes for an intersection of size two

DefinitionMaximal set of lanes#✓fully proved

In the standard road intersection of size \(n\), the lane \(E_iX_j\) joins the entry \(E_i\) to the exit \(X_j\), for \(i, j \in \{0, \dots, n-1\}\). Given a set \(A\) of allowed lanes, a set \(S\) of lanes is a maximal set of lanes (MSL) among \(A\) if \(S \subseteq A\), no two distinct lanes of \(S\) have a common point, and every lane of \(A\) not in \(S\) has a common point with some lane of \(S\). The standard road intersection allows every lane; the restricted one forbids the U-turns \(E_iX_i\).

def IsMaximalSetOfLanes {n : ℕ} (allowed S : Finset (Fin n × Fin n)) : Prop :=
  S ⊆ allowed ∧ (∀ ℓ ∈ S, ∀ ℓ' ∈ S, ℓ ≠ ℓ' → ¬ lanesMeet ℓ ℓ') ∧
    ∀ ℓ ∈ allowed, ℓ ∉ S → ∃ ℓ' ∈ S, lanesMeet ℓ ℓ'

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definitions 12 and 13 (restricted standard road intersection, MSL).

Uses 1 · Used by 6

Statement usesLanes with a common point

Used byAbsolute maximal sets of lanes are counted by lonely singles partitions · Nonabsolute maximal sets of lanes are counted by marriageable singles partitions · Maximal sets of lanes without U-turns are counted by lonely singles partitions · Absolute maximal set of lanes · Maximal sets of lanes and noncrossing partitions · Maximal sets of lanes for an intersection of size two

DefinitionAbsolute maximal set of lanes#✓fully proved

In the standard road intersection of size \(n\), the lane \(E_iX_j\) joins the entry \(E_i\) to the exit \(X_j\), for \(i, j \in \{0, \dots, n-1\}\). A set \(S\) of lanes is absolute if it is a maximal set of lanes among all lanes and there are no \(i \ne j\) such that \(S\) contains both U-turns \(E_iX_i\) and \(E_jX_j\) and replacing these two lanes in \(S\) by \(E_iX_j\) and \(E_jX_i\) gives again a maximal set of lanes among all lanes.

def IsAbsoluteMaximalSetOfLanes {n : ℕ} (S : Finset (Fin n × Fin n)) : Prop :=
  IsMaximalSetOfLanes Finset.univ S ∧
    ¬ ∃ i j : Fin n, i ≠ j ∧ (i, i) ∈ S ∧ (j, j) ∈ S ∧
      IsMaximalSetOfLanes Finset.univ (insert (i, j) (insert (j, i) ((S.erase (i, i)).erase (j, j))))

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 15.

Uses 1 · Used by 2

Statement usesMaximal set of lanes

Used byAbsolute maximal sets of lanes are counted by lonely singles partitions · Nonabsolute maximal sets of lanes are counted by marriageable singles partitions

TheoremMaximal sets of lanes for an intersection of size two#✓fully proved

Write \(E_iX_j\) for the lane from the \(i\)-th entry to the \(j\)-th exit. In the standard road intersection of size \(2\), in which every lane is allowed, the maximal sets of lanes are exactly \(\{E_1X_1, E_2X_2\}\) and \(\{E_1X_2, E_2X_1\}\).

theorem maximalSetsOfLanes_two :
    (Finset.univ.filter fun S : Finset (Fin 2 × Fin 2) => IsMaximalSetOfLanes Finset.univ S) =
      {{(0, 0), (1, 1)}, {(0, 1), (1, 0)}}

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Definition 13 (MSL).

Uses 2

Statement usesMaximal set of lanes · Lanes with a common point

TheoremNoncrossing partitions split into lonely and marriageable singles partitions#●ready to prove

For every \(n \ge 0\), the number \(C_n\) of noncrossing partitions of \(\{0, \dots, n-1\}\) equals \(L_n + M_n\), where \(M_n\) is the number of those that are marriageable singles partitions and \(L_n\) is the number of those that are not.

public theorem_wanted card_noncrossingPartition_eq_lonely_add_marriageable (n : ℕ) :
    Fintype.card (_root_.NoncrossingPartition n) =
      lonelySinglesCount n + marriageableSinglesCount n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Lemma 6 (jis-2025-25.1.1-lem-6).

Uses 6

Statement usesNumber of lonely singles partitions · Number of marriageable singles partitions · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

TheoremMaximal sets of lanes and noncrossing partitions#●ready to prove

For every \(n \ge 0\), the maximal sets of lanes of the standard road intersection of size \(n\), in which every lane is allowed, are in bijection with the noncrossing partitions of \(\{0, \dots, n-1\}\), and their number is the Catalan number \(C_n\).

public theorem_wanted maximalSetsOfLanes_equiv_noncrossingPartition (n : ℕ) :
    Nonempty ({S : Finset (Fin n × Fin n) // IsMaximalSetOfLanes Finset.univ S} ≃
      _root_.NoncrossingPartition n) ∧
    (Finset.univ.filter fun S : Finset (Fin n × Fin n) =>
      IsMaximalSetOfLanes Finset.univ S).card = catalan n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Lemma 16 (jis-2025-25.1.1-lem-16).

Uses 3

Statement usesMaximal set of lanes · Lanes with a common point · Noncrossing partition

TheoremNonabsolute maximal sets of lanes are counted by marriageable singles partitions#●ready to prove

For every \(n \ge 0\), the number of maximal sets of lanes of the standard road intersection of size \(n\) that are not absolute equals \(M_n\), the number of noncrossing partitions of \(\{0, \dots, n-1\}\) that are marriageable singles partitions.

public theorem_wanted card_nonabsolute_maximalSetsOfLanes (n : ℕ) :
    (Finset.univ.filter fun S : Finset (Fin n × Fin n) =>
      IsMaximalSetOfLanes Finset.univ S ∧ ¬ IsAbsoluteMaximalSetOfLanes S).card =
      marriageableSinglesCount n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Corollary 17 (jis-2025-25.1.1-cor-17).

Uses 4

Statement usesAbsolute maximal set of lanes · Maximal set of lanes · Lanes with a common point · Number of marriageable singles partitions

TheoremAbsolute maximal sets of lanes are counted by lonely singles partitions#●ready to prove

For every \(n \ge 0\), the number of absolute maximal sets of lanes of the standard road intersection of size \(n\) equals \(L_n\), the number of noncrossing partitions of \(\{0, \dots, n-1\}\) that are not marriageable singles partitions.

public theorem_wanted card_absolute_maximalSetsOfLanes (n : ℕ) :
    (Finset.univ.filter fun S : Finset (Fin n × Fin n) => IsAbsoluteMaximalSetOfLanes S).card =
      lonelySinglesCount n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Corollary 18 (jis-2025-25.1.1-cor-18).

Uses 4

Statement usesAbsolute maximal set of lanes · Maximal set of lanes · Lanes with a common point · Number of lonely singles partitions

TheoremMaximal sets of lanes without U-turns are counted by lonely singles partitions#●ready to prove

For every \(n \ge 0\), consider the restricted standard road intersection of size \(n\), in which the lane \(E_iX_j\) from the entry \(E_i\) to the exit \(X_j\), for \(i, j \in \{0, \dots, n-1\}\), is allowed exactly when \(i \ne j\) (the U-turns \(E_iX_i\) are forbidden). The number of maximal sets of lanes among these allowed lanes equals \(L_n\), the number of noncrossing partitions of \(\{0, \dots, n-1\}\) that are not marriageable singles partitions.

public theorem_wanted card_restricted_maximalSetsOfLanes (n : ℕ) :
    (Finset.univ.filter fun S : Finset (Fin n × Fin n) =>
      IsMaximalSetOfLanes (Finset.univ.filter fun ℓ : Fin n × Fin n => ℓ.1 ≠ ℓ.2) S).card =
      lonelySinglesCount n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Corollary 19 (jis-2025-25.1.1-cor-19).

Uses 3

Statement usesMaximal set of lanes · Lanes with a common point · Number of lonely singles partitions

TheoremStrict growth of the lonely and marriageable singles counts#●ready to prove

\(L_n < L_{n+1}\) for every \(n \ge 2\), and \(M_n < M_{n+1}\) for every \(n \ge 3\), where \(M_n\) is the number of noncrossing partitions of \(\{0, \dots, n-1\}\) that are marriageable singles partitions and \(L_n\) is the number of those that are not.

public theorem_wanted lonely_marriageable_strictMono :
    (∀ n, 2 ≤ n → lonelySinglesCount n < lonelySinglesCount (n + 1)) ∧
    ∀ n, 3 ≤ n → marriageableSinglesCount n < marriageableSinglesCount (n + 1)

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Proposition 20 (jis-2025-25.1.1-prop-20).

Uses 2

Statement usesNumber of lonely singles partitions · Number of marriageable singles partitions

TheoremThe marriageable and lonely singles counts tend to infinity#●ready to prove

Let \(M_n\) and \(L_n\) be the numbers of noncrossing partitions of \(\{0, \dots, n-1\}\) that are marriageable singles partitions and lonely singles partitions, respectively. Then \(M_n \to \infty\) and \(L_n \to \infty\) as \(n \to \infty\).

public theorem_wanted tendsto_marriageable_lonely_atTop :
    Filter.Tendsto marriageableSinglesCount Filter.atTop Filter.atTop ∧
      Filter.Tendsto lonelySinglesCount Filter.atTop Filter.atTop

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Corollary 21 (jis-2025-25.1.1-cor-21).

Uses 2

Statement usesNumber of lonely singles partitions · Number of marriageable singles partitions

TheoremRecursive lower bound for marriageable singles partitions#●ready to prove

For every \(n \ge 0\), \(C_n + 3M_n \le M_{n+2}\), where \(C_n\) is the number of noncrossing partitions of \(\{0, \dots, n-1\}\) and \(M_n\) is the number of those that are marriageable singles partitions.

public theorem_wanted card_add_three_mul_marriageable_le (n : ℕ) :
    Fintype.card (_root_.NoncrossingPartition n) + 3 * marriageableSinglesCount n ≤
      marriageableSinglesCount (n + 2)

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Proposition 22 (jis-2025-25.1.1-prop-22).

Uses 5

Statement usesNumber of marriageable singles partitions · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

TheoremCounting noncrossing partitions with no or one singleton block#●ready to prove

Write \(NC_{n,m,k}\) for the number of noncrossing partitions of \(\{0, \dots, n-1\}\) with \(m\) blocks of which \(k\) are singletons, and extend the binomial coefficient \(\binom{a}{b}\) to all integers \(a\), \(b\) by setting it to \(0\) when \(a < 0\) or \(b < 0\). For all natural numbers \(n\) and \(m\): if \((n, m) \ne (0, 0)\), then the following holds in \(\mathbb{Q}\), where \(1/0\) is taken to be \(0\) (the denominator vanishes only for \(m = n + 1\), where \(\binom{n}{m} = 0\)):

\[NC_{n,m,0} = \frac{1}{n-m+1} \binom{n}{m} \binom{n-m-1}{m-1};\]

and if \((n, m) \ne (1, 1)\), then

\[NC_{n,m,1} = \binom{n}{m-1} \binom{n-m-1}{m-2}.\]

public theorem_wanted noncrossingBlockSingletonCount_formulas (n m : ℕ) :
    ((n, m) ≠ (0, 0) →
      (noncrossingBlockSingletonCount n m 0 : ℚ) =
        1 / ((n : ℚ) - m + 1) * zeroExtendedChoose n m *
          zeroExtendedChoose ((n : ℤ) - m - 1) ((m : ℤ) - 1)) ∧
    ((n, m) ≠ (1, 1) →
      noncrossingBlockSingletonCount n m 1 =
        zeroExtendedChoose n ((m : ℤ) - 1) * zeroExtendedChoose ((n : ℤ) - m - 1) ((m : ℤ) - 2))

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Proposition 24 (jis-2025-25.1.1-prop-24).

Uses 2

Statement usesNoncrossing partitions by number of blocks and of singleton blocks · Zero-extended binomial coefficient

TheoremLower bound for the number of lonely singles partitions#●ready to prove

For every \(n \ge 2\), the number \(L_n\) of lonely singles partitions of \(\{0, \dots, n-1\}\) satisfies

\[ L_n \ge \sum_{m=1}^{\lfloor n/2 \rfloor} \frac{1}{n-m+1} \binom{n}{m} \binom{n-m-1}{m-1} + \sum_{m=2}^{\lfloor (n+1)/2 \rfloor} \binom{n}{m-1} \binom{n-m-1}{m-2}, \]

where a binomial coefficient \(\binom{a}{b}\) with \(a < 0\) or \(b < 0\) is taken to be \(0\).

public theorem_wanted lonelySinglesCount_ge_sum (n : ℕ) (hn : 2 ≤ n) :
    (∑ m ∈ Finset.Icc 1 (n / 2), 1 / ((n : ℚ) - m + 1) * zeroExtendedChoose n m *
        zeroExtendedChoose ((n : ℤ) - m - 1) ((m : ℤ) - 1)) +
      (∑ m ∈ Finset.Icc 2 ((n + 1) / 2),
        (zeroExtendedChoose n ((m : ℤ) - 1) * zeroExtendedChoose ((n : ℤ) - m - 1) ((m : ℤ) - 2) :
          ℚ)) ≤
      lonelySinglesCount n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Proposition 26 (jis-2025-25.1.1-prop-26).

Uses 2

Statement usesNumber of lonely singles partitions · Zero-extended binomial coefficient

TheoremLower bound for the number of marriageable singles partitions#●ready to prove

Extend the binomial coefficient \(\binom{a}{b}\) to all integers \(a\), \(b\) by setting it to \(0\) when \(a < 0\) or \(b < 0\), and for every natural number \(N\) let

\[S(N) = \sum_{m=0}^{\lfloor N/2 \rfloor} \frac{1}{N-m+1} \binom{N}{m} \binom{N-m-1}{m-1}.\]

For every \(n \ge 3\), the number \(M_n\) of noncrossing partitions of \(\{0, \dots, n-1\}\) that are marriageable singles partitions satisfies

\[M_n \ge \sum_{i=1}^{n-1} \sum_{j=i+1}^{n} S(n+i-j-1)\, S(j-i-1).\]

For \(N \ge 1\), \(S(N)\) is the number of noncrossing partitions of an \(N\)-element set with no singleton block; with the convention above, \(S(0) = 0\).

public theorem_wanted marriageableSinglesCount_ge_sum (n : ℕ) (hn : 3 ≤ n) :
    (∑ i ∈ Finset.Icc 1 (n - 1), ∑ j ∈ Finset.Icc (i + 1) n,
      (∑ m ∈ Finset.range ((n + i - j - 1) / 2 + 1),
          1 / ((n : ℚ) + i - j - m) * zeroExtendedChoose ((n : ℤ) + i - j - 1) m *
            zeroExtendedChoose ((n : ℤ) + i - j - m - 2) ((m : ℤ) - 1)) *
        (∑ m ∈ Finset.range ((j - i - 1) / 2 + 1),
          1 / ((j : ℚ) - i - m) * zeroExtendedChoose ((j : ℤ) - i - 1) m *
            zeroExtendedChoose ((j : ℤ) - i - m - 2) ((m : ℤ) - 1))) ≤
      marriageableSinglesCount n

Sources

• Julien Rouyer and Alain Ninet, Two New Integer Sequences Related to Crossroads and Catalan Numbers, Journal of Integer Sequences 28 (2025), Article 25.1.1, Proposition 27 (jis-2025-25.1.1-prop-27).

Uses 2

Statement usesNumber of marriageable singles partitions · Zero-extended binomial coefficient

16 fully proved11 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.