Expected ranks and determinantal regular sequences force a free complex to be exact

First verify that $I_i\mathrm{\ne }0$ for every $i$. If $I_i=R$ this is clear, including the $r_i=0$ convention where the $0$-minor is $1$. Otherwise it contains a regular sequence of positive length, whose first member is a nonzerodivisor on the nonzero ring $R$. Thus an $r_i$-minor is nonzero. Since all larger minors vanish, $d_i$ has rank exactly $r_i$.

If a matrix entry of some $d_k$ is a unit, [F1] splits an identity pair in degrees $k,k-1$. In the complement the expected rank at $k$ is $r_k-1$ and all other expected ranks remain $r_i$. The determinant identity for a block $1\oplus D$ gives $I_{r_k}(1\oplus D)=I_{r_k-1}(D)$ and $I_{r_k+1}(1\oplus D)=I_{r_k}(D)$; minors at other differentials are unchanged because the removed rows or columns there are zero. Therefore the complement satisfies the same hypotheses. Repeat finitely many times, since each split reduces the sum of all ranks. It suffices to prove exactness for a complex whose differential entries all lie in $\mathfrak{m}$; call this the minimal complex.

If the minimal complex has no positive-degree term, it is exact there. Otherwise let $t>0$ be its highest nonzero degree. Its expected rank is $r_t=n_t>0$, and $I_t\subseteq \mathfrak{m}$ because all entries of $d_t$ lie in $\mathfrak{m}$. By hypothesis $I_t$ contains a regular sequence of length $t$, so $\mathrm{depth}R\ge t$. Every nonzero free term of the minimal complex has this same depth; therefore $\mathrm{depth}{F}_j\ge j$ for every $j$. By [F3], $\dim R\ge t$. In particular if $\dim R=0$, there is no positive term and the complex is exact.

Induct on the finite integer $d=\dim R$; finiteness follows from the Noetherian maximal ideal and the height theorem [F3]. Assume $d>0$ and exactness for complexes with the stated hypotheses over all Noetherian local rings of dimension less than $d$. Let $\mathfrak{p}⊊\mathfrak{m}$. The localized complex over $R_{\mathfrak{p}}$ retains vanishing of all larger minors. If $(I_i{)}_{\mathfrak{p}}$ is unit, its alternative holds. Otherwise every element of a chosen regular sequence in $I_i$ belongs to $\mathfrak{p}$, and [F3] preserves its regularity after localization, including a nonzero terminal quotient. Thus each localized determinantal ideal satisfies the alternative. The ideal is nonzero by the localized regular sequence or unit condition, so the expected-rank equality persists. Because $\mathfrak{p}⊊\mathfrak{m}$, $\dim R_{\mathfrak{p}}<d$; the induction hypothesis makes the localized complex exact in positive degrees.

Each positive homology module $H_i$ of the minimal complex is finite over $R$ and vanishes after localization at every nonmaximal prime by step 3.1. Thus its support is contained in $\{\mathfrak{m}\}$. By [F4], $\sqrt{\mathrm{Ann}{H}_i}=\mathfrak{m}$ when $H_i\mathrm{\ne }0$. If $\mathfrak{m}=(x_1,\dots ,x_s)$, powers of all $x_a$ kill $H_i$; a sufficiently large power ${\mathfrak{m}}^N$ therefore kills it. The finite filtration by ${\mathfrak{m}}^j{H}_i$ has quotients finite-dimensional over $R\mathrm{/}\mathfrak{m}$, so $H_i$ has finite length. If any positive $H_i$ were nonzero, choose the largest such $i$. Step 2.1 supplies the depth bounds for the complex, while [F2] says this highest homology has depth at least one. A nonzero finite-length module has depth zero, contradiction. Hence the minimal complex is positively exact, and reattaching the contractible pairs from step 1.2 proves the original complex exact.

The dimension-zero base and positive-dimension induction complete the proof. AC is inherited by the regular-sequence, depth, and support suppliers; the unit-pair splitting itself is finite and choice-free.