Lean-verified proofs for [39]

Sergeev I. S. Formula complexity of a linear function in a k-ary basis. Mathematical Notes. 2021. 109(3), 445-458.

Basic facts for exponents, simple complexity bounds for the linear function (Proposition 1, Theorem 4(i)). LEAN

Bounds for exponents in the general case (Theorems 1, 2). LEAN (requires basic facts)

A lower bound for the exponent of the ternary unate basis (Theorem 3). LEAN (requires basic facts)

Lean-verified proofs were derived by an AI-assistant from text proofs in Reaslab environment.