Chapter 4 of [openai2026tenadvances] constructs a countable family \(\Gamma _n=E_n\rtimes K\). The acting property-(T) group \(K\) is fixed, while the discrete abelian kernels \(E_n\) are dual to different compact group laws on one underlying probability space. Binary carry changes the compact group structure but not its Borel probability space or the relevant \(K\)-action.

Pontryagin duality therefore presents every group factor by the same measured crossed product \(L^\infty (X\times Y)\rtimes K\) [openai2026tenadvances, Chapter 4, Sections 2.3, 4, and 6.1–6.2].

The proof separates the information forgotten by the group-factor functor from the information retained by the abstract group. The common measured action gives isomorphic factors.

For the first pair, order-four torsion already distinguishes the groups. For the full family, the parameter \(n\) is recovered from an intrinsic finite-orbit subgroup of \(E_n[2]/2E_n\); finite-index embeddings simultaneously prove mutual commensurability [openai2026tenadvances, Chapter 4, Sections 5.1, 6.2, and 6.4–6.5].

The same chapter proves property (T) by a relative-property-(T) spectral estimate and a Boolean-polynomial support bound, rather than taking it only from a classical lattice theorem [openai2026tenadvances, Chapter 4, Sections 5.2–5.5].

This is not Zhou's deformation. Zhou keeps both the discrete kernel and the quotient fixed and changes the action; the quadratic shear then conjugates the two dual actions [zhou2026icc, Section 1, pp. 2–3]. Here the action on the underlying measured space is already common, while the compact group law, hence its discrete dual, changes.

The present Lean development formalizes Zhou's action-changing route. Its Fourier and crossed-product interfaces are conceptually reusable, but the shifted carry groups, the infinite family, and its finite-orbit invariant are not claims of the current formalization. This change of kernel is also what lets the OpenAI construction produce an infinite fiber, whereas Zhou's theorem selects one explicit pair.

The balance of proof weight is correspondingly different. Once the compact models are identified as the same measured \(K\)-space, the factor comparison is short. More of the work lies in constructing the shifted family, proving the initial relative-property-(T) estimate, and extracting an intrinsic invariant that distinguishes every parameter. Zhou instead puts substantial weight into the explicit action conjugacy and into transporting a module obstruction through an arbitrary group isomorphism.