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.