I have some questions on the previous question which is written bellow.
Natural Proof and Constructivity : The topic of the previous question
Recently, 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 Derandomization"
My Question
Breaking 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 ?
