I have some questions on the previous question which is written bellow. Natural Proof and Constructivity : The topic of the previous questionRecently, Ryan Williams proved that Constructivity in Natural Proof is unavoidable to derive a separation of complexity classes : $\mathsf{NEXP}$ and $\mathsf{TC}^{0}$.   Constructivity in Natural Proof is a condition that all combinatorial proofs in circuit complexity satisfies and that we can decide whether the target function in $\mathsf{NEXP}$ (or another hard complexity classes) has a hard property by a algorithm that runs in poly-time in the length of target function's truth table.The other two conditions are: useless condition that require hard property can not be computed by any circuits in $\mathsf{TC}^0$ and largeness condition that the hard property is easy to find.References:* Ryan Williams, Natural Proofs Versus DerandomizationMy QuestionBreaking the largeness condition is formally stated as follows. There is a property such that $\mathop{Pr}_{f \leftarrow_{R} \{0,1\}^{2^{n}}} [f $ have the constructive property which is hard and useful against the class $\mathcal{C}] \leq \frac{o(2^{n})}{2^{2^{n}}}$If someone prove that the following statement , the statement have some meaning or shed light on this topic ?Statement:For some $f$, there exists  $n$-inputs circuit $C \in \mathcal{C}$ computing $f$ of size $m$ such that Circuit SAT on $C$ can be solved nontorivialy faster in the sence of the Ryan's technique, that is , $2^{n-l(m)}poly (m,n)$ giving a lower bound $2^{l(n)}$ against $NEXP$.I am not sure whether this question is a good one, because in the Ryan's methods, the circuit which is given as an instance of CKT-SAT is yield through proof by contradiction. That is, Ryan shows that if $NEXP \subseteq P/poly$ then there is a circuit as an compressed representation of witnesses and the exsistance of such circuit is derived through proof by contradiction using derandomization and $NEXP \subseteq P/poly \Rightarrow NEXP=EXP=MA$. I am not sure the property which circuits as a compressed representation of witnesses have and the function $f_{C}$ which circuits as a compressed representation computes.  If $f_{C}$ is very rare in the sence of largeness, can we break the largeness condition ?
Williams' Method, Natural Proofs and Constructivity
cc.complexity theory;complexity classes;circuit complexity;sat;natural proofs