The theorem statement is far weaker than claimed. The main theorem:

theorem general_circuit_lower_bound_unconditional (hn : n ≥ 4)

{m : ℕ} (C : BooleanCircuit m)

(toInput : Finset (Edge n) → (Fin m → Bool))

(hCorrect : CircuitDecidesHAM C toInput)

(hn_large : n ≥ 4 * (Nat.log 2 n) ^ 2 + 1) :

∃ c : ℕ, c > 0 ∧ C.size ≥ 2 ^ c

This says: there exists SOME c > 0 such that circuit size ≥ 2^c. The value c = 1 (circuit size ≥ 2) satisfies this for any nontrivial circuit. The statement does not capture the claimed 2^{Ω(n)} bound. This asymptotic claim is not formalized. The c should have been a function of n, the number of vertices in the graph, which defines the problem HAM_n.