It is known that the minimum size of $U_2$-circuits computing the parity function exactly equals $3(n-1)$. The lower bound proof is based on the gate elimination method.
Recently, I noticed that the gate elimination method works well also for nondeterministic $U_2$-circuits, and we can prove a $3(n-1)$ lower bound for the size of nondeterministic $U_2$-circuits computing the parity function.
(It means that nondeterministic computation is useless to compute parity by $U_2$-circuits and cannot reduce the size from $3(n-1)$. Thus, the minimum circuits don't change from the deterministic case.)
My questions are the following two:
(1) Is this a new result or a known result?
(2) More generally, are there some known results of lower bounds for the size of nondeterministic circuits (including formulas, constant depth circuits, and so on) with unlimited nondeterministic input bits (or, in other words, unlimited nondeterminism) for an explicit function?
Additional explanation (Nov 27, 2014)
In the second question, I intended that I would like to know especially whether this is the first nontrivial lower bound for the size of nondeterministic circuits (including formulas, constant depth circuits, and so on) with unlimited nondeterminism for an explicit function or not. I know there are some results if nondeterminism is limited, as follows.
[1] Hartmut Klauck: Lower Bounds for Computation with Limited Nondeterminism. IEEE Conference on Computational Complexity 1998: 141-
[2] Vikraman Arvind, K. V. Subrahmanyam, N. V. Vinodchandran: The Query Complexity of Program Checking by Constant-Depth Circuits. ISAAC 1999: 123-132