Motivation [connes-000Z]
✍️source

    The motivation for this formalization experiment is threefold.

    1. Mathematical motivation

      The three counterexamples form a controlled test of nonfaithfulness. OpenAI varies the abelian kernel [openai2026tenadvances, Chapter 4]; Zhou fixes the kernel while varying the action and module structure [zhou2026icc, Sections 1 and 3]; and Anthropic fixes both while varying the extension class [anthropic2026icc, Sections 3–5]. In each construction, a genuine group distinction survives algebraically but disappears after measurable crossed-product transport. The comparison asks which distinctions survive representation, twisting, duality, and analytic completion. Property (T) here serves as a control condition: failure of reconstruction persists for groups with strong representation-theoretic rigidity.

      2. Formalization motivation

        Formalization asks where the information is lost. Named interfaces for the characteristic-two retraction, Fourier shear, measurable transport, continuous closure, spectral detection, and characteristic-module obstruction turn the claim that a factor forgets structure into an auditable dependency map. This separates direct translation from designed bridges and makes the project a consumer of Mathlib and TauCeti. Missing or bespoke interfaces mark candidates for reusable contributions to those libraries.

        3. Agent-assisted work and human examination

          The project also tests whether an agent-authored formalization can be brought to a standard suitable for human examination and digestion. Literature grounding, the exact external premise boundary, provenance, technical proof replay, mathematical audit, and companion notes answer different questions. Technical verification checks the formal statement and its replay; source and mathematical review ask whether the theorem, definitions, hypotheses, and supporting facts match the intended mathematics. A reader can then trace a claim from the literature to its Lean declaration, downstream use, audit status, and executable check.

          References

            Reference. ICC property-(T) groups without W-star-superrigidity [zhou2026icc]

            @misc{zhou2026icc,
  title = {ICC Property-(T) Groups Without W*-Superrigidity},
  author = {Zhou, Shuoxing},
  year = {2026},
  eprint = {2608.02327},
  archivePrefix = {arXiv},
  primaryClass = {math.OA},
  url = {https://arxiv.org/abs/2608.02327}
}

            Reference. Ten advances in mathematics and theoretical computer science [openai2026tenadvances]

            @misc{openai2026tenadvances,
  title = {Ten Advances in Mathematics and Theoretical Computer Science},
  author = {{OpenAI}},
  year = {2026},
  url = {https://cdn.openai.com/pdf/ten-proofs-oai.pdf}
}

            Reference. Two non-isomorphic ICC property (T) groups with isomorphic group von Neumann algebras [anthropic2026icc]

            @misc{anthropic2026icc,
  title = {Two Non-Isomorphic ICC Property (T) Groups with Isomorphic Group von Neumann Algebras},
  author = {{Anthropic}},
  year = {2026},
  url = {https://www-cdn.anthropic.com/files/4zrzovbb/website/1f7272990efcd274cbf92b6fdc14e3e280f59fdc.pdf}
}

            Context

              Introduction [connes-0010]

              Connes' rigidity conjecture [connes-000O]

                For a countable discrete group \(\Gamma \), the group von Neumann algebra \(L(\Gamma )\) is generated by the left regular representation of \(\Gamma \). When \(\Gamma \) has infinite conjugacy classes (ICC), meaning that every nonidentity conjugacy class is infinite, \(L(\Gamma )\) is a \(\mathrm {II}_1\) factor. The reconstruction question asks how much of \(\Gamma \) remains visible in that analytic completion.

                Kazhdan's property (T) says that a unitary representation with almost invariant unit vectors has a nonzero invariant vector [ershov2010noncommutative, Section 3.1]. ICC makes the group von Neumann algebra a factor, while property (T) imposes representation-theoretic rigidity. These are the two hypotheses in the conjecture and in all three counterexample constructions below [zhou2026icc, Section 1, pp. 1–2].

                Connes first proved that, for an ICC property-(T) group, \(\operatorname {Out}(L(\Gamma ))\) and the fundamental group \(\mathcal F(L(\Gamma ))\) are countable [zhou2026icc, Section 1, p. 1].

                He subsequently proposed that such groups should be \(W^*\)-superrigid: for every countable group \(\Lambda \), an isomorphism \(L(\Lambda )\cong L(\Gamma )\) should force \(\Lambda \cong \Gamma \). Zhou's introduction states this original 1982 conjecture and distinguishes it from the later, narrower rigidity question for higher-rank lattices [zhou2026icc, Section 1, pp. 1–2].

                The counterexamples considered here disprove the broad conjecture. They do not settle that higher-rank-lattice question.

                Counterexample background [connes-000P]

                  The OpenAI and Zhou counterexamples were obtained independently and at nearly the same time. Zhou records that his preliminary manuscript predated the public OpenAI announcement, while acknowledging that the two projects were concurrent [zhou2026icc, Section 1, pp. 2–3].

                  OpenAI gives a countable family of pairwise nonisomorphic ICC property-(T) groups with isomorphic group factors [openai2026tenadvances, Chapter 4]. Zhou gives an explicit pair through a different action-changing construction [zhou2026icc, Theorem A and Section 3].

                  The later Anthropic proof gives another explicit pair by comparing a split extension with a nonsplit one [anthropic2026icc, Sections 3–5].

                  These are not three presentations of one proof. The algebraic datum hidden by the factor sits at a different level in each construction, and each factor argument removes it by a different measurable mechanism. The mathematical and formalization motivations for comparing them are stated next. The detailed OpenAI and Anthropic architectures appear in § [connes-000M] and § [connes-000N]; Sections 2–7 below follow Zhou's proof in its original order.

                  Motivation [connes-000Z]
                  ✍️source

                    The motivation for this formalization experiment is threefold.

                    Mathematical motivation

                      The three counterexamples form a controlled test of nonfaithfulness. OpenAI varies the abelian kernel [openai2026tenadvances, Chapter 4]; Zhou fixes the kernel while varying the action and module structure [zhou2026icc, Sections 1 and 3]; and Anthropic fixes both while varying the extension class [anthropic2026icc, Sections 3–5]. In each construction, a genuine group distinction survives algebraically but disappears after measurable crossed-product transport. The comparison asks which distinctions survive representation, twisting, duality, and analytic completion. Property (T) here serves as a control condition: failure of reconstruction persists for groups with strong representation-theoretic rigidity.

                      Formalization motivation

                        Formalization asks where the information is lost. Named interfaces for the characteristic-two retraction, Fourier shear, measurable transport, continuous closure, spectral detection, and characteristic-module obstruction turn the claim that a factor forgets structure into an auditable dependency map. This separates direct translation from designed bridges and makes the project a consumer of Mathlib and TauCeti. Missing or bespoke interfaces mark candidates for reusable contributions to those libraries.

                        Agent-assisted work and human examination

                          The project also tests whether an agent-authored formalization can be brought to a standard suitable for human examination and digestion. Literature grounding, the exact external premise boundary, provenance, technical proof replay, mathematical audit, and companion notes answer different questions. Technical verification checks the formal statement and its replay; source and mathematical review ask whether the theorem, definitions, hypotheses, and supporting facts match the intended mathematics. A reader can then trace a claim from the literature to its Lean declaration, downstream use, audit status, and executable check.

                          Formalization design [connes-000K]

                          The Lean development turns the preceding motivations into one construction stage and four certificate lanes: factor equivalence, property (T), ICC, and group nonisomorphism. The final theorem assembles those four endpoints.

                          The diagram is a map of both the proof and the notes. Solid arrows are internal Lean developments. The dashed arrow is the sole substantive mathematical input left external: the Ershov–Jaikin-Zapirain–Kassabov property-(T) theorem for \(\mathrm {EL}_3(\mathbb F_2[t])\). Each lane uses a separate port at the construction and theorem nodes.

                          The mathematical weight is uneven:

                          • Construction. The characteristic-two calculation in Lemma [connes-000C], with its Lean realization in § [connes-000U], is concrete algebra and supplies every later carrier.
                          • Factor equivalence. Theorem [connes-0007], § [connes-000D], and § [connes-000E] carry heavy operator algebra: compact duals, Haar measure, Fourier transforms, von Neumann closures, and trace transport.
                          • Property (T). Definition [connes-0003], § [connes-000V], Theorem [connes-0004], § [connes-000Y], Lemma [connes-0005], and § [connes-000W] carry heavy harmonic and representation theory. Spectral measures and finite detectors are internal; EJZK enters at one boundary.
                          • ICC. Theorem [connes-0006] is the lightest lane conceptually, but its implementation in § [connes-000X] still needs exact orbit and finite-quotient displacement calculations.
                          • Nonisomorphism. Theorem [connes-0008] is the deepest internal algebraic chain. Characteristic kernels, quotient twists, semisimplicity, and a finite cocycle obstruction must survive an arbitrary isomorphism.

                          Most definitions and algebraic laws translate directly. Six interfaces require special design:

                          • the square-span certificate implemented in § [connes-000U];
                          • the Fourier-shear proof of factor equivalence: its unitary implementation in Theorem [connes-0007], its automatic projection-order transport in § [connes-001C], the four conjugation identities in § [connes-001D], and the measure and closure arguments in § [connes-000D] and § [connes-000E];
                          • the quantitative detector and qualitative property-(T) boundary in Definition [connes-0003], § [connes-000V], Theorem [connes-0004], and § [connes-000Y];
                          • the three-case ICC criterion in Theorem [connes-0006] and § [connes-000X];
                          • the quotient twist in § [connes-000H]; and
                          • the proposition-valued assembly in § [connes-0002].

                          The formalization lessons are discussed in § [connes-000A], § [connes-000F], § [connes-001C], § [connes-001D], and § [connes-000J].

                          The code has two layers. Reusable group theory, linear algebra, topology, measure theory, and operator algebra live in a foundation layer. Zhou-specific carriers and certificates live in construction and paper layers. This separation lets the paper-facing modules state small consumer interfaces while coordinate or finite calculations remain behind named certificates.

                          The public formalization plan and statement map give the complete module and declaration crosswalk.

                          Each lane exports the smallest object needed by its next consumer: a spatial witness, a qualitative property-(T) certificate, orbit and displacement data, or a twist-stable module obstruction.

                          Four corrections were mathematically decisive:

                          • replace identity-action scaffolds by Zhou's actions;
                          • make the ICC abstraction handle the finite \(\operatorname {Sp}_4(\mathbb F_2)\) factor;
                          • follow the quotient automorphism induced by a hypothetical group isomorphism; and
                          • tie the factor target to the Fourier shear and completed von Neumann closures.

                          The final interface remains proposition-valued. Its assembly and trust boundary are detailed in § [connes-0002] and Theorem [connes-0009]; the remaining EJZK work is scoped in § [connes-000B], § [connes-000G], and § [connes-000I]; the representation-universe boundary is recorded in § [connes-000L].

                          Section 1 separates the mathematical introduction, counterexample background, three motivations, and design. Sections 2–7 correspond respectively to Zhou's Sections 2–7; their headings record that correspondence without reusing Zhou's section number as the note title. Section 8 collects proof-engineering adaptations, Sections 9–10 compare the other two proof architectures, Section 11 scopes the remaining EJZK formalization, and Section 12 records the human–agent contribution and review workflow.

                          The formalization adapts selected public Lean proof blocks and organization patterns from a pinned openai/ten-proofs snapshot, but does not import that repository. The project records declaration-level adaptations in its public port map; the concrete Zhou carriers, corrected theorem boundaries, and final assembly are local to this development.

                          Backlinks

                            Agent-assisted work and human examination [connes-000T]

                              This draft expands the examination method summarized in § [connes-000Z].

                              An agent-authored formalization is easier to examine when the code comes with a route back to the literature, an executable verification record, and an audit of the questions that technical checks cannot settle. This project tests that combined method.

                              • Grounding: mathematical claims tied to the literature and external inputs identified at their exact Lean boundary.
                              • Technical verification: statement and axiom comparison, Landlock and network isolation, and replay through the Lean kernel and nanoda, as recorded in the Comparator note.
                              • Mathematical audit: source correspondence, definitions, hypotheses, concrete consumers, literature claims, and proof architecture tracked in the audit ledger.
                              • Traceability: declarations and transferred proof material connected to their sources by the provenance ledger.
                              • Exposition: mathematical arguments, implementation choices, and unresolved boundaries collected in these notes.

                              Together these layers let a reader follow a claim from the literature to its Lean declaration, downstream consumer, audit status, and executable check. The resulting draft includes the material a human needs to examine and digest the work.

                              Formalization motivation [connes-000S]

                                This draft expands the formalization motivation summarized in § [connes-000Z].

                                The mathematical comparison identifies where information is lost. The formalization asks whether that loss can be exposed as an explicit proof interface. Lean turns the claim that a factor forgets structure into an auditable dependency map.

                                • Expose hidden interfaces: square-span, Fourier shear, measurable transport, continuous closure, spectral detection, characteristic kernels, and quotient-twisted modules.
                                • Separate routine translation from proof design: the concrete boundaries are summarized in § [connes-000K].
                                • Make forgetting auditable: each change of structure crosses a named Lean interface.

                                Library consumer. The project uses Mathlib and TauCeti algebraic, analytic, and representation-theoretic infrastructure. Its missing or bespoke interfaces indicate where contributions to those libraries could support later formalizations. The present library boundary is recorded in § [connes-000G].

                                Mathematical motivation [connes-000Q]

                                  This draft expands the mathematical motivation summarized in § [connes-000Z].

                                  The counterexample is not merely a negative answer to Connes' conjecture. Its richer content is a controlled experiment in nonfaithfulness. The three proof families vary different algebraic inputs while preserving the analytic output.

                                  The group distinction survives algebraically but disappears after measurable crossed-product transport.

                                  Three kinds of information loss stand out:

                                  • Cocycle: algebraically nontrivial, measurably removable;
                                  • Action: Fourier–Pontryagin transport conjugates distinct module actions; and
                                  • Extension data: characteristic-two data distinguish groups while their factors remain isomorphic.

                                  Property (T) acts as a control condition: these are rigid groups, not examples explained by group-theoretic flexibility. The comparison asks which algebraic distinctions survive representation, twisting, duality, and analytic completion, and at which step the others disappear.