Circuit-family outputs as formula families -- proof internals

theorem Complexity.Circuit.depth_eq_outputDepth_zero_internal {N G : ℕ} [NeZero N] (circuit : Circuit Basis.andOr2 N 1 G) : circuit.depth = circuit.outputDepth 0

theorem Complexity.CircuitFamily.eval_outputFormulaFamily_internal (F : CircuitFamily Basis.andOr2) (n : ℕ) (assignment : ℕ → Bool) : BoolFormula.eval assignment (F.outputFormulaFamily n) = F.function n fun (input : Fin n) => assignment ↑input

theorem Complexity.CircuitFamily.depth_outputFormulaFamily_le_internal (F : CircuitFamily Basis.andOr2) (n : ℕ) : (F.outputFormulaFamily n).depth ≤ 2 * F.depth n

theorem Complexity.CircuitFamily.outputFormulaFamily_variables_lt_internal (F : CircuitFamily Basis.andOr2) (n index : ℕ) (hindex : index ∈ (F.outputFormulaFamily n).vars) : index < n

theorem Complexity.CircuitFamily.outputFormulaFamily_computes_internal {F : CircuitFamily Basis.andOr2} {f : BoolFunFamily} (hcomputes : F.Computes f) : F.outputFormulaFamily.ComputesOnTotalAssignments f.onTotalAssignments

theorem Complexity.CircuitFamily.outputFormulaFamily_logDepth_internal {F : CircuitFamily Basis.andOr2} {c : ℕ} (hdepth : F.DepthBoundedBy fun (n : ℕ) => c * Nat.log 2 n + c) : F.outputFormulaFamily.LogDepth

theorem Complexity.NC1_onTotalAssignments_subset_FormulaNC1OnTotalAssignments_internal : BoolFunFamily.onTotalAssignments '' NC1 ⊆ FormulaNC1OnTotalAssignments