Kernel-checked Lean 4 certificates for finite constructions: optimization constants 1a, 1c, 1d and 49, Ramsey colourings, covering designs and binary codes

Kernel-checked Lean 4 proofs of bounds and properties of explicit finite constructions: the autocorrelation constant C1a, the signed constant C1d, replays of tracker entries 1c, 1d and 49, seven two-colourings of complete graphs, forty covering designs and thirty-one binary linear codes. Every input is identified by URL, commit and SHA-256.