Chvátal–Sankoff constant

AbbreviationBinary strings#✓fully proved

For a natural number \(n\), a binary string of length \(n\) is a function from \(\{0, 1, \dots, n - 1\}\) to \(\{\mathrm{false}, \mathrm{true}\}\), that is, a sequence of \(n\) bits listed in order.

abbrev BinaryString (n : ℕ) := Fin n → Bool
Used by 15
Used byConcatenation of binary string pairs · Pairs of binary strings · Lengths of common subsequences · Existence of a longest common subsequence · Expected length of a longest common subsequence · Expected LCS length is at most the string length · Expected LCS length is nonnegative · Superadditivity of the expected LCS length · Common subsequence · Length of a longest common subsequence · Superadditivity of the LCS length under concatenation · The LCS length as a bounded maximum · The LCS length is the maximum common-subsequence length · The LCS length is at most the string length · The finite set of pairs of binary strings

AbbreviationPairs of binary strings#✓fully proved

For a natural number \(n\), a pair of binary strings of length \(n\) is an ordered pair \((x, y)\) of binary strings \(x\) and \(y\), each of length \(n\). These pairs form the finite sample space over which expected longest common subsequence lengths are taken.

abbrev BinaryStringPair (n : ℕ) := BinaryString n × BinaryString n
Uses 1 · Used by 6
Statement usesBinary strings
Used byConcatenation of binary string pairs · Expected length of a longest common subsequence · Expected LCS length is at most the string length · Expected LCS length is nonnegative · Superadditivity of the expected LCS length · The finite set of pairs of binary strings

DefinitionCommon subsequence#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), a finite sequence of bits \(z\) is a common subsequence of \(x\) and \(y\) if \(z\) is obtained both from \(x\) and from \(y\) by deleting some (possibly no) entries and keeping the remaining entries in order.

Repeated symbols are kept with their multiplicities.

def IsCommonSubsequence {n : ℕ} (z : List Bool)
    (x y : BinaryString n) : Prop :=
  z.Sublist (List.ofFn x) ∧ z.Sublist (List.ofFn y)
Uses 1 · Used by 6
Statement usesBinary strings
Used byLengths of common subsequences · Existence of a longest common subsequence · Superadditivity of the LCS length under concatenation · The LCS length as a bounded maximum · The LCS length is the maximum common-subsequence length · The LCS length is at most the string length

DefinitionLengths of common subsequences#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), the set of natural numbers \(k\) such that some binary list of length \(k\) is a common subsequence of \(x\) and \(y\).

def commonSubsequenceLengths {n : ℕ} (x y : BinaryString n) : Set ℕ :=
  {k | ∃ z : List Bool, IsCommonSubsequence z x y ∧ z.length = k}
Uses 2 · Used by 4
Statement usesBinary strings · Common subsequence
Used byExistence of a longest common subsequence · Superadditivity of the LCS length under concatenation · The LCS length as a bounded maximum · The LCS length is the maximum common-subsequence length

DefinitionLength of a longest common subsequence#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), \(\mathrm{LCS}(x, y)\) is the length returned by the dynamic-programming algorithm for the longest common subsequence, applied to \(x\) and \(y\) read as lists of bits.

This value is the greatest length of a common subsequence of \(x\) and \(y\).

def lcsLength {n : ℕ} (x y : BinaryString n) : ℕ :=
  (Cslib.Algorithms.Lean.longestCommonSubsequence
    (List.ofFn x) (List.ofFn y)).ret.1
Uses 2 · Used by 9
Statement usesLongest common subsequence by dynamic programming · Binary strings
Used byExistence of a longest common subsequence · Expected length of a longest common subsequence · Expected LCS length is at most the string length · Expected LCS length is nonnegative · Superadditivity of the expected LCS length · Superadditivity of the LCS length under concatenation · The LCS length as a bounded maximum · The LCS length is the maximum common-subsequence length · The LCS length is at most the string length

TheoremThe LCS length is the maximum common-subsequence length#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), let \(\mathrm{LCS}(x, y)\) be the length returned by the dynamic-programming algorithm for the longest common subsequence on \(x\) and \(y\). Then some common subsequence of \(x\) and \(y\) has length \(\mathrm{LCS}(x, y)\), and every common subsequence of \(x\) and \(y\) has length at most \(\mathrm{LCS}(x, y)\).

theorem lcsLength_isGreatest {n : ℕ} (x y : BinaryString n) :
    IsGreatest (commonSubsequenceLengths x y) (lcsLength x y)
Uses 6 · Used by 3
Statement usesBinary strings · Lengths of common subsequences · Length of a longest common subsequence
Proof usesLongest common subsequence by dynamic programming · Correctness of the longest common subsequence algorithm · Common subsequence
Used byExistence of a longest common subsequence · Superadditivity of the LCS length under concatenation · The LCS length as a bounded maximum

TheoremExistence of a longest common subsequence#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), there is a binary list \(z\) that is a common subsequence of \(x\) and \(y\), whose length equals the LCS length of \(x\) and \(y\), and such that every common subsequence \(w\) of \(x\) and \(y\) has length at most the length of \(z\).

theorem exists_longestCommonSubsequence {n : ℕ} (x y : BinaryString n) :
    ∃ z : List Bool,
      IsCommonSubsequence z x y ∧ z.length = lcsLength x y ∧
        ∀ w : List Bool, IsCommonSubsequence w x y → w.length ≤ z.length
Uses 5 · Used by 1
Statement usesBinary strings · Common subsequence · Length of a longest common subsequence
Proof usesLengths of common subsequences · The LCS length is the maximum common-subsequence length
Used byThe LCS length is at most the string length

TheoremThe LCS length is at most the string length#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), the length \(\mathrm{LCS}(x, y)\) of a longest common subsequence satisfies \(\mathrm{LCS}(x, y) \le n\).

theorem lcsLength_le {n : ℕ} (x y : BinaryString n) : lcsLength x y ≤ n
Uses 4 · Used by 2
Statement usesBinary strings · Length of a longest common subsequence
Proof usesCommon subsequence · Existence of a longest common subsequence
Used byExpected LCS length is at most the string length · The LCS length as a bounded maximum

TheoremThe LCS length as a bounded maximum#✓fully proved

For binary strings \(x\) and \(y\) of length \(n\), the length \(\mathrm{LCS}(x, y)\) of a longest common subsequence equals the largest \(k \le n\) such that \(x\) and \(y\) have a common subsequence of length \(k\) (such \(k\) exist, since the empty sequence is a common subsequence).

theorem lcsLength_eq_findGreatest {n : ℕ} (x y : BinaryString n) :
    lcsLength x y =
      (by
        classical
        exact Nat.findGreatest (fun k => k ∈ commonSubsequenceLengths x y) n)
Uses 6
Statement usesBinary strings · Lengths of common subsequences · Length of a longest common subsequence
Proof usesCommon subsequence · The LCS length is the maximum common-subsequence length · The LCS length is at most the string length

DefinitionThe finite set of pairs of binary strings#✓fully proved

For a natural number \(n\), this is the finite set of all ordered pairs \((x, y)\) of binary strings \(x\) and \(y\) of length \(n\).

def uniformBinaryStringPairs (n : ℕ) : Finset (BinaryStringPair n) :=
  Finset.univ
Uses 2 · Used by 3
Statement usesBinary strings · Pairs of binary strings
Used byExpected length of a longest common subsequence · Expected LCS length is at most the string length · Expected LCS length is nonnegative

DefinitionExpected length of a longest common subsequence#✓fully proved

For \(n \in \mathbb{N}\), the expected LCS length \(E_n\) is the average of \(\mathrm{LCS}(x, y)\), the length of a longest common subsequence of \(x\) and \(y\), over all ordered pairs \((x, y)\) of binary strings of length \(n\): it is the sum of \(\mathrm{LCS}(x, y)\) over these pairs divided by their number \(4^n\). Equivalently, \(E_n\) is the expectation of \(\mathrm{LCS}(x, y)\) for two independent uniformly random binary strings \(x\), \(y\) of length \(n\).

def expectedLCSLength (n : ℕ) : ℝ :=
  (∑ pair ∈ uniformBinaryStringPairs n,
      (lcsLength pair.1 pair.2 : ℝ)) /
    (Fintype.card (BinaryStringPair n) : ℝ)
Uses 4 · Used by 6
Statement usesBinary strings · Pairs of binary strings · Length of a longest common subsequence · The finite set of pairs of binary strings
Used bySuperadditivity implies the binary LCS limit exists · Expected LCS length is at most the string length · Expected LCS length is nonnegative · Superadditivity of the expected LCS length · Normalized expected LCS length · Normalized expected LCS lengths lie in \((0,1)\)

TheoremExpected LCS length is nonnegative#✓fully proved

For every \(n\), the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\) is at least \(0\).

theorem expectedLCSLength_nonneg (n : ℕ) : 0 ≤ expectedLCSLength n
Uses 5 · Used by 1
Statement usesExpected length of a longest common subsequence
Proof usesBinary strings · Pairs of binary strings · Length of a longest common subsequence · The finite set of pairs of binary strings
Used byNormalized expected LCS lengths lie in \((0,1)\)

TheoremExpected LCS length is at most the string length#✓fully proved

For every \(n\), the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\) is at most \(n\).

theorem expectedLCSLength_le (n : ℕ) : expectedLCSLength n ≤ n
Uses 6 · Used by 2
Statement usesExpected length of a longest common subsequence
Proof usesBinary strings · Pairs of binary strings · Length of a longest common subsequence · The LCS length is at most the string length · The finite set of pairs of binary strings
Used bySuperadditivity implies the binary LCS limit exists · Normalized expected LCS lengths lie in \((0,1)\)

DefinitionNormalized expected LCS length#✓fully proved

For \(n \ge 1\), the normalized expected LCS length at \(n\) is \(E_n / n\), where \(E_n\) is the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). At \(n = 0\) it is defined to be \(0\).

def normalizedExpectedLCS (n : ℕ) : ℝ :=
  if n = 0 then 0 else expectedLCSLength n / (n : ℝ)
Uses 1 · Used by 6
Statement usesExpected length of a longest common subsequence
Used byBinary Chvátal–Sankoff constant · Trivial bounds for the binary Chvátal–Sankoff constant · Statement of the Chvátal–Sankoff limit theorem · Superadditivity implies the binary LCS limit exists · Normalized expected LCS lengths lie in \((0,1)\) · Any limit of the normalized expected LCS lengths is the binary Chvátal–Sankoff constant

TheoremNormalized expected LCS lengths lie in \((0,1)\)#✓fully proved

For every natural number \(n\), the normalized expected LCS length at \(n\) (the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\), divided by \(n\), and \(0\) for \(n = 0\)) lies in the closed interval \([0,1]\).

theorem normalizedExpectedLCS_mem_Icc (n : ℕ) :
    normalizedExpectedLCS n ∈ Set.Icc (0 : ℝ) 1
Uses 4 · Used by 1
Statement usesNormalized expected LCS length
Proof usesExpected length of a longest common subsequence · Expected LCS length is at most the string length · Expected LCS length is nonnegative
Used byTrivial bounds for the binary Chvátal–Sankoff constant

DefinitionBinary Chvátal–Sankoff constant#✓fully proved

Let \(L_n\) be the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). The binary Chvátal–Sankoff constant is the real number \(\liminf_{n \to \infty} \mathbb{E}[L_n]/n\).

For every \(n \ge 1\) the quotient \(\mathbb{E}[L_n]/n\) lies in \([0, 1]\), so this limit inferior is finite. By the theorem of Chvátal and Sankoff the sequence converges, so the constant equals the ordinary limit \(\lim_{n \to \infty} \mathbb{E}[L_n]/n\); defining it as a limit inferior avoids choosing an arbitrary value before convergence is known.

noncomputable def binaryChvatalSankoffConstant : ℝ :=
  Filter.liminf normalizedExpectedLCS Filter.atTop
Uses 1 · Used by 2
Statement usesNormalized expected LCS length
Used byCatalogue notation for the binary Chvátal–Sankoff constant · Any limit of the normalized expected LCS lengths is the binary Chvátal–Sankoff constant

AbbreviationCatalogue notation for the binary Chvátal–Sankoff constant#✓fully proved

Let \(L_n\) be the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). The notation \(C_{31a}\) stands for the binary Chvátal–Sankoff constant \(\liminf_{n \to \infty} \mathbb{E}[L_n]/n\).

noncomputable abbrev C31a : ℝ :=
  binaryChvatalSankoffConstant
Uses 1 · Used by 12
Statement usesBinary Chvátal–Sankoff constant
Used byTrivial bounds for the binary Chvátal–Sankoff constant · Statement of the Chvátal–Sankoff positivity bound · Statement of Dančík's lower bound · Statement of the Dančík–Paterson upper bound · Statement of the Heineman et al. lower bound · Statement of Lueker's lower bound · Statement of Lueker's upper bound · Statement of the reported 2026 lower bound \(0.79970\) · Statement of the trivial lower bound · The binary Chvátal–Sankoff constant is nonnegative · Trivial upper bound for the binary Chvátal–Sankoff constant · The binary Chvátal–Sankoff constant is at most one

DefinitionStatement of the Chvátal–Sankoff limit theorem#✓fully proved

Let \(L_n\) be the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). This proposition asserts that the sequence \(\mathbb{E}[L_n]/n\) converges to a real number as \(n \to \infty\). Chvátal and Sankoff proved that it holds.

def chvatalSankoffLimitExists : Prop :=
  ∃ c : ℝ, Filter.Tendsto normalizedExpectedLCS Filter.atTop (nhds c)
Uses 1 · Used by 3
Statement usesNormalized expected LCS length
Used byChvátal–Sankoff theorem: the binary LCS limit exists · Superadditivity implies the binary LCS limit exists · Any limit of the normalized expected LCS lengths is the binary Chvátal–Sankoff constant

TheoremTrivial bounds for the binary Chvátal–Sankoff constant#✓fully proved

Let \(L_n\) be the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\), and let \(C_{31a} = \liminf_{n \to \infty} \mathbb{E}[L_n]/n\) be the binary Chvátal–Sankoff constant. Then \(0 \le C_{31a} \le 1\).

theorem binaryChvatalSankoffConstant_mem_Icc :
    C31a ∈ Set.Icc (0 : ℝ) 1
Uses 3 · Used by 2
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Proof usesNormalized expected LCS length · Normalized expected LCS lengths lie in \((0,1)\)
Used byThe binary Chvátal–Sankoff constant is nonnegative · The binary Chvátal–Sankoff constant is at most one

DefinitionTrivial upper bound for the binary Chvátal–Sankoff constant#✓fully proved

Let \(C_{31a}\) be the binary Chvátal–Sankoff constant: the limit inferior as \(n \to \infty\) of \(E_n / n\), where \(E_n\) is the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). This is the proposition \(C_{31a} \le 1\).

def trivialUpperBound : Prop :=
  C31a ≤ 1
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byThe binary Chvátal–Sankoff constant is at most one

DefinitionStatement of the Dančík–Paterson upper bound#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(\gamma\) satisfies \(\gamma \le 0.837623\). Here \(\gamma\) is the limit inferior, as \(n \to \infty\), of \(\mathbb{E}[L_n]/n\), where \(L_n\) is the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\).

def dancikPatersonUpperBound : Prop :=
  C31a ≤ (837623 : ℝ) / 1000000
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byDančík–Paterson upper bound for the binary Chvátal–Sankoff constant

DefinitionStatement of Lueker's upper bound#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(C_{31a}\) is at most \(0.826280\).

def luekerUpperBound : Prop :=
  C31a ≤ (826280 : ℝ) / 1000000
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byLueker's upper bound for the binary Chvátal–Sankoff constant

DefinitionStatement of the trivial lower bound#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(C_{31a}\) satisfies \(0 \le C_{31a}\).

def trivialLowerBound : Prop :=
  0 ≤ C31a
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byThe binary Chvátal–Sankoff constant is nonnegative

DefinitionStatement of the Chvátal–Sankoff positivity bound#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(\gamma\) is strictly positive, \(0 < \gamma\). Here \(\gamma\) is the limit inferior, as \(n \to \infty\), of \(\mathbb{E}[L_n]/n\), where \(L_n\) is the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\).

def chvatalSankoffStrictPositive : Prop :=
  0 < C31a
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byThe binary Chvátal–Sankoff constant is positive

DefinitionStatement of Dančík's lower bound#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(\gamma\) satisfies \(0.773911 \le \gamma\). Here \(\gamma\) is the limit inferior, as \(n \to \infty\), of \(\mathbb{E}[L_n]/n\), where \(L_n\) is the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\).

def dancikLowerBound : Prop :=
  (773911 : ℝ) / 1000000 ≤ C31a
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byDančík's lower bound for the binary Chvátal–Sankoff constant

DefinitionStatement of Lueker's lower bound#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(C_{31a}\) is at least \(0.788071\).

def luekerLowerBound : Prop :=
  (788071 : ℝ) / 1000000 ≤ C31a
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byLueker's lower bound for the binary Chvátal–Sankoff constant

DefinitionStatement of the Heineman et al. lower bound#✓fully proved

For each \(n\), let \(E_n\) be the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\), and let \(C\), the binary Chvátal–Sankoff constant, be the limit inferior of \(E_n / n\) as \(n \to \infty\). This is the proposition \(0.792665992 \le C\).

Heineman et al. obtained this computer-assisted bound; the decimal is an exact rational endpoint.

def heinemanLowerBound : Prop :=
  (792665992 : ℝ) / 1000000000 ≤ C31a
Uses 1 · Used by 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant
Used byHeineman et al. lower bound for the binary Chvátal–Sankoff constant

DefinitionStatement of the reported 2026 lower bound \(0.79970\)#✓fully proved

The proposition that the binary Chvátal–Sankoff constant \(C_{31a}\) is at least \(0.79970\).

This bound was reported in 2026 as AI and computer assisted and has not been verified.

def sourceReportedUnverified2026LowerBound : Prop :=
  (79970 : ℝ) / 100000 ≤ C31a
Uses 1
Statement usesCatalogue notation for the binary Chvátal–Sankoff constant

DefinitionConcatenation of binary string pairs#✓fully proved

For natural numbers \(m\) and \(n\), sending a pair \((x_1, y_1)\) of binary strings of length \(m\) together with a pair \((x_2, y_2)\) of binary strings of length \(n\) to the pair \((x_1 x_2, y_1 y_2)\) of concatenations is a bijection from the product of the set of pairs of length-\(m\) binary strings and the set of pairs of length-\(n\) binary strings onto the set of pairs of binary strings of length \(m + n\). Its inverse splits each string of length \(m + n\) into its first \(m\) and its last \(n\) symbols.

MathlibExt.Combinatorics.BinaryChvatalSankoffWanted.appendBinaryStringPairEquiv · 18 lines 
def appendBinaryStringPairEquiv (m n : ℕ) :
    BinaryStringPair m × BinaryStringPair n ≃ BinaryStringPair (m + n) where
  toFun pair :=
    ((Fin.appendEquiv m n) (pair.1.1, pair.2.1),
      (Fin.appendEquiv m n) (pair.1.2, pair.2.2))
  invFun pair :=
    ((((Fin.appendEquiv m n).symm pair.1).1,
      ((Fin.appendEquiv m n).symm pair.2).1),
      (((Fin.appendEquiv m n).symm pair.1).2,
      ((Fin.appendEquiv m n).symm pair.2).2))
  left_inv pair := by
    rcases pair with ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
    simp
  right_inv pair := by
    rcases pair with ⟨x, y⟩
    apply Prod.ext
    · exact (Fin.appendEquiv m n).apply_symm_apply x
    · exact (Fin.appendEquiv m n).apply_symm_apply y
Sources
  • uniform independent binary-string model; concatenation identifies two independent pairs with a pair of the combined length.
Uses 2 · Used by 1
Statement usesBinary strings · Pairs of binary strings
Used bySuperadditivity of the expected LCS length

TheoremSuperadditivity of the LCS length under concatenation#✓fully proved

Write \(\mathrm{LCS}(x, y)\) for the length of a longest common subsequence of binary strings \(x\) and \(y\) of equal length. Let \(x_1, y_1\) be binary strings of length \(m\) and \(x_2, y_2\) binary strings of length \(n\), and write \(x_1x_2\) and \(y_1y_2\) for the concatenated strings of length \(m + n\). Then \(\mathrm{LCS}(x_1, y_1) + \mathrm{LCS}(x_2, y_2) \le \mathrm{LCS}(x_1x_2, y_1y_2)\).

theorem lcsLength_append_le {m n : ℕ}
    (x₁ y₁ : BinaryString m) (x₂ y₂ : BinaryString n) :
    lcsLength x₁ y₁ + lcsLength x₂ y₂ ≤
      lcsLength (Fin.append x₁ x₂) (Fin.append y₁ y₂)
Sources
  • common subsequences concatenate without changing their order.
Uses 5 · Used by 1
Statement usesBinary strings · Length of a longest common subsequence
Proof usesCommon subsequence · Lengths of common subsequences · The LCS length is the maximum common-subsequence length
Used bySuperadditivity of the expected LCS length

TheoremAny limit of the normalized expected LCS lengths is the binary Chvátal–Sankoff constant#✓fully proved

If the normalized expected LCS lengths converge to some real number as \(n \to \infty\), then they converge to the binary Chvátal–Sankoff constant \(C_{31a}\), which is defined as their limit inferior.

theorem tendsto_binaryChvatalSankoffConstant
    (h : chvatalSankoffLimitExists) :
    Filter.Tendsto normalizedExpectedLCS Filter.atTop
      (nhds binaryChvatalSankoffConstant)
Uses 3
Statement usesBinary Chvátal–Sankoff constant · Statement of the Chvátal–Sankoff limit theorem · Normalized expected LCS length

TheoremSuperadditivity implies the binary LCS limit exists#✓fully proved

For each natural number \(n\), let \(E_n\) be the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). If \(E_m + E_n \le E_{m+n}\) for all natural numbers \(m\) and \(n\), then the sequence \((E_n / n)_{n \ge 1}\) converges to a real number as \(n \to \infty\).

The proof applies Fekete's lemma.

theorem chvatalSankoffLimitExists_of_superadditive
    (h : ∀ m n : ℕ,
      expectedLCSLength m + expectedLCSLength n ≤ expectedLCSLength (m + n)) :
    chvatalSankoffLimitExists
Uses 4 · Used by 1
Statement usesStatement of the Chvátal–Sankoff limit theorem · Expected length of a longest common subsequence
Proof usesExpected LCS length is at most the string length · Normalized expected LCS length
Used byChvátal–Sankoff theorem: the binary LCS limit exists

TheoremThe binary Chvátal–Sankoff constant is nonnegative#✓fully proved

The binary Chvátal–Sankoff constant \(C_{31a}\) satisfies \(0 \le C_{31a}\).

theorem trivialLowerBound_holds : trivialLowerBound
Uses 3
Statement usesStatement of the trivial lower bound
Proof usesCatalogue notation for the binary Chvátal–Sankoff constant · Trivial bounds for the binary Chvátal–Sankoff constant

TheoremThe binary Chvátal–Sankoff constant is at most one#✓fully proved

The binary Chvátal–Sankoff constant \(C_{31a}\) satisfies \(C_{31a} \le 1\).

theorem trivialUpperBound_holds : trivialUpperBound
Uses 3
Statement usesTrivial upper bound for the binary Chvátal–Sankoff constant
Proof usesCatalogue notation for the binary Chvátal–Sankoff constant · Trivial bounds for the binary Chvátal–Sankoff constant

TheoremSuperadditivity of the expected LCS length#✓fully proved

Let \(E_n\) be the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). Then for all natural numbers \(m\) and \(n\), \(E_m + E_n \le E_{m+n}\).

theorem expectedLCSLength_superadditive :
    ∀ m n : ℕ,
      expectedLCSLength m + expectedLCSLength n ≤ expectedLCSLength (m + n)
Sources
  • adapted from the verified gpt-5.6-sol proof in task T292145496.
Uses 6 · Used by 1
Statement usesExpected length of a longest common subsequence
Proof usesBinary strings · Pairs of binary strings · Concatenation of binary string pairs · Length of a longest common subsequence · Superadditivity of the LCS length under concatenation
Used byChvátal–Sankoff theorem: the binary LCS limit exists

TheoremChvátal–Sankoff theorem: the binary LCS limit exists#✓fully proved

Let \(L_n\) be the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). Then the sequence \(\mathbb{E}[L_n]/n\) converges to a real number as \(n \to \infty\).

theorem chvatalSankoffLimitExists_holds : chvatalSankoffLimitExists
Uses 3
Statement usesStatement of the Chvátal–Sankoff limit theorem
Proof usesSuperadditivity implies the binary LCS limit exists · Superadditivity of the expected LCS length

TheoremDančík–Paterson upper bound for the binary Chvátal–Sankoff constant#●ready to prove

The binary Chvátal–Sankoff constant \(\gamma\) satisfies \(\gamma \le 0.837623\), where \(\gamma\) is the limit inferior, as \(n \to \infty\), of \(\mathbb{E}[L_n]/n\) and \(L_n\) is the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\).

theorem_wanted dancikPatersonUpperBound_wanted : dancikPatersonUpperBound
Sources
  • Dančík--Paterson (1995), catalogue upper bound 0.837623.
Uses 1
Statement usesStatement of the Dančík–Paterson upper bound

TheoremLueker's upper bound for the binary Chvátal–Sankoff constant#●ready to prove

The binary Chvátal–Sankoff constant \(C_{31a}\) is at most \(0.826280\).

theorem_wanted luekerUpperBound_wanted : luekerUpperBound
Sources
  • Lueker (2009), catalogue computer-assisted upper bound 0.826280.
Uses 1
Statement usesStatement of Lueker's upper bound

TheoremThe binary Chvátal–Sankoff constant is positive#●ready to prove

Let \(L_n\) be the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\). The binary Chvátal–Sankoff constant \(C_{31a} = \liminf_{n \to \infty} \mathbb{E}[L_n]/n\) satisfies \(C_{31a} > 0\).

theorem_wanted chvatalSankoffStrictPositive_wanted : chvatalSankoffStrictPositive
Sources
  • Chvátal--Sankoff (1975), catalogue strict lower bound > 0.
Uses 1
Statement usesStatement of the Chvátal–Sankoff positivity bound

TheoremDančík's lower bound for the binary Chvátal–Sankoff constant#●ready to prove

The binary Chvátal–Sankoff constant \(\gamma\) satisfies \(0.773911 \le \gamma\), where \(\gamma\) is the limit inferior, as \(n \to \infty\), of \(\mathbb{E}[L_n]/n\) and \(L_n\) is the length of a longest common subsequence of two independent uniformly random binary strings of length \(n\).

theorem_wanted dancikLowerBound_wanted : dancikLowerBound
Sources
  • Dančík (1994), catalogue computer-assisted lower bound 0.773911.
Uses 1
Statement usesStatement of Dančík's lower bound

TheoremLueker's lower bound for the binary Chvátal–Sankoff constant#●ready to prove

For each \(n\), let \(E_n\) be the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\), and let \(C\), the binary Chvátal–Sankoff constant, be the limit inferior of \(E_n / n\) as \(n \to \infty\). Then \(0.788071 \le C\).

theorem_wanted luekerLowerBound_wanted : luekerLowerBound
Sources
  • Lueker (2009), catalogue computer-assisted lower bound 0.788071.
Uses 1
Statement usesStatement of Lueker's lower bound

TheoremHeineman et al. lower bound for the binary Chvátal–Sankoff constant#●ready to prove

For each \(n\), let \(E_n\) be the expected length of a longest common subsequence of two independent uniformly random binary strings of length \(n\), and let \(C\), the binary Chvátal–Sankoff constant, be the limit inferior of \(E_n / n\) as \(n \to \infty\). Then \(0.792665992 \le C\).

theorem_wanted heinemanLowerBound_wanted : heinemanLowerBound
Sources
  • Heineman et al., arXiv:2407.10925v1 (2024), catalogue computer-assisted lower bound 0.792665992.
Uses 1
Statement usesStatement of the Heineman et al. lower bound
36 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.