Changing the extension class and measurably gauging it away [connes-000N]
Changing the extension class and measurably gauging it away [connes-000N]
The construction in [anthropic2026icc] fixes both the kernel \(A=\mathbb Z^4\) and quotient \(Q=\operatorname {Sp}_4(\mathbb Z)\). It compares the split semidirect product \(\Gamma _0=A\rtimes Q\) with an extension \(\Gamma _\tau \) defined by a nonzero two-torsion class \([\tau ]\in H^2(Q,A)\).
The algebraic difference lies neither in the kernel nor in the action, but in the extension cocycle. The class is obtained as a Bockstein of the theta-characteristic cocycle [anthropic2026icc, Sections 3.1–3.3].
After Fourier transform, the two group factors become an untwisted and a twisted crossed product over \(\mathbb T^4\). A Borel choice of representatives for \(\mathbb R^4/\mathbb Z^4\) produces an integral carry cocycle. The paper combines that carry with a quadratic refinement of the symplectic form to construct phases \(\Psi _g\); their coboundary is exactly the dual twist \(u_\tau \).
The resulting gauge is a trace-preserving isomorphism of the crossed products [anthropic2026icc, Sections 2.3 and 5.1–5.3, especially Theorems 5.1 and 5.2].
Nonisomorphism survives because \([\tau ]\ne 0\): one extension splits and the other does not [anthropic2026icc, Section 4]. The paper proves ICC directly and obtains property (T) from the classical \(\operatorname {Sp}_4(\mathbb Z)\) and relative-property-(T) input, followed by finite-index permanence [anthropic2026icc, Lemmas 3.7–3.8].
The constructions vary three different algebraic data:
- OpenAI changes the kernel through a different compact dual law;
- Zhou changes the action through a nonsplit module extension; and
- Anthropic changes the group-extension class in \(H^2\).
Their measurable repairs also differ: an already common measured action, an explicit conjugacy of actions, and a one-cochain that untwists a crossed-product two-cocycle. Remark 7.1 of [anthropic2026icc] describes the last point as a torsion class becoming measurably trivial on the connected dual while its branch defects are repaired by the quadratic carry terms.
Formalizing this proof would not be a small refactor of the Zhou development. The current factor-transport layer treats untwisted crossed products and strict action conjugacy. The Anthropic route would need:
- explicit group-extension cohomology;
- cocycle-twisted crossed products;
- Borel fundamental-domain representatives; and
- a verified measurable gauge.
Its property-(T) lane appears shorter than the current EJZK boundary, but its factor lane introduces new infrastructure. These claims are not included in the present Lean theorem.