Uniform polynomial time for the hard language and its balanced padding

Apply the finite-alphabet simulator to the source's explicit decider, then use the existing P verdict characterization and balanced-padding FP closure.

theorem Complexity.DepthThreeLowerBound.language_mem_P_proof : {w : List Bool | language w = true} ∈ P

theorem Complexity.DepthThreeLowerBound.language_eval_mem_FP_proof : (fun (w : List Bool) => [language w]) ∈ FP

theorem Complexity.DepthThreeLowerBound.balancedLanguage_mem_P_proof : {w : List Bool | balancedLanguage w = true} ∈ P

theorem Complexity.DepthThreeLowerBound.exists_balanced_language_in_P_depth_three_lower_bound_proof : ∃ (L : List Bool → Bool), {w : List Bool | L w = true} ∈ P ∧ (∀ (n : ℕ), {x : Cube (Fin (n + 1)) | L (List.ofFn x) = true}.card = 2 ^ n) ∧ ∀ (A : ℝ), 0 < A → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (D : Circuit3 (Fin (n + 1))), ((D.Computes fun (x : Cube (Fin (n + 1))) => L (List.ofFn x)) ∨ D.ComputesDual fun (x : Cube (Fin (n + 1))) => L (List.ofFn x)) → 2 ^ (A * √↑(n + 1)) < ↑D.gateCount