By induction on $l$, this is immediately reduced to the case $l=1$. We may assume that $\pr_{\tilde 1} \rest f(U)$ is injective and $\bm U^{\flat}$ is an elementary blowup in the first coordinate. If $\bm U \in \mRV[k]$ then it is enough to construct a focus map into the first coordinate with locus $f(U)^\sharp$; this can be easily done, using once again the fact that every definable set contains a definable point (see Remark <ref>). If $\bm U \in \mRV^{\db}[k]$ then the aperture $(\tau, t)$ of $\bm U^{\flat}$ needs to be factored into the construction. Fix a definable point $c \in t^\sharp$. For $u \in U$ and $a \in  f(u)_{\tilde 1}^\sharp$, the $\RV$-disc $f(u)_{1}^\sharp$ contains an $a$-definable point $b_a$; moreover, by Lemma <ref>, these points may be chosen uniformly via a differentiable function. Thus there is a continuous (fiberwise) additive translation, with respect to the points $b_a$ and $b_a - c b_a$, between the two sets in question, which is proper covariant by Lemma <ref>.

§.§ Standard contractions

Suppose that $A \sub \VF^{n} \times \RV^{m}$ is an invariant set. Let $i \in [n]$ and $T_i$ be a definable bijection on $A$,  relatively special covariant in the $i$th $\VF$-coordinate, such that for every $a \in \pr_{\tilde i}(A)$, the set $T_i(A_a)$ is an $\RV$-pullback. Moreover, if $A$ is proper invariant then $T_i$ is continuous and proper covariant. Note that $T_i$ is not necessarily a special covariant bijection since, to begin with,  the various special covariant bijections in the $i$th $\VF$-coordinate  may not even be of the same length. Let

\[
A_i = \bigcup_{a \in \pr_{\tilde i}(A)} a \times (T_i(A_a))_{\RV} \sub \VF^{n-1} \times \RV^{m_i}.
\]

Let $\hat T_i : A \fun A_i$ be the function induced by $T_i$. If $A$ is proper invariant then $A_i$ is proper invariant too, which is not guaranteed if we do not demand $T_i$ to be proper covariant (continuity is needed for other reasons, see Definition <ref> and the proof of Lemma <ref> below).

For any $j \in [n{-}1]$, we repeat the above procedure on $A_i$ with respect to the $j$th $\VF$-coordinate and thereby obtain a set $A_{j} \sub \VF^{n-2} \times \RV^{m_j}$ and a function $\hat T_{j} : A_i \fun A_{j}$. The relatively special covariant bijection on $T_i(A)$ induced by $\hat T_{j}$ is denoted by $T_j$. Continuing thus, we obtain a sequence of  bijections $T_{\sigma(1)}, \ldots, T_{\sigma(n)}$ and a corresponding function $\hat T_{\sigma} : A \fun \RV^{l}$, where $\sigma$ is the permutation of $[n]$ in question. The composition $T_{\sigma(n)} \circ \ldots \circ T_{\sigma(1)}$, which is referred to as the lift of $\hat T_{\sigma}$, is denoted by $T_{\sigma}$.

Suppose that there is a $k \in 0 \cup [m]$ such that  $(A_a)_{\leq k} \in \RV[k]$  for  every $a \in A_{\VF}$. In particular, if $k=0$ then $A \in \VF_*$. By Lemma <ref>, $\hat T_{\sigma}(A)_{\leq n+k}$ is an object of $\RV[{\leq} l{+}k]$, where $\dim_{\VF}(A) = l$, or even an object of $\RV^{\db}[n{+}k]$ if $A$ is proper invariant.

The function $\hat T_{\sigma}$, or the object $\hat T_{\sigma}(A)_{\leq n+k}$, is referred to as a standard contraction of the invariant set $A$ with the head start $k$.

Suppose that $\omega : A \fun \RV$ is a definable function, proper covariant if $A$ is proper invariant, and $\hat T_{\sigma}$ is a standard contraction of $A_\omega$ (recall Notation <ref>). Let $\hat T^\omega_{\sigma}(A)_{\leq n+k}$ be the $(n+k)$th component of $\hat T_{\sigma}(A_\omega)_{\leq n+k}$, which is not the empty object if and only if $\dim_{\VF}(A) = n$.  The definable function on $\hat T^\omega_{\sigma}(A)_{\leq n+k}$ induced by $\omega$ is denoted by $\omega_{\hat T_{\sigma}}$. The function $\hat T_{\sigma}$, or the object

\[
\hat T_{\sigma}(\bm A)_{\leq n+k} \coloneqq (\hat T^\omega_{\sigma}(A), \omega_{\hat T_{\sigma}})_{\leq n+k},
\]

is referred to as a standard contraction of the pair $\bm A = (A, \omega)$.

Let $A^\sharp = \bigcup_{a \in A_{\VF}} a \times \bb L (A_a)_{\leq k}$, which is an object of $\VF_*$. The volume form on $A^\sharp$ induced by $\omega$ is still denoted by $\omega$. The  bijection $A^\sharp_\omega \fun \mathbb{L} \hat T_{\sigma}(A_\omega)_{\leq n+k}$ induced by $T_{\sigma}$, which is still denoted by $T_{\sigma}$, is indeed a $\mVF[n{+}k]$-morphism or a $\mVF^{\diamond}[n{+}k]$-morphism if $(A, \omega)$ is proper invariant.

The head start of a standard contraction is usually implicit. In fact, it is always $0$ except in Lemma <ref>, and can be circumvented even there. This seemingly needless gadget only serves to make the above definition more streamlined: If $A \in \VF_*$ then the intermediate steps of a standard contraction of $A$ may or may not result in objects of $\VF_*$ and hence the definition cannot be formulated entirely within $\VF_*$.

By Remark <ref> and compactness, every pseudo invariant pair $(A, \omega)$ of the above form admits a standard contraction with respect to any permutation $\sigma$ of $[n]$ and any head start $k \in [m]$. This also holds for the other case:

If $(A, \omega)$ is proper invariant then it also admits such a standard contraction.

Before we start the proof, first observe that $(A, \omega)$ may be viewed as the obvious intermediate result of a  standard contraction of $(A^\sharp, \omega) \in \mVF^{\diamond}[n{+}k]$. Thus we may and do assume $k=0$, that is, $A \in \VF_*$.

We do induction on $n$. The base case $n=1$ follows from Remark <ref>. For the inductive step, we may assume $\sigma = \id$ and, by compactness, $\omega = 1$. By the inductive hypothesis and compactness again,  there is a definable bijection $T$ on $A$ such that, for every $a \in A' \coloneqq \pr_n(A) \sub \VF$, the induced bijection $T_a$ on $A_a$ is the lift of a standard contraction $\hat T_a$ of $A_a$; in particular, $T$ may be written as a composition of relatively proper special covariant bijections $T_i : A_{i-1} \fun A_{i}$. Note that each $T^{-1}_i$ is $\rv$-contractible.

Suppose that $A$ is proper $\delta$-invariant. Let $\ga$ range over open discs of radius $\delta$ contained in $A'$. Applying Lemma <ref> in the $n$th $\VF$-coordinate as in the proof of Proposition <ref>, we deduce that over all but finitely many definable open discs $\ga$, the $\RV$-data of $T_a$ is constant over $\ga$; it will become clear what $\RV$-data is actually needed below. By FMT (Terminology <ref>), we may assume that there are no exceptional discs and in light of Lemma <ref>,  every $T_i$ is continuous.

By the constancy of $\RV$-data over each $\ga$  and Lemma <ref>, the $\VF$-coordinates of $A_i$  are bounded and the $\RV$-coordinates of $A_i$ are doubly bounded. Pulling back open polydiscs of the form $\ga \times \gp$ along $T^{-1}$, where  $\gp$ is an $\RV$-polydisc, we see that every $\VF$-fiber of $A_i$ is a union  of open polydiscs of the form $\gb \times \gq$, where $\gb \sub \ga$ for some $\ga$ and the radius of $\gq$ only depends on $\ga$ and the $\VF$-fiber in question. These open discs $\gb$ may be taken to be maximal in the obvious sense and hence form an $\go$-partition. By Lemma <ref>, we conclude that each $A_i$ is indeed proper invariant. Then, by Lemma <ref>, every $T_i$ is proper covariant. Finally, applying Remark <ref> to the set $\bigcup_{a \in A'} a \times \hat T_a(A_a)$, the lemma follows.

We remark that  standard contractions bear marked similarities to special covariant bijections and may indeed be used to deduce, say, Lemma <ref>, etc.

Suppose that $[(A, \omega)] = [(B, \sigma)]$ in $\gsk \mVF[1]$ (respectively,  $\gsk \mVF^{\diamond}[1]$). Let $(\bm U, \omega')$, $(\bm V, \sigma')$ be, respectively, standard contractions of $(A, \omega)$, $(B, \sigma)$ in $\mRV[1]$ (respectively,  $\mRV^{\db}[1]$). Then

\[
([(\bm U, \omega')], [(\bm V, \sigma')]) \in \misp \quad (\text{respectively, } \mispdb).
\]

Let $F: (A, \omega) \fun (B, \sigma)$ be a $\mVF[1]$-morphism. The essential bijection $\bb L \bm U \fun \bb L \bm V$ induced by $F$ is denoted by $F'$. Let $A' = \dom(F')$ and $B' = \ran(F')$. By Lemma <ref>, deleting finitely many points from $A'$, $B'$ if necessary, we may assume that there are special bijections $T$, $R$ on $\bb L \bm U$, $\bb L \bm V$ such that $A'^{\flat}$, $B'^{\flat}$ are $\RV$-pullbacks and $F'^{\flat}_{\downarrow}$ is an $\RV[1]$-morphism

\[
\bm A' \coloneqq (A'^{\flat}_{\RV})_1 \fun \bm B' \coloneqq (B'^{\flat}_{\RV})_1.
\]

By Lemma <ref>, $(\bm A', \omega'_T)$, $(\bm B', \sigma'_R)$ are isomorphic to blowups of $(\bm U, \omega')$, $(\bm V, \sigma')$, respectively. By Lemma <ref>, the bijection $F'^{\flat}_{\downarrow}$ is indeed a $\mRV[1]$-morphism $(\bm A', \omega'_T) \fun (\bm B', \sigma'_R)$ except at finitely many points (the condition involving $\jcb_{\Gamma}$ might fail). At this stage, without loss of generality, we may retroactively assume that $A'$, $B'$ are of the forms $t^\sharp$, $s^\sharp$, where $t, s \in \RV$, and $T$, $R$ are both centripetal transformations, and $F'$ has dtdp (after deleting finitely many points again, see  Lemma <ref> and the proof of <cit.> for more details). Since the volume forms $\omega'_T$, $\sigma'_R$ are constant, by -minimality in the $\K$-sort and Lemma <ref> again, we must have that $F'^{\flat}_{\downarrow}$ is differentiable everywhere and indeed,  for all $u \in \rv(A'^{\flat})$ and all $a \in u^\sharp$,

\[
\rv(\jcb_{\VF} F'^{\flat}( a)) = \jcb_{\RV} F'^{\flat}_{\downarrow}(u) = \omega'_T / \sigma'_R.
\]

It follows that $F'^{\flat}_{\downarrow}$ is a $\mRV[1]$-morphism.

The argument above also works for the other case. Note that  $F$ and hence $F'$ are then already  bijections. Also, we are not free to delete finitely many points to enforce dtdp. Instead, Lemma <ref> is applied as in the proof of Lemma <ref> to ensure that the condition involving $\jcb_{\Gamma}$ holds at these exceptional points.

Let $A'$, $A''$ be definable sets with $A'_{\VF} = A''_{\VF} \eqqcolon A \sub \VF^n$ and $\omega'$, $\omega''$ definable functions from $A'$, $A''$ into $\RV$, respectively. Write $\bm A' = (A', \omega')$ and $\bm A'' = (A'', \omega'')$. Suppose that there is a $k \in \N$ such that for  every $a \in A$,

\begin{equation}\label{condi:fiber}
([(A'_a, \omega')]_{\leq k}, [(A''_a, \omega'')]_{\leq k}) \in \misp.
\end{equation}

Let $\hat T_{\sigma}$, $\hat R_{\sigma}$ be standard contractions of $\bm A'$, $\bm A''$, respectively. Then

\[
([\hat T_{\sigma}(\bm A')]_{\leq n+k}, [\hat R_{\sigma}(\bm A'')]_{\leq n+k}) \in \misp.
\]

If $\bm A'$, $\bm A''$ are proper invariant then the same holds with respect to $\mispdb$.

Note that condition (<ref>) makes sense only  over the substructure $\mdl S \la a \ra$.

By induction on $n$, this is immediately reduced to the case $n=1$. So assume $A \sub \VF$. After replacing $A'$, $A''$ with $A'_{\omega'}$, $A''_{\omega''}$, we see that the special bijection $F : A \fun A^\sharp$ constructed in the proof of <cit.> also satisfies the condition that for all $\RV$-polydisc $\gp \sub A^{\sharp}$ and all $a_1, a_2 \in F^{-1}(\gp)$,

\[
\omega' \rest A'_{a_1} = \omega' \rest A'_{a_2} \dand \omega'' \rest A''_{a_1} = \omega'' \rest A''_{a_2}.
\]

Therefore, using Lemma <ref> in place of <cit.>, that proof goes through here with virtually no changes (the additional computations involving $\jcb_{\RV}$ and $\jcb_{\Gamma}$ are all straightforward).

The second claim is similar, except that $F$ must be a proper special covariant bijection with a sufficiently large aperture. As before, this may be taken care of by  FMT (also see the discussion in Remark <ref>) .

Let $\bm A'$, $\bm A''$ be as above with $k=0$, and suppose that there is a morphism $F : \bm A' \fun \bm A''$ that is relatively unary in the $i$th $\VF$-coordinate. Then for any permutation $\sigma$ of $[n]$ with $\sigma(1) = i$ and any standard contractions $\hat T_{\sigma}$, $\hat R_{\sigma}$ of $\bm A'$, $\bm A''$,

\[
([\hat T_{\sigma}(\bm A')]_{\leq n}, [\hat R_{\sigma}(\bm A'')]_{\leq n}) \in \misp \quad (\text{respectively, } \mispdb).
\]

First suppose that $F$ is a $\mVF[n]$-morphism. Note that since $F$ is partially differentiable outside a definable subset of $\VF$-dimension less than $n$, it may not induce a morphism $\bm A'_a \fun \bm A''_a$ for every $a \in \pr_{\tilde i}(A)$. By Lemma <ref>, there is a standard contraction $\hat T'_{\sigma}$ of $\bm A'$ such that the subset of $A'$ that corresponds to $\hat T'_{\sigma}(\bm A')_{\leq n}$ via $T'_{\sigma}$ is contained in the partial differential locus of $F$. Thus, by Lemma <ref>, we may assume that $F$ is indeed differentiable. But then the claim follows immediately from Lemmas <ref> and <ref>.

If $F$ is a $\mVF^{\diamond}[n]$-morphism then there is a $\delta \in \absG^+$ such that $A'$ and $\hat T_{\sigma(1)}(A')$ are both $\delta$-invariant. This means that for all $a \in \pr_{\tilde i}(A)$ there is a $b \in \pr_{\tilde i}(A)$ such that they are contained in the same open polydisc of radius $\delta$, $F$ induces a morphism $\bm A'_b \fun \bm A''_b$, and $\hat T_{\sigma(1)}(A')_a = \hat T_{\sigma(1)}(A')_b$. Thus the claim follows immediately from Lemmas <ref> and <ref> again.

Let $\ga$ be an open disc and $f : \ga \fun \VF$ an injection.
We say that $f$ is $\vv$-affine if there is a (necessarily unique) $\gamma \in \Gamma$, called the shift of $f$, such that, for all $a, a' \in \ga$,

\[
\abval(f(a) - f(a')) = \gamma + \abval(a - a').
\]

We say that $f$ is $\rv$-affine if there is a (necessarily unique) $t \in \RV$, called the slope of $f$, such that, for all $a, a' \in \ga$,

\[
\rv(f(a) - f(a')) = t \rv(a - a').
\]

Let $A \sub \VF^2$ be a definable set such that $\ga_1 \coloneqq \pr_1(A)$ and $\ga_2 \coloneqq \pr_2(A)$ are both open discs. Let $f : \ga_1 \fun \ga_2$ be a definable bijection that has dtdp.  We say that $f$ is balanced in $A$ if $f$ is actually $\rv$-affine and there are $t_1, t_2 \in \RVV$, called the paradigms of $f$, such that, for every $a \in \ga_1$,

\[
A_a = t_2^\sharp + f(a) \dand f^{-1}(A_a) = a - t_1^\sharp.
\]

We say that a set $A$ is a $1$-cell if it is either an open disc contained in a single $\RV$-disc or a point in $\VF$. We say
that $A$ is a $2$-cell if

* $A$ is a subset of $\VF^2$ contained in a single $\RV$-polydisc and $\pr_1(A)$ is a $1$-cell,

* there is a function $\epsilon : A_1 \coloneqq \pr_1 (A) \fun \VF$ and a $t \in \RV$ such that, for every $a \in A_1$, $A_a = t^\sharp + \epsilon(a)$,

* one of the following three possibilities occurs:

* $\epsilon$ is constant,

* $\epsilon$ is injective, has dtdp, and $\rad(\epsilon(A_1)) \geq \abs{\vrv(t)}$,

* $\epsilon$ is balanced in $A$.

The function $\epsilon$ is called the positioning function of $A$ and the element $t$ the paradigm of $A$.

More generally, a set $A$ with exactly one $\VF$-coordinate is a $1$-cell if, for each $t \in A_{\RV}$, $A_t$ is a $1$-cell in the above sense; the parameterized version of the notion of a $2$-cell is formulated in the same way.

Let  $A \sub \VF^2$ be an invariant set. Then there is a standard contraction $\hat T_\sigma$ of $A$ such that $A_s$ is a $2$-cell for every $s \in \hat T_\sigma(A)$.

This is just <cit.> if $A$ is pseudo invariant, even though it is not exactly stated in this form. The proof of <cit.> proceeds by constructing a positioning function $\epsilon_{(t,s)}$ in each $\VF$-fiber, which heavily relies on the use of standard contractions in the preceding auxiliary results, namely <cit.>.  It is not hard to see that if $A$ is proper invariant  then that proof still goes through, provided that FMT is applied at suitable places to cut out finitely many exceptional open discs in the first coordinate at which the desired properties of $\epsilon_{(t,s)}$ do not hold, as we have done above, say, in the proof of Lemma <ref>.

We also remark that Lemma <ref> holds fiberwise for invariant sets $A \sub \VF^n$ with $n \geq 2$, that is, there is a standard contraction $\hat T_\sigma$ of $A$ such that for every $(a, s) \in \hat T_{\sigma(2)}(A)$, $\hat T_{\sigma(2)}^{-1}(a, s)$ is of the form $a \times C$, where $C$ is a $2$-cell. This is immediate by compactness if $A$ is pseudo invariant. If $A$ is proper invariant then it follows from Lemma <ref> and the construction in the proof of  Lemma <ref> (Lemma <ref> serves as the base case and hence, in the inductive step, we can assume that $\hat T_{\sigma(2)}$ is already as desired fiberwise).

From now on, the pain of treating two cases (pseudo versus proper) in parallel is over, as the proofs will be formal and work for either one.

For the next two lemmas, let $12$, $21$ denote the permutations of $[2]$ and $\bm A = (A, \omega)$ be an object of either $\mVF[2]$ or $\mVF^\diamond[2]$.

Suppose that $A \sub \VF^2$ is a $2$-cell and $\omega$ is constant. Then there are standard contractions $\hat T_{12}$, $\hat R_{21}$ of $\bm A$ such that $[\hat T_{12}(\bm A)]_{\leq 2} = [\hat R_{21}(\bm A)]_{\leq 2}$.

We may of course assume $\dim_{\VF}(A) = 2$. All we need to do is to check that the maps constructed in the proof of  <cit.> are indeed $\mRV[2]$- or $\mRV^{\db}[2]$-morphisms. By inspection of that proof, we see that there are two cases: $A$ is a product of two open discs or the positioning function $\epsilon$ in question is balanced in $A$ with nonzero paradigms $t_1$, $t_2$. The first case is obvious since we can simply use the identity map. In the second case, observe that there is no requirement on $\jcb_{\RV}$ since the resulting standard contractions are of $\RV$-dimension $1$. On the other hand, a morphism between the standard contractions can be easily constructed using  $\epsilon$  (we could also cite Lemma <ref>, but the situation here is much simpler), and  the requirement on $\jcb_{\Gamma}$ is satisfied since the slope of the $\rv$-affine function $\epsilon$ is $-t_2/t_1$ (see the last paragraph of <cit.> for further explanation).

There are a morphism $\bm A \fun \bm A^*$, relatively unary in both coordinates, and two standard contractions $\hat T_{12}$, $\hat R_{21}$ of $\bm A^*$ such that $[\hat T_{12}(\bm A^*)]_{\leq 2} = [\hat R_{21}(\bm A^*)]_{\leq 2}$.

This follows from  Lemmas <ref>, <ref>, and compactness (see the proof of <cit.> for a bit more details).

Let $\bm A = (A, \omega)$ be an object of $\mVF[n]$ (respectively, $\mVF^\diamond[n]$). Suppose that $i, j \in [n]$ are distinct and $\sigma_1$, $\sigma_2$ are  permutations of $[n]$ such that

\[
\sigma_1(1) = \sigma_2(2) = i, \quad \sigma_1(2) = \sigma_2(1) = j, \quad \sigma_1
\rest \set{3, \ldots, n} = \sigma_2 \rest \set{3, \ldots, n}.
\]

Then, for any standard contractions $\hat T_{\sigma_1}$, $\hat T_{\sigma_2}$ of $\bm A$,

\[
([\hat T_{\sigma_1}(\bm A)]_{\leq n}, [\hat T_{\sigma_2}(\bm A)]_{\leq n}) \in \misp  \quad (\text{respectively, } \mispdb).
\]

Let $ij$, $ji$ denote the permutations of $\{i, j\}$ and $E = [n] \mi \{i, j\}$. By compactness and
Lemma <ref>, it is enough to show
that for $a \in A_E$ and any standard
contractions $\hat T_{ij}$, $\hat T_{ji}$ of $\bm A_a \coloneqq (A_a, \omega \rest A_a)$,

\[
([\hat T_{ij}(\bm A_a)]_{\leq 2}, [\hat T_{ji}(\bm A_a)]_{\leq 2})
\in \misp \quad (\text{respectively, }\mispdb).
\]

By Corollary <ref> and Lemma <ref>, it is enough to find a morphism $\bm A_a \fun \bm B$, relatively unary in both coordinates, and  standard contractions $\hat R_{ij}$, $\hat R_{ji}$ of $\bm B$ such that $[\hat R_{ij}(\bm B)]_{\leq 2} = [\hat R_{ji}(\bm B)]_{\leq 2}$. This is just Lemma <ref>.

§.§ The kernel of ${\mu}\mathbb{L}$ and the main theorems

The following proposition is the culmination of the preceding technicalities, which identifies the
congruence relations $\misp$ and $\mispdb$ with those induced by
$\mu\bb L$.

For $\bm U, \bm V \in \mRV[k]$,

\[
[\mu\bb L \bm U] = [\mu\bb L \bm V] \text{ in }\gsk \mVF[k] \quad \text{if and only if} \quad ([\bm U], [\bm V]) \in \misp.
\]

The same holds with respect to $\mRV^{\db}[k]$, $\gsk \mVF^\diamond[k]$, and $\mispdb$.

The “if” direction simply follows from Lemma <ref> and
Proposition <ref>.

For the “only if” direction, we proceed by induction on $k$. The base case $k = 1$ is of course Lemma <ref>. For the inductive step, let

\[
\mu\bb L \bm U = \bm B_1 \to^{G_1} \bm B_2 \cdots \bm B_l \to^{G_l} \bm B_{l+1} = \mu\bb L \bm V
\]

be relatively unary $\mVF[k]$-morphisms, which exist by Lemma <ref>. For each $j \leq l - 2$, we can choose five standard contractions

\[
[\bm U_j]_{\leq k}, \quad [\bm U_{j+1}]_{\leq k}, \quad [\bm U'_{j+1}]_{\leq k}, \quad [\bm U''_{j+1}]_{\leq k}, \quad [\bm U_{j+2}]_{\leq k}
\]

of $\bm B_j$, $\bm B_{j+1}$, $\bm B_{j+1}$, $\bm B_{j+1}$, $\bm B_{j+2}$ with the permutations $\sigma_{j}$, $\sigma_{j+1}$, $\sigma'_{j+1}$, $\sigma''_{j+1}$, $\sigma_{j+2}$ of $[k]$, respectively, such that

* $\sigma_{j+1}(1)$ and $\sigma_{j+1}(2)$ are the $\VF$-coordinates targeted by $G_{j}$ and $G_{j+1}$, respectively,

* $\sigma''_{j+1}(1)$ and $\sigma''_{j+1}(2)$ are the $\VF$-coordinates targeted by $G_{j+1}$ and $G_{j+2}$, respectively,

* $\sigma_{j} = \sigma_{j+1}$, $\sigma''_{j+1} =  \sigma_{j+2}$,  and $\sigma'_{j+1}(1) = \sigma''_{j+1}(1)$,

* the relation between $\sigma_{j+1}$ and $\sigma'_{j+1}$ is as described in Lemma <ref>.

By Corollary <ref> and Lemma <ref>, all the adjacent pairs of these standard contractions are indeed $\misp$-congruent, except $([\bm U'_{j+1}]_{\leq k}, [\bm U''_{j+1}]_{\leq k})$.  Since we can choose $[\bm U'_{j+1}]_{\leq k}$, $[\bm U''_{j+1}]_{\leq k}$ so that they start with the same contraction in the first targeted $\VF$-coordinate of $\bm B_{j+1}$, the resulting sets from this step are the same. Therefore, applying  the inductive hypothesis in each fiber over the just contracted coordinate, we see that this last pair is also $\misp$-congruent. This completes the “only if” direction.

The same argument works for the other case. Notice that Lemma <ref> is no longer needed since it is built into the definition of $\mVF^\diamond[k]$.

Recall from Remark <ref> the obvious surjective semiring homomorphism
$\bb F : \gsk \mRV[*] \epi \gsk \mgRV[*]$. The congruence relation $\misp$ induces a semiring congruence relation $\mgisp$ on $\gsk \mgRV[*]$ via $\bb F$, which may also be regarded as the coarser congruence relation on $\gsk \mRV[*]$ generated by $\misp$ and the kernel of $\bb F$; similarly for the congruence relation $\mgispdb$ on $\gsk \mRV^{\db}[*]$.

By Lemma <ref> and Remark <ref>, if $([\bm U], [\bm V]) \in \mgisp$ then  $[{\mgL}{\bb F\bm U}] = [{\mgL} \bb F\bm V]$. Conversely, suppose that $[{\mgL}{\bb F\bm U}] = [{\mgL} \bb F\bm V]$ in  $\gsk \mgVF[*]$. By (the remark before) Lemma <ref>, there is an $\bm A \in \mVF[*]$ such that $[{\mL}{\bm U}] = [\bm A]$ in  $\gsk \mVF[*]$ and $\bb F \bm A = {\mgL} \bb F\bm V$. It is easy to see that, after attaching additional $\RV$-coordinates to account for each other's volume forms, there are standard contractions $\bm U'$, $\bm V'$ of $\bm A$, ${\mL} {\bm V}$ such that the identity map is a morphism $\bb F \bm U' \fun \bb F \bm V'$. So we may deduce $([\bm U], [\bm V]) \in \mgisp$ from Proposition <ref>.

By the same reasoning, we have

\[
[{\mgL}{\bb F\bm U}] = [{\mgL} \bb F\bm V] \text{ in } \gsk \mgVF^\diamond[*] \quad \text{if and only if} \quad  ([\bm U], [\bm V]) \in \mgispdb.
\]

Proposition <ref> shows that the kernel of $\mL$ in $\gsk \mRV[*]$ is indeed generated by the pair $([1],  [\RV^{\circ \circ}])$ and hence the corresponding ideal of the graded ring $\ggk \mRV[*]$ is generated by the element $\bm P$ (Notation <ref>). On the other hand, the kernel  of $\mL$ in $\gsk \mRV^{\db}[*]$ is generated by the pairs $([1], [\RV^{\circ \circ}(t)_\gamma])$, where $\gamma \in \absG$ and $t \in \gamma^\sharp$ are definable (Notation <ref>), and hence  the corresponding ideal of the graded ring $\ggk \mRV^{\db}[*]$  is generated by the set $\bm P_\Gamma$ of elements $\bm P_\gamma$, $\abs \gamma > 0$ (Notation <ref>); note that the class $\bm P_\gamma$ does not depend on the choice of $t_\gamma \in \gamma^\sharp$.

Remark <ref> shows the same thing for the ideals of $\ggk \mgRV[*]$, $\ggk \mgRV^{\db}[*]$ induced by $\mgL$.

For each $k \geq 0$ there is a canonical isomorphism of Grothendieck semigroup

\[
\int_{+} : \gsk  \mVF[k] \fun \gsk  \mRV[k] /  \misp
\]

such that

\[
\int_{+} [\bm A] = [\bm U]/  \misp \quad \text{if and only if} \quad  [\bm A] = [\mu\bb L\bm U].
\]

Putting these together, we obtain a canonical isomorphism of graded Grothendieck semirings

\[
\int_{+} : \gsk \mVF[*] \fun \gsk  \mRV[*] /  \misp.
\]

Similarly, there are three other such isomorphisms

\begin{gather*}
\int_{+}: \gsk \mgVF[*] \fun \gsk  \mgRV[*] /  \mgisp, \\
\int^{\diamond}_+ : \gsk \mVF^\diamond[*] \fun \gsk  \mRV^{\db}[*] /  \mispdb,\\
\int^{\diamond}_+  : \gsk \mgVF^\diamond[*] \fun \gsk  \mgRV^{\db}[*] /  \mgispdb.
\end{gather*}

This is immediate by Corollary <ref>, Proposition <ref>, Remarks <ref> and <ref>.

The  isomorphism $\int_+$ induces  two graded ring homomorphisms

\[
\Xint{\textup{e}}^g, \Xint{\textup{e}}^b: \ggk \mgVF[*] \to^{\int} \ggk \mgRV[*] / (\bm P) \two^{\mgE_{g}}_{\mgE_{b}} \F_3\abs\Gamma[X].
\]

In contrast, the  isomorphism $\int_{+}^\diamond$ induces only one graded ring homomorphism

\[
\Xint{\textup{e}}^\diamond : \ggk \mgVF^\diamond[*] \to^{\int^\diamond} \ggk \mgRV^{\db}[*] / (\bm P_\Gamma) \to^{\mgE^{\db}} \Z[X].
\]

This is of course just a combination of Theorem <ref>, Remark <ref>, and Propositions <ref> and <ref>.

Let $F$ be a definable set with $A \coloneqq F_{\VF} \sub \VF^n$ and $\omega : F \fun \RV$ a definable function on $F$. Note that we are not assuming $F \in \VF_*$.

The pair $(F, \omega)$ is viewed as a representative of a definable function

\[
(\bm F, \bm \omega) : A \fun \gsk \mRV[*] / \misp
\]

given by $a \efun [(F_a, \omega_a)] / \misp$, where $\omega_a$ is the function on $F_a$ induced by $\omega$.

Note that $[(F_a, \omega_a)]$ depends on the parameter $a$ and, for distinct $a, a' \in A$, there is a priori no way to compare $[(F_a, \omega_a)]$ and $[(F_{a'}, \omega_{a'})]$ unless we work over the substructure $\mdl S \la a, a' \ra$. Similarly, given another definable pair $(G, \sigma)$ of this form with $A = G_{\VF}$, we say that the corresponding definable function $(\bm G, \bm \sigma)$ is equivalent to $(\bm F, \bm \omega)$, written as $(\bm G, \bm \sigma) \sim (\bm F, \bm \omega)$, if $(\bm G, \bm \sigma)(a) = (\bm F, \bm \omega)(a)$ over $\mdl S \la a \ra$ for all $a \in A$ outside a definable subset of $\VF$-dimension less than $n$. Thus, if $\dim_{\VF}(A) < n$ then there is only one such function on $A$, namely $0$. The set of all such functions, or rather the equivalence classes of such functions, is denoted by $\mfn_+(A)$, which is a  $\gsk  \mRV[*] / \misp$-semimodule. If $E \sub [n]$ is a nonempty set then, for each $a \in \pr_{E}(A)$, the definable function in $\mfn_+(A_a)$ represented by $(F_a, \omega_a)$ is denoted by $(\bm F_a, \bm \omega_a)$.

We say that  $(\bm F, \bm \omega)$ is proper invariant if $(F, \omega)$ is proper invariant (recall Remark <ref>). Notice that if $(\bm G, \bm \sigma)$ is also proper invariant and $(\bm G, \bm \sigma) \sim (\bm F, \bm \omega)$ then $(\bm G, \bm \sigma)(a) = (\bm F, \bm \omega)(a)$ over $\mdl S \la a \ra$ for all $a \in A$. The set of proper invariant functions is denoted by $\mfn^\diamond_+(A)$, which is a  $\gsk  \mRV^{\db}[*] / \mispdb$-semimodule.

The semimodules $\mgfn_+(A)$, $\mgfn^\diamond_+(A)$ with $\Gamma$-volume forms are constructed likewise.

Let $\bb L F = \bigcup_{a \in A} a \times F_a^\sharp$ and $\bb L \omega$ be the function on $\bb L F$ induced by $\omega$. Set $\int_{+A} (\bm F, \bm \omega) = \int_+ [(\bb L F, \bb L \omega)]$,
which, by Theorem <ref> and compactness, does not depend on the representative $(F, \omega)$ (alternatively, this also follows from Lemma <ref>). If $(\bm F, \bm \omega)$ is proper invariant then we replace $\int_+$ with $\int^\diamond_+$. Thus there are canonical homomorphisms of semimodules:

\begin{gather*}
\int_{+A} : \mfn_+(A) \fun \gsk \mRV[*] /  \misp, \\
\int_{+A}^\diamond : \mfn^\diamond_+(A) \fun \gsk \mRV^{\db}[*] /  \mispdb;
\end{gather*}

similarly for the semimodules  with $\Gamma$-volume forms.

For all definable functions $(\bm F, \bm \omega)$ on $A$ and all nonempty sets $E, E' \sub [n]$,

\[
\int_{+ a \in \pr_{E}(A)} \int_{+ A_a}  (\bm F_a, \bm \omega_a) = \int_{+ a \in \pr_{E'}(A)} \int_{+ A_a} (\bm F_a, \bm \omega_a).
\]

This is clear since both sides equal $\int_{+A} (\bm F, \bm \omega)$.

Let $B \sub \VF^n$ be a definable set and $\phi : B \fun A$ a definable  bijection. Suppose that $\phi$ is a $\mVF^\diamond[n]$-morphism (volume forms are ignored) if $(F, \omega)$ is proper invariant.

Let $F_B = \bigcup_{b \in B} b \times F_{\phi(b)}$. For simplicity, the bijection $F_B \fun F$ induced by $\phi$ is still denoted by $\phi$. By Corollary <ref>, if $(F, \omega)$ is proper invariant then $(F_B, \omega \circ \phi)$ is proper invariant as well. So $(F_B, \omega \circ \phi)$ represents a function in $\mfn_+(B)$ or $\mfn^\diamond_+(B)$, which does not depend on the representative $(F, \omega)$ and is denoted by $( \bm F \circ \phi, \bm \omega \circ \phi)$. The corresponding functions

\[
\phi_* : \mfn_+(A) \fun \mfn_+(B), \quad \phi_* : \mfn^\diamond_+(A) \fun \mfn^\diamond_+(B);
\]

are indeed isomorphisms of semimodules; similarly for the semimodules  with $\Gamma$-volume forms. However, in general, these do not preserve integrals.

Let $\sigma : B \fun \RV$ be a definable function such that $\sigma = \rv \circ (\jcb_{\VF} \phi)$ outside a definable subset of $\VF$-dimension less than $n$ and,  if $(F, \omega)$ is proper invariant, then $\sigma$ is proper covariant. Let  $\omega  \sigma$ be the function on $F_{B}$ given by $(b, t) \efun (\omega \circ \phi)( b, t) \cdot \sigma( b)$. Then  $(F_B, \omega  \sigma)$ represents another function in $\mfn_+(B)$ or $\mfn^\diamond_+(B)$, which is denoted by $( \bm F \circ \phi, \bm {\omega \sigma})$.

The Jacobian transformation of $(\bm F, \bm \omega)$ with respect to $\phi$ and $\sigma$ is given by
$\phi^{\sigma}_{*}(\bm F, \bm \omega) = ( \bm F \circ \phi, \bm {\omega \sigma})$.

The Jacobian transformation itself does depend on the choice of $\sigma$. However, the point is that the integral does not:

$\int_{+A} ( \bm F, \bm \omega) = \int_{+B} \phi^{\sigma}_{*}(\bm F, \bm \omega)$.

Let $\bb L \phi$ be the bijection $\bb L F_B \fun \bb L F$ induced by $\phi$.
For all $(b, b') \in \bb L F_B$ outside a definable subset of $\VF$-dimension less than $n+m$, where $F_{\RV} \sub \RV^m$, we have $\jcb_{\VF} \bb L \phi (b, b') = \jcb_{\VF} \phi(b)$. So  $\bb L \phi$ is a $\mVF[*]$- or $\mVF^\diamond[*]$-morphism $(\bb L F_B, \bb L \omega\sigma) \fun (\bb L F, \bb L \omega)$. The equality then follows from Theorem <ref>.

[1]
Lou van den Dries, $T$-convexity and tame extensions II, Journal of
Symbolic Logic 62 (1997), no. 1, 14–34.

[2]
, Tame topology and -minimal structures, LMS Lecture Note
Series, vol. 248, Cambridge University Press, Cambridge, UK, 1998.

[3]
Lou van den Dries and Adam H. Lewenberg, $T$-convexity and tame
extensions, Journal of Symbolic Logic 60 (1995), no. 1, 74–102.

[4]
Lou van den Dries and Patrick Speissegger, The field of reals with
multisummable series and the exponential function, Proc. London Math. Soc.
81 (2000), no. 3, 513–565.

[5]
Jan Holly, Canonical forms for definable subsets of algebraically closed
and real closed valued fields, Journal of Symbolic Logic 60 (1995),
no. 3, 843–860.

[6]
Ehud Hrushovski and David Kazhdan, Integration in valued fields,
Algebraic geometry and number theory, Progr. Math., vol. 253, Birkhäuser,
Boston, MA, 2006, math.AG/0510133, pp. 261–405.

[7]
M. Kageyama and M. Fujita, Grothendieck rings of $o$-minimal expansions
of ordered abelian groups, Journal of Algebra 299 (2006), 8–20,

[8]
Dugald Macpherson, David Marker, and Charles Steinhorn, Weakly
-minimal structures and real closed fields, Transactions of the
American Mathematical Society 352 (2000), no. 12, 5435–5483.

[9]
James Tyne, $T$-levels and $T$-convexity, Ph.D. thesis, University
of Illinois at Urbana-Champaign, 2003.

[10]
Yimu Yin, Fourier transform of the additive group in algebraically
closed valued fields, Selecta Mathematica 20 (2014), no. 4,
1111–1157, arXiv:0903.1097.

[11]
, Generalized Euler characteristic in power-bounded $T$-convex
valued fields,  (2014), to appear in Compositio Mathematica.