What is the proof for why border adjustments are exactly offset in theory by currency appreciation? Why is it true, in theory, that border adjustments are exactly offset by currency appreciation? I've read the colloquial explanations online, but am looking for something more rigorous. 

For example, http://taxfoundation.org/blog/exchange-rates-and-border-adjustment says that 


  Standard economic theory states that a border adjustment ends up in a wash for both exporters and importers because prices adjust to leave the trade balance unchanged. Specifically, the value of the domestic currency adjusts upward. Standard supply and demand shows why both the import tax and the export exemption work together to push the value of the domestic currency up.
Here is a reference by Feldstein, Krugman that is often quoted when discussing the FX neutrality of border tax adjustments: 
http://www.nber.org/chapters/c7211.pdf

Another useful reference that takes a somewhat skeptical view and lists more references is 
http://voxeu.org/article/exchange-rate-implications-border-tax-adjustment-neutrality. All models developed or mentioned in these references are non-monetary models, i.e. changes in the exchange rates 

I have not digested these references completely yet. However, my understanding of the basic argument is as follows:

In present value terms exports must always equals imports. Changes to taxation may disturb this equilibrium which may then lead to an adjustment of the exchange rate. However, in a world with inelastic labor supply as assumed by Feldstein/Krugman a VAT with border tax adjustments does not have any distortive effects as it changes neither the consumption/savings decision, nor the present value of imports or exports it will not have any real effects. 

In principle already from this result one can conclude that border tax adjustments that limit any tax impact on domestic economic agents cannot change any consumption or production decisions as long as the economy is small, labor supply is inelastic and tax revenue is redistributed in a lump sump fashion.

However, a more rigorous argument is as follows:

With inelastic labor supply, households have to decide on their consumption and savings. The first order condition resulting from a standard intertemporal optimization model is (following Feldstein, Krugman)

${U_C}_1/(\delta{U_C}_2)=(1+r)p_1/p_2$

This condition shows that the consumption/savings decision changes only when relative prices or interest rates change. 

Consider now various types of firms underlying Auerbach's border tax adjustments, where we again model the firm as in Feldstein, Krugman:


Exporting firms


$maxV=p_X X^1+(1-\tau)(p_D^1 D^1-w^1l^1-p_D^1k^2)+[p_X X^2+(1-\tau)(p_D^2 D^2-w^2l^2)]/(1+r)$

subject to

$Q^1(l^1)=X^1+D^1$ and $Q^2(l^2;k^2)=X^2+D^2$

Where D denotes domestic and X denotes export sales.
Labor market equilibrium is given by

$\bar L=l^1$  and  $\bar L =l^2$

Equilibrium conditions are in the first period

$p_D^1=p_X/(1-\tau)$; $w^1=p_X/(1-\tau)Q_l^1(\bar L)$

From this follows that in the first period and increase in $\tau$ leads to a proportional increase in $p_D^1$ and $w$. This means essentially that the exchange rate will adjust to neutralize the impact of $\tau$.

These conclusions can be shown to hold also in period 2, where there is one additional equilibrium condition $1=Q_k^2(\bar L,k^2)$.


Exporting firms importing an intermediate good


$$maxV=p_X X^1+(1-\tau)(p_D^1 D^1-w^1l^1-p_D^1k^2)-p_m^1m^1+\frac{p_X X^2+(1-\tau)(p_D^2 D^2-w^2l^2)-p_m^2m}{1+r}$$
subject to
$Q^1(l^1;m^1)=X^1+D^1$ and $Q^2(l^2;m^2;k^2)=X^2+D^2.$

Compared to 1. there is one additional equilibrium condition in period 1: $p_m^1/p_X=Q_m^1(l^1;m^1)$ and one in period 2 $p_m^2/p_X=Q_m^2(l^2;m^2;k^2)$.  However, also these addtional equilibrium conditions do not change the overall conclusion that changes in $\tau$ will only impact $p_D$ and $w$.

These conclusions also hold in a more general context, for instance, if there are importing firms producing nontradeable goods.