A Non-Conservation Theorem for Mereology

I'm a bit less sure of the content of this second paper, but popping it up here in case some reader notices an error. The previous post showed how to conservatively extend a theory $T$ with axioms $\mathsf{F}$ for mereology (more exactly, for fusions). The axioms of $\mathsf{F}$ are:

$\mathsf{D}_{\preceq}$: $\hspace{5mm} x \preceq y \leftrightarrow y = x \oplus y$.
$\mathsf{D}_{O}$: $\hspace{5mm} xOy \leftrightarrow \exists w(w \preceq x \wedge w \preceq y)$.
$\mathsf{D}_{At}$: $\hspace{3mm} At(x) \leftrightarrow \forall z(z \preceq x \rightarrow z = x)$.
$\mathsf{F}_1$: $\hspace{6mm} x \oplus x = x$.
$\mathsf{F}_2$: $\hspace{6mm} x \oplus y = y \oplus x$.
$\mathsf{F}_3$: $\hspace{6mm} x \oplus (y \oplus z) = (x \oplus y) \oplus z$.
$\mathsf{UF}$: $\hspace{5mm} \exists x \phi(x) \rightarrow \exists! z [\forall x(\phi(x) \rightarrow x \preceq z) \wedge \forall y \preceq z \exists x(\phi(x) \wedge xOy)]$.

Crucial for that result is the restriction of any axiom schemes of $T$ to the original language. At the end of the paper, "What Difference Does it Make?", I wondered if extending Peano arithmetic, $\mathsf{PA}$, with fusion theory and full induction yields a non-conservative extension.

This second paper, "Arithmetic with Fusions", is very much a preliminary draft, and it would be nice if any reader could find a snag. (Some earlier attempts did run into snags, but eventually, it now seems that the two main interpretability results are correct.) In the paper, we argue that the fusion extension of Peano arithmetic, denoted $\mathsf{PAF}$, interprets full second-order arithmetic, $Z_2$. If this is right, then $\mathsf{PAF}$ is a very strong theory indeed. One might also conclude that this sort of non-conservation undermines a fictionalist view of mereological fusions. (This is joint work with Thomas Schindler.)