From Internal to External: Classical Models of ZF + PP + $\mathrm{\neg }$AC

Goal. We analyze when the Partition Principle ($\mathsf{P}\mathsf{P}$) holds without $\mathsf{A}\mathsf{C}$ in models arising from a free finite $H$-action on Cantor space, and reconcile two standard routes to such models. Approach. Route I proceeds via a Boolean-valued presentation $\mathrm{S}\mathrm{h}(\mathbb{B})$ and symmetric names; Route II uses direct forcing with $\mathrm{F}\mathrm{n}(\mathbb{N}\times H,2)$ and finite-support automorphisms. We prove a unification theorem identifying the resulting symmetric submodels and develop a Local-to-Global Embedding Principle (LEP) for hereditarily symmetric names. Results. We prove external $\mathsf{P}\mathsf{P}$ in the symmetric model $N$ built via Route II. From LEP we obtain that $\mathsf{P}\mathsf{P}$ holds in the symmetric model, hence $N\models \mathsf{Z}\mathsf{F}+\mathsf{P}\mathsf{P}+\mathrm{\neg }\mathsf{A}\mathsf{C}$. Along the way, we unify the Route I/Route II presentations functorially. Limitations. Our proof exploits the countable-support stratification of $\mathrm{F}\mathrm{n}(\mathbb{N}\times H,2)$; extending the LEP/gluing to uncountable presentations (e.g. $\mathrm{F}\mathrm{n}(\kappa \times H,2)$ for $\kappa >\omega$) or, more generally, to $\kappa$-directed families of finite supports remains open.