Internal: Schnorr bridge from descriptors to typed circuits

This module transports the descriptor-level gate-elimination theorem to the typed fan-in-two circuit model.

theorem Complexity.schnorr_lower_bound_circuit_internal (N G : ℕ) [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (comp : Bool) (heval : ∀ (x : BitString N), c.eval x 0 = (comp ^^ Schnorr.xorBool N x)) (hN : 1 ≤ N) : G + 2 ≥ 2 * N

Internal Schnorr lower bound transported to typed circuits.