I am looking for a direct proof (i.e. without going through ABPs) that if $f(\bar{x})$ has an arithmetic formula of size $s$ then it is a projection of an $O(s)\times O(s)$ determinant.
It seems possible using induction on $s$.
The basis, when $s=1,2,3$ is trivial.
Suppose we proved it for size $s$ formulas and let $f$ be a size $s+1$ formula.
If the root gate is a $\times$ gate with children $f_1,\cdots,f_k$, by induction we have that each $f_i$, which is also a formula, is a projection of a determinant of size $O(s_i)\times O(s_i)$, say $f_i=\text{det}(M_i)$.
So, if we construct a new matrix $M$ which is a block matrix with the $M_i$'s as its blocks and zeros elsewhere. Then $\text{det}(M)=\prod_{i=1}^k\text{det}(M_i)$ and the dimension of $M$ is $O(s_1)+\cdots+O(s_k)=O(s)$.
My problem is when the root is a $+$ gate.
