Certified upper bounds for the Chvátal–Sankoff constant

Let γ2 be the Chvátal–Sankoff constant, so that the expected length of a longest common subsequence of two independent uniformly random binary strings of length n is γ2n + o(n). Lueker proved γ2 ≤ 0.826280 with a finite automaton that reads a pair of strings as a sequence of minimal match pairs and remembers the last h symbols of each string, for h = 8. We carry out his method up to h = 13 and prove γ2 ≤ 0.821963. For h = 13 the certificate lists 165,695,219,469 states of the automaton, reduced by a symmetry. The bound rests on an explicit positive vector for the weighted transition matrix of the automaton; a checker rebuilds every transition with its own code and verifies the required inequalities in exact integer arithmetic. We also give a complete proof that the automaton accepts the truncated canonical decomposition of every pair of strings, the property on which the method depends. The weaker bound γ2 ≤ 0.822579 for h = 12 is also proved in the Lean 4 proof assistant, with a computation evaluated by compiled code, and the bounds γ2 ≤ 0.825101, γ2 ≤ 0.824120 and γ2 ≤ 0.823290 for h = 9, 10 and 11 by formal proofs that are checked entirely by the Lean kernel. The programs, the Lean proofs and the logs are available at github.com/tejasvi/chvatal-sankoff-certificates-v4; they and the certificates for h = 8 to 11 are archived at doi:10.5281/zenodo.23562700.