Unfolding fan-in-two circuit outputs into Boolean formulas -- proof internals

theorem Complexity.BoolFormula.eval_negateIf_internal (assignment : ℕ → Bool) (negated : Bool) (formula : BoolFormula) : eval assignment (negateIf negated formula) = (negated ^^ eval assignment formula)

theorem Complexity.BoolFormula.depth_negateIf_le_internal (negated : Bool) (formula : BoolFormula) : (negateIf negated formula).depth ≤ formula.depth + 1

theorem Complexity.BoolFormula.depth_andOr_negateIf_le_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (formula₀ formula₁ : BoolFormula) : (match op with | AndOrOp.and => (negateIf negated₀ formula₀).conj (negateIf negated₁ formula₁) | AndOrOp.or => (negateIf negated₀ formula₀).disj (negateIf negated₁ formula₁)).depth ≤ 2 + max formula₀.depth formula₁.depth

theorem Complexity.Gate.eval_toBoolFormula_internal {W : ℕ} (gate : Gate Basis.andOr2 W) (wireFormula : Fin W → BoolFormula) (assignment : ℕ → Bool) : BoolFormula.eval assignment (gate.toBoolFormula wireFormula) = gate.eval fun (wire : Fin W) => BoolFormula.eval assignment (wireFormula wire)

theorem Complexity.Gate.depth_toBoolFormula_le_internal {W : ℕ} (gate : Gate Basis.andOr2 W) (wireFormula : Fin W → BoolFormula) : have input₀ := ⟨0, ⋯⟩; have input₁ := ⟨1, ⋯⟩; (gate.toBoolFormula wireFormula).depth ≤ 2 + max (wireFormula (gate.inputs input₀)).depth (wireFormula (gate.inputs input₁)).depth

theorem Complexity.Circuit.wireFormula_of_lt_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (wire : Fin (N + G)) (hinput : ↑wire < N) : circuit.wireFormula wire = BoolFormula.var ↑wire

theorem Complexity.Circuit.wireFormula_of_not_lt_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (wire : Fin (N + G)) (hinput : ¬↑wire < N) : circuit.wireFormula wire = (circuit.gates ⟨↑wire - N, ⋯⟩).toBoolFormula fun (source : Fin (N + G)) => circuit.wireFormula source

theorem Complexity.Circuit.wireDepth_of_not_lt_two_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (wire : Fin (N + G)) (hinput : ¬↑wire < N) : let gate := circuit.gates ⟨↑wire - N, ⋯⟩; have input₀ := ⟨0, ⋯⟩; have input₁ := ⟨1, ⋯⟩; circuit.wireDepth wire = 1 + max (circuit.wireDepth (gate.inputs input₀)) (circuit.wireDepth (gate.inputs input₁))

theorem Complexity.Circuit.outputDepth_two_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (output : Fin M) : let gate := circuit.outputs output; have input₀ := ⟨0, ⋯⟩; have input₁ := ⟨1, ⋯⟩; circuit.outputDepth output = 1 + max (circuit.wireDepth (gate.inputs input₀)) (circuit.wireDepth (gate.inputs input₁))

theorem Complexity.Circuit.eval_wireFormula_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (assignment : ℕ → Bool) (wire : Fin (N + G)) : BoolFormula.eval assignment (circuit.wireFormula wire) = circuit.wireValue (fun (input : Fin N) => assignment ↑input) wire

theorem Complexity.Circuit.eval_outputFormula_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (assignment : ℕ → Bool) (output : Fin M) : BoolFormula.eval assignment (circuit.outputFormula output) = circuit.eval (fun (input : Fin N) => assignment ↑input) output

theorem Complexity.Circuit.vars_wireFormula_lt_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (wire : Fin (N + G)) (index : ℕ) : index ∈ (circuit.wireFormula wire).vars → index < N

theorem Complexity.Circuit.vars_outputFormula_lt_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (output : Fin M) (index : ℕ) : index ∈ (circuit.outputFormula output).vars → index < N

theorem Complexity.Circuit.depth_wireFormula_le_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (wire : Fin (N + G)) : (circuit.wireFormula wire).depth ≤ 2 * circuit.wireDepth wire

theorem Complexity.Circuit.depth_outputFormula_le_outputDepth_internal {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (output : Fin M) : (circuit.outputFormula output).depth ≤ 2 * circuit.outputDepth output