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.